Actual source coefficient paths for the transverse inverse

Evaluation of the uniformly smooth spatial coefficient path gives a genuine smooth map from position to time paths. Restriction to the fixed orthonormal reference plane is a linear contraction. The pointwise source derivative bounds therefore imply exactly the time-path coefficient bounds required by the constructed transverse inverse.

The source frame Q = F R⊥

These coefficient lemmas discharge the moving-plane range and lower-frame hypotheses using the prescribed invertible deformation and orthonormal reference plane. No inverse solution or acceleration is supplied as input.

noncomputable def EulerTransverseSourceFrame.referenceEmbedding {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m₀ : E) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) : U →L[ℝ] E

The fixed orthonormal reference-plane embedding.

Equations

• EulerTransverseSourceFrame.referenceEmbedding m₀ R = (EulerTransverseFrameCoordinates.referencePlane m₀).subtypeL ∘SL ↑↑R

noncomputable def EulerTransverseSourceFrame.framePath {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m₀ : E) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (T : ℝ) (F : C(↑(Set.Icc 0 T), E →L[ℝ] E)) : C(↑(Set.Icc 0 T), U →L[ℝ] E)

Applying the source deformation to the fixed orthonormal reference plane.

Equations

• EulerTransverseSourceFrame.framePath m₀ R T F = { toFun := fun (t : ↑(Set.Icc 0 T)) => F t ∘SL EulerTransverseSourceFrame.referenceEmbedding m₀ R, continuous_toFun := ⋯ }

