Actual coefficient bounds for the transverse forward equation

The Gram inverse is genuinely constructed and differentiated. Its one fixed factorial shift is absorbed into a coefficient radius enlargement. The source generator and projected forcing coefficients then have shift-zero bounds by actual composition, with explicit polynomial amplitudes.

Genuine parameter regularity of the transverse forward inverse

The source coefficient is formed from the actual Gram inverse and frame coefficients. These constructions and the forced forward solve are smooth in the uniform time norm, without assuming parameter regularity of the homogeneous evolution supplied by (H3).

theorem EulerTransverseForwardRegularity.frameLeftInversePath_contDiff {P : Type u_1} {V : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q : P → C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) {n : WithTop ℕ∞} (hQr : ContDiff ℝ n Q) : ContDiff ℝ n fun (x : P) => EulerTransverseGramPath.frameLeftInversePath T (Q x) c hc ⋯

The actual canonical frame left inverse varies smoothly in parameters.

theorem EulerTransverseForwardRegularity.generator_contDiff {P : Type u_1} {V : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q Q₁ : P → C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) {n : WithTop ℕ∞} (hQr : ContDiff ℝ n Q) (hQ₁r : ContDiff ℝ n Q₁) : ContDiff ℝ n fun (x : P) => EulerTransverseForwardInverse.generator T (Q x) (Q₁ x) c hc ⋯

The literal source generator is smoothly parameterized.

theorem EulerTransverseForwardRegularity.forcing_contDiff {P : Type u_1} {V : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q : P → C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (f : P → C(↑(Set.Icc 0 T), E)) {n : WithTop ℕ∞} (hQr : ContDiff ℝ n Q) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : P) => (EulerTransverseForwardInverse.forcingOperator T (Q x) c hc ⋯) (f x)

Applying the actual projected forcing map preserves smooth parameter dependence.

theorem EulerTransverseForwardRegularity.coordinates_contDiff {P : Type u_1} {V : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (U : (x : P) → EulerLinearDuhamel.Evolution T hT (EulerTransverseForwardInverse.generator T (Q x) (Q₁ x) c hc ⋯)) (f : P → C(↑(Set.Icc 0 T), E)) (a₀ : P → V) {n : WithTop ℕ∞} (hQr : ContDiff ℝ n Q) (hQ₁r : ContDiff ℝ n Q₁) (hf : ContDiff ℝ n f) (ha₀ : ContDiff ℝ n a₀) : ContDiff ℝ n fun (x : P) => EulerTransverseForwardInverse.coordinates T hT (Q x) (Q₁ x) c hc ⋯ (U x) (f x) (a₀ x)

The actually constructed coordinates are smooth in external parameters.

theorem EulerTransverseForwardRegularity.velocity_contDiff {P : Type u_1} {V : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (U : (x : P) → EulerLinearDuhamel.Evolution T hT (EulerTransverseForwardInverse.generator T (Q x) (Q₁ x) c hc ⋯)) (f : P → C(↑(Set.Icc 0 T), E)) (a₀ : P → V) {n : WithTop ℕ∞} (hQr : ContDiff ℝ n Q) (hQ₁r : ContDiff ℝ n Q₁) (hf : ContDiff ℝ n f) (ha₀ : ContDiff ℝ n a₀) : ContDiff ℝ n fun (x : P) => EulerTransverseForwardInverse.velocity T hT (Q x) (Q₁ x) c hc ⋯ (U x) (f x) (a₀ x)

The actual physical velocity inherits uniform-time parameter smoothness.

theorem EulerTransverseForwardRegularity.coordinateDerivative_contDiff {P : Type u_1} {V : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (U : (x : P) → EulerLinearDuhamel.Evolution T hT (EulerTransverseForwardInverse.generator T (Q x) (Q₁ x) c hc ⋯)) (f : P → C(↑(Set.Icc 0 T), E)) (a₀ : P → V) {n : WithTop ℕ∞} (hQr : ContDiff ℝ n Q) (hQ₁r : ContDiff ℝ n Q₁) (hf : ContDiff ℝ n f) (ha₀ : ContDiff ℝ n a₀) : ContDiff ℝ n fun (x : P) => EulerTransverseForwardInverse.coordinateDerivative T hT (Q x) (Q₁ x) c hc ⋯ (U x) (f x) (a₀ x)

The actual coordinate derivative is smooth in external parameters too.

theorem EulerTransverseForwardRegularity.velocityDerivative_contDiff {P : Type u_1} {V : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (U : (x : P) → EulerLinearDuhamel.Evolution T hT (EulerTransverseForwardInverse.generator T (Q x) (Q₁ x) c hc ⋯)) (f : P → C(↑(Set.Icc 0 T), E)) (a₀ : P → V) {n : WithTop ℕ∞} (hQr : ContDiff ℝ n Q) (hQ₁r : ContDiff ℝ n Q₁) (hf : ContDiff ℝ n f) (ha₀ : ContDiff ℝ n a₀) : ContDiff ℝ n fun (x : P) => EulerTransverseForwardInverse.velocityDerivative T hT (Q x) (Q₁ x) c hc ⋯ (U x) (f x) (a₀ x)

The actual physical time derivative is smooth in the same uniform-time parameter norm.

theorem EulerTransverseForwardCoefficientGevrey.inverseRadius_bounds (c C Rc R : ℝ) (hc : 0 < c) (hRc : 0 ≤ Rc) (hR : 2 * EulerTimeLpGramGevrey.gramCost c C 1 * (Rc + 1) ≤ R) : 0 ≤ R ∧ Rc ≤ 4 * R

@[instance_reducible]

noncomputable def EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey1 {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedAddCommGroup (V →L[ℝ] V)

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

Equations

• EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey1 = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey2 {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] : NormedSpace ℝ (V →L[ℝ] V)

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

Equations

• EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey2 = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey3 {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), V →L[ℝ] V)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,V →L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey3 T = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey4 {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), V →L[ℝ] V)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,V →L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey4 T = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey5 {V : Type u_2} {E : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), V →L[ℝ] E)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,V →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey5 T = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey6 {V : Type u_2} {E : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), V →L[ℝ] E)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,V →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey6 T = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey7 {V : Type u_2} {E : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), E →L[ℝ] V)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,E →L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey7 T = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey8 {V : Type u_2} {E : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), E →L[ℝ] V)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,E →L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerTransverseForwardCoefficientGevrey.instTransverseForwardCoefficientGevrey8 T = inferInstance

