Source-scale Gevrey bounds for the actual globally constructed Picard flow. Only bounds on the given velocity jets and the small product BRT are hypotheses; smoothness and all time-jet identities of the flow come from its construction.

Finite-order small-flow estimates. The only evolution input is the literal integral (or, in the final theorem, differential) equation for the actual spatial derivatives. The nonlinear majorant is derived here from Faà di Bruno; no bound on the flow derivatives is assumed.

theorem EulerGevreyFlowFinite.derivativeSum_continuousOn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : ℝ → E → F) (N : ℕ) (z T : ℝ) (x : E) (hc : ∀ n ∈ Finset.Icc 1 N, ContinuousOn (fun (t : ℝ) => iteratedFDeriv ℝ n (f t) x) (Set.Icc 0 T)) : ContinuousOn (fun (t : ℝ) => EulerGevreyGeneratingDerivatives.derivativeSum (f t) N z x) (Set.Icc 0 T)

theorem EulerGevreyFlowFinite.derivativeSum_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (N : ℕ) (z : ℝ) (x : E) : EulerGevreyGeneratingDerivatives.derivativeSum 0 N z x = 0

theorem EulerGevreyFlowFinite.derivative_term_le_sum {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (N n : ℕ) (z : ℝ) (x : E) (hn : n ∈ Finset.Icc 1 N) (hz : 0 ≤ z) : ‖iteratedFDeriv ℝ n f x‖ / ↑n.factorial ^ 2 * z ^ n ≤ EulerGevreyGeneratingDerivatives.derivativeSum f N z x

theorem EulerGevreyFlowFinite.derivativeSum_le_integral {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (v : ℝ → E → F) (N : ℕ) (z t : ℝ) (x : E) (ht : 0 ≤ t) (hz : 0 ≤ z) (hc : ∀ n ∈ Finset.Icc 1 N, ContinuousOn (fun (s : ℝ) => iteratedFDeriv ℝ n (v s) x) (Set.Icc 0 t)) (heq : ∀ n ∈ Finset.Icc 1 N, iteratedFDeriv ℝ n f x = ∫ (s : ℝ) in 0..t, iteratedFDeriv ℝ n (v s) x) : EulerGevreyGeneratingDerivatives.derivativeSum f N z x ≤ ∫ (s : ℝ) in 0..t, EulerGevreyGeneratingDerivatives.derivativeSum (v s) N z x

theorem EulerGevreyFlowFinite.flow_generating_sum_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ψ b : ℝ → E → E) (N : ℕ) (T B R : ℝ) (hT : 0 ≤ T) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hψ : ∀ t ∈ Set.Icc 0 T, ContDiff ℝ (↑N) (ψ t)) (hb : ∀ t ∈ Set.Icc 0 T, ContDiff ℝ (↑N) (b t)) (hψ0 : ψ 0 = 0) (hbjet : ∀ t ∈ Set.Icc 0 T, ∀ (y : E), ∀ n ∈ Finset.Icc 1 N, ‖iteratedFDeriv ℝ n (b t) y‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (hcψ : ∀ n ∈ Finset.Icc 1 N, ∀ (x : E), ContinuousOn (fun (t : ℝ) => iteratedFDeriv ℝ n (ψ t) x) (Set.Icc 0 T)) (hcv : ∀ n ∈ Finset.Icc 1 N, ∀ (x : E), ContinuousOn (fun (t : ℝ) => iteratedFDeriv ℝ n (b t ∘ (id + ψ t)) x) (Set.Icc 0 T)) (heq : ∀ n ∈ Finset.Icc 1 N, ∀ t ∈ Set.Icc 0 T, ∀ (x : E), iteratedFDeriv ℝ n (ψ t) x = ∫ (s : ℝ) in 0..t, iteratedFDeriv ℝ n (b s ∘ (id + ψ s)) x) (t : ℝ) : t ∈ Set.Icc 0 T → ∀ (x : E), EulerGevreyGeneratingDerivatives.derivativeSum (ψ t) N (4 * R)⁻¹ x ≤ B * t

Uniform finite-order bound for a genuine flow displacement, from its actual differentiated integral equation. The smallness condition and the resulting radius are independent of N.

theorem EulerGevreyFlowFinite.derivative_bound_of_generating_sum {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (N n : ℕ) (R A : ℝ) (x : E) (hR : 0 < R) (hn : n ∈ Finset.Icc 1 N) (hbound : EulerGevreyGeneratingDerivatives.derivativeSum f N (4 * R)⁻¹ x ≤ A) : ‖iteratedFDeriv ℝ n f x‖ ≤ A * (4 * R) ^ n * ↑n.factorial ^ 2

Extracting one term from the same finite sum gives a single fixed Gevrey radius, rather than a radius enlarged at each derivative order.

theorem EulerGevreyFlowFinite.jet_integral_of_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (ψ v : ℝ → E → E) (n : ℕ) (T : ℝ) (hψ0 : ψ 0 = 0) (hd : ∀ t ∈ Set.Icc 0 T, ∀ (x : E), HasDerivWithinAt (fun (s : ℝ) => iteratedFDeriv ℝ n (ψ s) x) (iteratedFDeriv ℝ n (v t) x) (Set.Icc 0 T) t) (hc : ∀ (x : E), ContinuousOn (fun (t : ℝ) => iteratedFDeriv ℝ n (v t) x) (Set.Icc 0 T)) (t : ℝ) (ht : t ∈ Set.Icc 0 T) (x : E) : iteratedFDeriv ℝ n (ψ t) x = ∫ (s : ℝ) in 0..t, iteratedFDeriv ℝ n (v s) x

The integral equation used above follows from the actual within-time derivative identity on the closed interval, including a degenerate end.

theorem EulerGevreyFlowFinite.flow_generating_sum_bound_of_jet_derivative {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (ψ b : ℝ → E → E) (N : ℕ) (T B R : ℝ) (hT : 0 ≤ T) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hψ : ∀ t ∈ Set.Icc 0 T, ContDiff ℝ (↑N) (ψ t)) (hb : ∀ t ∈ Set.Icc 0 T, ContDiff ℝ (↑N) (b t)) (hψ0 : ψ 0 = 0) (hbjet : ∀ t ∈ Set.Icc 0 T, ∀ (y : E), ∀ n ∈ Finset.Icc 1 N, ‖iteratedFDeriv ℝ n (b t) y‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (hd : ∀ n ∈ Finset.Icc 1 N, ∀ t ∈ Set.Icc 0 T, ∀ (x : E), HasDerivWithinAt (fun (s : ℝ) => iteratedFDeriv ℝ n (ψ s) x) (iteratedFDeriv ℝ n (b t ∘ (id + ψ t)) x) (Set.Icc 0 T) t) (hcv : ∀ n ∈ Finset.Icc 1 N, ∀ (x : E), ContinuousOn (fun (t : ℝ) => iteratedFDeriv ℝ n (b t ∘ (id + ψ t)) x) (Set.Icc 0 T)) (t : ℝ) : t ∈ Set.Icc 0 T → ∀ (x : E), EulerGevreyGeneratingDerivatives.derivativeSum (ψ t) N (4 * R)⁻¹ x ≤ B * t

The finite flow bound using genuine time derivatives of the spatial jets, with no independent integral-equation assumption.

theorem EulerGevreyFlowFinite.flow_positive_derivative_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (ψ b : ℝ → E → E) (T B R : ℝ) (hT : 0 ≤ T) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hψ : ∀ t ∈ Set.Icc 0 T, ContDiff ℝ (↑⊤) (ψ t)) (hb : ∀ t ∈ Set.Icc 0 T, ContDiff ℝ (↑⊤) (b t)) (hψ0 : ψ 0 = 0) (hbjet : ∀ t ∈ Set.Icc 0 T, ∀ (y : E) (n : ℕ), 0 < n → ‖iteratedFDeriv ℝ n (b t) y‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (hd : ∀ (n : ℕ), 0 < n → ∀ t ∈ Set.Icc 0 T, ∀ (x : E), HasDerivWithinAt (fun (s : ℝ) => iteratedFDeriv ℝ n (ψ s) x) (iteratedFDeriv ℝ n (b t ∘ (id + ψ t)) x) (Set.Icc 0 T) t) (hcv : ∀ (n : ℕ), 0 < n → ∀ (x : E), ContinuousOn (fun (t : ℝ) => iteratedFDeriv ℝ n (b t ∘ (id + ψ t)) x) (Set.Icc 0 T)) (t : ℝ) : t ∈ Set.Icc 0 T → ∀ (x : E) (n : ℕ), 0 < n → ‖iteratedFDeriv ℝ n (ψ t) x‖ ≤ B * t * (4 * R) ^ n * ↑n.factorial ^ 2

All positive spatial orders have the same radius 4R and the same linear amplitude B*t. Smoothness and the jet equation are qualitative inputs; the derivative estimates are conclusions.

@[instance_reducible]

noncomputable def EulerSmoothFlowGevrey.instSmoothFlowGevrey1 {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.instSmoothFlowGevrey1 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothFlowGevrey.instSmoothFlowGevrey2 {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.instSmoothFlowGevrey2 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothFlowGevrey.instSmoothFlowGevrey3 {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.instSmoothFlowGevrey3 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothFlowGevrey.instSmoothFlowGevrey4 {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.instSmoothFlowGevrey4 n = inferInstance

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

Velocity extension, given by A.field (projIcc 0 T hT t) x.

Equations

• EulerSmoothFlowGevrey.velocityExtension T hT A t x = (A.field (Set.projIcc 0 T hT t)) x

@[simp]

theorem EulerSmoothFlowGevrey.velocityExtension_apply {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ↑(Set.Icc 0 T)) (x : E) : velocityExtension T hT A (↑t) x = (A.field t) x

theorem EulerSmoothFlowGevrey.velocityExtension_contDiff {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (t : ℝ) : ContDiff ℝ (↑⊤) (velocityExtension T hT A t)

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

theorem EulerSmoothFlowGevrey.composition_jet_hasDerivWithinAt {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (n : ℕ) (x : E) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : HasDerivWithinAt (fun (s : ℝ) => iteratedFDeriv ℝ n (EulerSmoothBanachFlow.displacement T hT A s) x) (iteratedFDeriv ℝ n (velocityExtension T hT A t ∘ (id + EulerSmoothBanachFlow.displacement T hT A t)) x) (Set.Icc 0 T) t

theorem EulerSmoothFlowGevrey.composition_jet_continuous {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (n : ℕ) (x : E) : ContinuousOn (fun (t : ℝ) => iteratedFDeriv ℝ n (velocityExtension T hT A t ∘ (id + EulerSmoothBanachFlow.displacement T hT A t)) x) (Set.Icc 0 T)

theorem EulerSmoothFlowGevrey.constructed_generating_sum_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 : ℝ) (ht : t ∈ Set.Icc 0 T) (x : E) : EulerGevreyGeneratingDerivatives.derivativeSum (EulerSmoothBanachFlow.displacement T hT A t) N (4 * R)⁻¹ x ≤ B * t

A finite generating sum for the actual constructed flow, with a cutoff-independent radius and coefficient.

theorem EulerSmoothFlowGevrey.displacement_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 : ℝ) (ht : t ∈ Set.Icc 0 T) (x : E) : ‖iteratedFDeriv ℝ n (EulerSmoothBanachFlow.displacement T hT A t) x‖ ≤ B * t * (4 * R) ^ n * ↑n.factorial ^ 2

theorem EulerSmoothFlowGevrey.displacement_zero_bound {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (B R : ℝ) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (t : ℝ) (ht : t ∈ Set.Icc 0 T) (x : E) : ‖iteratedFDeriv ℝ 0 (EulerSmoothBanachFlow.displacement T hT A t) x‖ ≤ B * t

Order zero uses direct integration of the actual velocity.

theorem EulerSmoothFlowGevrey.displacement_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 : ℝ) (ht : t ∈ Set.Icc 0 T) (x : E) : ‖iteratedFDeriv ℝ n (EulerSmoothBanachFlow.displacement T hT A t) x‖ ≤ B * t * (4 * R) ^ n * ↑n.factorial ^ 2

Source-only all-order spatial estimate for the actual Picard flow displacement. It includes order zero and is linear in B*t.