theorem EulerTransverseSourceFrame.framePath_apply {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m₀ : E) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (T : ℝ) (F : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (t : ↑(Set.Icc 0 T)) (x : U) : ((framePath m₀ R T F) t) x = (F t) ↑(R x)

The frame is literally the source expression F R⊥.

theorem EulerTransverseSourceFrame.framePath_tangent {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (m₀ : E) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (T : ℝ) (F : ↑(Set.Icc 0 T) → E ≃L[ℝ] E) (A : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hA : ∀ (t : ↑(Set.Icc 0 T)), A t = ↑(F t)) (t : ↑(Set.Icc 0 T)) (x : U) : inner ℝ (EulerTransverseFrameCoordinates.movingNormal (F t) m₀) (((framePath m₀ R T A) t) x) = 0

The source frame maps into the moving tangent plane.

theorem EulerTransverseSourceFrame.framePath_range {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (m₀ : E) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (T : ℝ) (F : ↑(Set.Icc 0 T) → E ≃L[ℝ] E) (A : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hA : ∀ (t : ↑(Set.Icc 0 T)), A t = ↑(F t)) (t : ↑(Set.Icc 0 T)) (η : E) (hη : inner ℝ (EulerTransverseFrameCoordinates.movingNormal (F t) m₀) η = 0) : ∃ (x : U), ((framePath m₀ R T A) t) x = η

Every moving tangent vector is in the range of the actual source frame.

theorem EulerTransverseSourceFrame.framePath_lower_bound {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m₀ : E) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (T : ℝ) (F : ↑(Set.Icc 0 T) → E ≃L[ℝ] E) (A : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hA : ∀ (t : ↑(Set.Icc 0 T)), A t = ↑(F t)) (B : ℝ) (hB : 0 < B) (hinv : ∀ (t : ↑(Set.Icc 0 T)), ‖↑(F t).symm‖ ≤ B) (t : ↑(Set.Icc 0 T)) (x : U) : B⁻¹ ^ 2 * ‖x‖ ^ 2 ≤ ‖((framePath m₀ R T A) t) x‖ ^ 2

A bound on F⁻¹ gives a quantitative lower frame bound, because R⊥ is isometric.

theorem EulerTransverseSourceFrame.framePath_hasDerivWithinAt {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m₀ : E) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (T : ℝ) (hT : 0 ≤ T) (A A₁ : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (A₁ t) (Set.Icc 0 T) ↑t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (framePath m₀ R T A)) ((framePath m₀ R T A₁) t) (Set.Icc 0 T) ↑t

The actual within-interval derivative commutes with a fixed reference frame.

theorem EulerTransverseSourceFrame.framePath_second_equation {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m₀ : E) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (T : ℝ) (A A₂ H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hframe : ∀ (t : ↑(Set.Icc 0 T)), A₂ t = -H t ∘SL A t) (t : ↑(Set.Icc 0 T)) : (framePath m₀ R T A₂) t = -H t ∘SL (framePath m₀ R T A) t

The source equation F_tt = -H F gives the precise frame equation used in (10).

theorem EulerTransverseSourceFrame.sourceFrame_strong {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (m₀ : E) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (T : ℝ) (hT : 0 < T) (F : ↑(Set.Icc 0 T) → E ≃L[ℝ] E) (A A₁ A₂ H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hA : ∀ (t : ↑(Set.Icc 0 T)), A t = ↑(F t)) (B : ℝ) (hB : 0 < B) (hinv : ∀ (t : ↑(Set.Icc 0 T)), ‖↑(F t).symm‖ ≤ B) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ A) (A₁ t) (Set.Icc 0 T) ↑t) (hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ A₁) (A₂ t) (Set.Icc 0 T) ↑t) (hframe : ∀ (t : ↑(Set.Icc 0 T)), A₂ t = -H t ∘SL A t) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x : E), inner ℝ ((H t) x) x ≤ K * ‖x‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T E)) : have m := fun (t : ↑(Set.Icc 0 T)) => EulerTransverseFrameCoordinates.movingNormal (F t) m₀; have u := ↑((EulerTransverseVariationalInverse.transverseSolver T ⋯ m H K hK hH hsmall) f); ∃ (ξ : ℝ → U) (v : ℝ → U) (a : ↥(EulerTimeLp.TimeLp T U)), AbsolutelyContinuousOnInterval ξ 0 T ∧ AbsolutelyContinuousOnInterval v 0 T ∧ ξ 0 = 0 ∧ ξ T = 0 ∧ (∀ (t : ↑(Set.Icc 0 T)), (F t) ↑(R (ξ ↑t)) = EulerTerminalTimePrimitive.realPrimitive T u ↑t) ∧ (∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt ξ (v t) t) ∧ (∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt v (↑↑a t) t) ∧ ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, (EulerTransverseGramInverse.gram (EulerVolterraConvolution.extendPath T ⋯ (framePath m₀ R T A) t)) (↑↑a t) = (ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T ⋯ (framePath m₀ R T A) t)) (↑↑f t - 2 • (EulerVolterraConvolution.extendPath T ⋯ (framePath m₀ R T A₁) t) (v t))

For the literal source frame F R⊥, the actual transverse inverse has zero-endpoint H² coordinates satisfying equation (10). All range and inverse bounds used by the strong theorem are discharged from F and R⊥ here.

@[instance_reducible]

noncomputable def EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath1 {V : Type u_2} [NormedAddCommGroup V] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space V)

Cache the standard NormedAddCommGroup (Space →ᵇ V) instance to shorten typeclass synthesis.

Equations

• EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath1 = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath2 {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space V)

Cache the standard NormedSpace ℝ (Space →ᵇ V) instance to shorten typeclass synthesis.

Equations

• EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath2 = inferInstance