theorem EulerTransverseForwardCoefficientGevrey.inversePath_coefficient_bound {P : Type u_1} {V : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q : P → C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hQr : ContDiff ℝ (↑⊤) Q) (Rc C₀ Ri : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C₀ 1 * (Rc + 1) ≤ Ri) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => EulerTransverseGramPath.gramInversePath T (Q y) c hc ⋯) x‖ ≤ Ri * EulerGevrey.majorant (4 * Ri) 0 n

The genuine inverse becomes a shift-zero coefficient at radius 4 Ri.

theorem EulerTransverseForwardCoefficientGevrey.frameLeftInversePath_bound {P : Type u_1} {V : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q : P → C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hQr : ContDiff ℝ (↑⊤) Q) (Rc C₀ Ri : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C₀ 1 * (Rc + 1) ≤ Ri) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => EulerTransverseGramPath.frameLeftInversePath T (Q y) c hc ⋯) x‖ ≤ 3 * Ri * C₀ * EulerGevrey.majorant (4 * Ri) 0 n

The actual left inverse K⁻¹ Q* has a polynomial multiplier amplitude.

theorem EulerTransverseForwardCoefficientGevrey.generator_bound {P : Type u_1} {V : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q Q₁ : P → C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hQr : ContDiff ℝ (↑⊤) Q) (hQ₁r : ContDiff ℝ (↑⊤) Q₁) (Rc C₀ C₁ Ri : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C₀ 1 * (Rc + 1) ≤ Ri) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => EulerTransverseForwardInverse.generator T (Q y) (Q₁ y) c hc ⋯) x‖ ≤ 18 * Ri * C₀ * C₁ * EulerGevrey.majorant (4 * Ri) 0 n

The ordinary generator in (12) has actual shift-zero coefficient bounds.

theorem EulerTransverseForwardCoefficientGevrey.projected_forcing_bound {P : Type u_1} {V : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q : P → C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hQr : ContDiff ℝ (↑⊤) Q) (Rc C₀ Ri : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C₀ 1 * (Rc + 1) ≤ Ri) (hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (f : P → C(↑(Set.Icc 0 T), E)) (hf : ContDiff ℝ (↑⊤) f) (R D : ℝ) (hR : 4 * Ri ≤ R) (hD : 0 ≤ D) (d : ℕ) (hbf : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n f x‖ ≤ D * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => (EulerTransverseForwardInverse.forcingOperator T (Q y) c hc ⋯) (f y)) x‖ ≤ 9 * Ri * C₀ * D * EulerGevrey.majorant R d n

Multiplication by the actual projected-forcing coefficient preserves the input factorial shift, with a polynomial amplitude.