Polynomial-radius bounds for the velocity and material acceleration of the constructed flow. The second expression is literally (A₁ + D A · A) ∘ Φ; identifying A₁ as the time derivative is a separate qualitative chain rule, not an assumption about its size.

@[instance_reducible]

noncomputable def EulerSmoothFlowGevrey.instSmoothFlowTimeGevrey1 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedAddCommGroup (E [×n]→L[ℝ] E)

Cache the standard NormedAddCommGroup (E [×n]→L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerSmoothFlowGevrey.instSmoothFlowTimeGevrey1 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothFlowGevrey.instSmoothFlowTimeGevrey2 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedSpace ℝ (E [×n]→L[ℝ] E)

Cache the standard NormedSpace ℝ (E [×n]→L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerSmoothFlowGevrey.instSmoothFlowTimeGevrey2 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothFlowGevrey.instSmoothFlowTimeGevrey3 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction E (E [×n]→L[ℝ] E))

Cache the standard NormedAddCommGroup (E →ᵇ (E [×n]→L[ℝ] E)) instance to shorten typeclass synthesis.

Equations

• EulerSmoothFlowGevrey.instSmoothFlowTimeGevrey3 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothFlowGevrey.instSmoothFlowTimeGevrey4 {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction E (E [×n]→L[ℝ] E))

Cache the standard NormedSpace ℝ (E →ᵇ (E [×n]→L[ℝ] E)) instance to shorten typeclass synthesis.

Equations

• EulerSmoothFlowGevrey.instSmoothFlowTimeGevrey4 n = inferInstance

def EulerSmoothFlowGevrey.flowRadius (B R T S : ℝ) : ℝ

Flow radius, given by (4*R+1)*((1+B*T)*S+2).

Equations

• EulerSmoothFlowGevrey.flowRadius B R T S = (4 * R + 1) * ((1 + B * T) * S + 2)

theorem EulerSmoothFlowGevrey.field_jet_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E) : ‖iteratedFDeriv ℝ n (⇑(A.field t)) x‖ ≤ B * R ^ n * ↑n.factorial ^ 2

theorem EulerSmoothFlowGevrey.forward_positive_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (n : ℕ) (hn : 0 < n) (t : ↑(Set.Icc 0 T)) (x : E) : ‖iteratedFDeriv ℝ n (fun (y : E) => (EulerSmoothBanachFlow.flowData T hT A).forward (↑t) y) x‖ ≤ (1 + B * T) * (4 * R + 1) ^ n * ↑n.factorial ^ 2

noncomputable def EulerSmoothFlowGevrey.materialVelocity {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ↑(Set.Icc 0 T)) (x : E) : E

Material velocity, given by A.field t ((flowData T hT A).forward t x).

Equations

• EulerSmoothFlowGevrey.materialVelocity T hT A t x = (A.field t) ((EulerSmoothBanachFlow.flowData T hT A).forward (↑t) x)

theorem EulerSmoothFlowGevrey.materialVelocity_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E) : ‖iteratedFDeriv ℝ n (materialVelocity T hT A t) x‖ ≤ B * flowRadius B R T R ^ n * ↑n.factorial ^ 2

noncomputable def EulerSmoothFlowGevrey.accelerationField {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ↑(Set.Icc 0 T)) (x : E) : E

Acceleration field, given by A₁.field t x + fderiv ℝ (A.field t : E → E) x (A.field t x).

Equations

• EulerSmoothFlowGevrey.accelerationField T A A₁ t x = (A₁.field t) x + (fderiv ℝ (⇑(A.field t)) x) ((A.field t) x)

theorem EulerSmoothFlowGevrey.accelerationField_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ (↑⊤) (accelerationField T A A₁ t)

theorem EulerSmoothFlowGevrey.accelerationField_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R B₁ R₁ : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hB₁ : 0 ≤ B₁) (hR₁ : 0 ≤ R₁) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (hb₁ : ∀ (n : ℕ), ‖A₁.jet n‖ ≤ B₁ * R₁ ^ n * ↑n.factorial ^ 2) (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E) : ‖iteratedFDeriv ℝ n (accelerationField T A A₁ t) x‖ ≤ (B₁ + 3 * B ^ 2 * R) * EulerGevrey.majorant (4 * R + R₁) 0 n

noncomputable def EulerSmoothFlowGevrey.materialAcceleration {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ↑(Set.Icc 0 T)) (x : E) : E

Material acceleration, given by accelerationField T A A₁ t ((flowData T hT A).forward t x).

Equations

• EulerSmoothFlowGevrey.materialAcceleration T hT A A₁ t x = EulerSmoothFlowGevrey.accelerationField T A A₁ t ((EulerSmoothBanachFlow.flowData T hT A).forward (↑t) x)

theorem EulerSmoothFlowGevrey.materialAcceleration_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R B₁ R₁ : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hB₁ : 0 ≤ B₁) (hR₁ : 0 ≤ R₁) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (hb₁ : ∀ (n : ℕ), ‖A₁.jet n‖ ≤ B₁ * R₁ ^ n * ↑n.factorial ^ 2) (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : E) : ‖iteratedFDeriv ℝ n (materialAcceleration T hT A A₁ t) x‖ ≤ (B₁ + 3 * B ^ 2 * R) * flowRadius B R T (4 * R + R₁) ^ n * ↑n.factorial ^ 2