noncomputable def EulerTransverseSourceCoefficientPath.pathEvaluation {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (x : EulerSmoothLimit.Space) : C(K, BoundedContinuousFunction EulerSmoothLimit.Space V) →L[ℝ] C(K, V)

Actual spatial evaluation, performed uniformly along the time path.

Equations

• EulerTransverseSourceCoefficientPath.pathEvaluation x = ContinuousLinearMap.compLeftContinuous ℝ K (BoundedContinuousFunction.evalCLM ℝ x)

theorem EulerTransverseSourceCoefficientPath.pathEvaluation_norm {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (x : EulerSmoothLimit.Space) : ‖pathEvaluation x‖ ≤ 1

Evaluation is a contraction in the genuine uniform path norm.

noncomputable def EulerTransverseSourceCoefficientPath.pointPath {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerMeanCoefficients.SmoothCoefficientPath K V) (x : EulerSmoothLimit.Space) : C(K, V)

The source coefficient viewed as a time path at a spatial position.

Equations

• EulerTransverseSourceCoefficientPath.pointPath A x = (EulerTransverseSourceCoefficientPath.pathEvaluation 0) (EulerMeanCoefficients.translateCoefficientPath A.field x)

theorem EulerTransverseSourceCoefficientPath.pointPath_apply {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerMeanCoefficients.SmoothCoefficientPath K V) (x : EulerSmoothLimit.Space) (t : K) : (pointPath A x) t = (A.field t) x

The coefficient path has the literal prescribed pointwise values.

theorem EulerTransverseSourceCoefficientPath.pointPath_contDiff {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerMeanCoefficients.SmoothCoefficientPath K V) : ContDiff ℝ (↑⊤) (pointPath A)

Genuine smooth position dependence, in the uniform time-path norm.

theorem EulerTransverseSourceCoefficientPath.pointPath_derivative_bound {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerMeanCoefficients.SmoothCoefficientPath K V) (n : ℕ) (C : ℝ) (hC : 0 ≤ C) (hb : ∀ (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(A.field t)) x‖ ≤ C) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (pointPath A) x‖ ≤ C

Source pointwise derivative bounds give actual operator-norm derivatives of the time path.

theorem EulerTransverseSourceCoefficientPath.pointPath_gevrey {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : EulerMeanCoefficients.SmoothCoefficientPath K V) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (d : ℕ) (hb : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(A.field t)) x‖ ≤ C * EulerGevrey.majorant Rc d n) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (pointPath A) x‖ ≤ C * EulerGevrey.majorant Rc d n

Every prescribed factorial coefficient bound survives the time-path construction.

theorem EulerTransverseSourceCoefficientPath.pointPath_pullback_contDiff {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (L : P →L[ℝ] EulerSmoothLimit.Space) (A : EulerMeanCoefficients.SmoothCoefficientPath K V) : ContDiff ℝ ↑⊤ fun (x : P) => pointPath A (L x)

Independent angle variables can be added by a fixed spatial projection.

theorem EulerTransverseSourceCoefficientPath.pointPath_pullback_derivative_bound {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (L : P →L[ℝ] EulerSmoothLimit.Space) (hL : ‖L‖ ≤ 1) (A : EulerMeanCoefficients.SmoothCoefficientPath K V) (n : ℕ) (C : ℝ) (hC : 0 ≤ C) (hb : ∀ (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(A.field t)) x‖ ≤ C) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => pointPath A (L y)) x‖ ≤ C

A spatial projection of norm at most one preserves the literal source derivative bounds.

theorem EulerTransverseSourceCoefficientPath.pointPath_pullback_gevrey {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] {P : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] (L : P →L[ℝ] EulerSmoothLimit.Space) (hL : ‖L‖ ≤ 1) (A : EulerMeanCoefficients.SmoothCoefficientPath K V) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (d : ℕ) (hb : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(A.field t)) x‖ ≤ C * EulerGevrey.majorant Rc d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => pointPath A (L y)) x‖ ≤ C * EulerGevrey.majorant Rc d n

Joint spatial/angle coefficient bounds follow from the source spatial bounds.

@[instance_reducible]

noncomputable def EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath3 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (U →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath3 = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath4 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ (U →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath4 = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath5 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), U →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath5 T = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath6 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), U →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath6 T = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath7 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath7 T = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath8 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerTransverseSourceCoefficientPath.instTransverseSourceCoefficientPath8 T = inferInstance

theorem EulerTransverseSourceCoefficientPath.referenceEmbedding_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : EulerSmoothLimit.Space) (Rperp : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) : ‖EulerTransverseSourceFrame.referenceEmbedding m₀ Rperp‖ ≤ 1

The fixed orthonormal reference embedding is a contraction, including a trivial plane.

noncomputable def EulerTransverseSourceCoefficientPath.referenceRestriction {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : EulerSmoothLimit.Space) (Rperp : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) : (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) →L[ℝ] U →L[ℝ] EulerSmoothLimit.Space

Restrict an actual coefficient operator to the reference plane.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerTransverseSourceCoefficientPath.framePathMap {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : EulerSmoothLimit.Space) (Rperp : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (T : ℝ) : C(↑(Set.Icc 0 T), EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) →L[ℝ] C(↑(Set.Icc 0 T), U →L[ℝ] EulerSmoothLimit.Space)

The time-path reference restriction is a genuine bounded linear map.

Equations

• EulerTransverseSourceCoefficientPath.framePathMap m₀ Rperp T = ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerTransverseSourceCoefficientPath.referenceRestriction m₀ Rperp)

theorem EulerTransverseSourceCoefficientPath.framePathMap_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : EulerSmoothLimit.Space) (Rperp : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (T : ℝ) (A : C(↑(Set.Icc 0 T), EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) : (framePathMap m₀ Rperp T) A = EulerTransverseSourceFrame.framePath m₀ Rperp T A

This restriction is exactly the source frame path F Rperp.

theorem EulerTransverseSourceCoefficientPath.framePathMap_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : EulerSmoothLimit.Space) (Rperp : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (T : ℝ) : ‖framePathMap m₀ Rperp T‖ ≤ 1

Orthogonal reference restriction does not enlarge the coefficient path norm.

theorem EulerTransverseSourceCoefficientPath.sourceFrame_contDiff {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : EulerSmoothLimit.Space) (Rperp : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (T : ℝ) (A : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) : ContDiff ℝ ↑⊤ fun (x : EulerSmoothLimit.Space) => EulerTransverseSourceFrame.framePath m₀ Rperp T (pointPath A x)

The actual source frame depends smoothly on position in time-path operator norm.

theorem EulerTransverseSourceCoefficientPath.sourceFrame_gevrey {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : EulerSmoothLimit.Space) (Rperp : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (T : ℝ) (A : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (d : ℕ) (hb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(A.field t)) x‖ ≤ C * EulerGevrey.majorant Rc d n) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (y : EulerSmoothLimit.Space) => EulerTransverseSourceFrame.framePath m₀ Rperp T (pointPath A y)) x‖ ≤ C * EulerGevrey.majorant Rc d n

Source spatial factorial bounds give the exact frame-path bounds used by the inverse.

theorem EulerTransverseSourceCoefficientPath.sourceFrame_pullback_contDiff {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : EulerSmoothLimit.Space) (Rperp : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (L : P →L[ℝ] EulerSmoothLimit.Space) (A : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) : ContDiff ℝ ↑⊤ fun (x : P) => EulerTransverseSourceFrame.framePath m₀ Rperp T (pointPath A (L x))

The literal frame remains smooth after adjoining independent angle coordinates.

theorem EulerTransverseSourceCoefficientPath.sourceFrame_pullback_gevrey {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : EulerSmoothLimit.Space) (Rperp : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (L : P →L[ℝ] EulerSmoothLimit.Space) (hL : ‖L‖ ≤ 1) (A : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (d : ℕ) (hb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(A.field t)) x‖ ≤ C * EulerGevrey.majorant Rc d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => EulerTransverseSourceFrame.framePath m₀ Rperp T (pointPath A (L y))) x‖ ≤ C * EulerGevrey.majorant Rc d n

The actual source F Rperp coefficients satisfy the full joint parameter factorial bounds.