Actual all-order parameter regularity of the transverse inverse

The fixed Hilbert-space operator is assembled from the prescribed coefficient paths and their true Bochner multipliers. Its coercive inverse is the previously constructed transverse solution. Smoothness of every finite order follows from coefficient smoothness; no regularity of a pre-existing inverse is assumed.

theorem EulerTransverseParameterRegularity.contDiff_adjoint {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {n : WithTop ℕ∞} {A : P → U →L[ℝ] E} (hA : ContDiff ℝ n A) : ContDiff ℝ n fun (x : P) => ContinuousLinearMap.adjoint (A x)

Adjoint regularity with both operator spaces fixed before composition.

theorem EulerTransverseParameterRegularity.contDiff_fixedFrameDerivative {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) {n : WithTop ℕ∞} (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) : ContDiff ℝ n fun (x : P) => EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT (Q x) (Q₁ x)

Parameter regularity of the actual H¹ physical derivative map.

theorem EulerTransverseParameterRegularity.contDiff_fixedFramePrimitive {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) {n : WithTop ℕ∞} (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) : ContDiff ℝ n fun (x : P) => EulerTransverseFixedSpaceInverse.fixedFramePrimitive T hT (Q x) (Q₁ x)

Parameter regularity of the actual physical displacement map.

theorem EulerTransverseParameterRegularity.contDiff_fixedFrameOperator {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) {n : WithTop ℕ∞} (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) (hH : ContDiff ℝ n H) : ContDiff ℝ n fun (x : P) => EulerTransverseFixedSpaceInverse.fixedFrameOperator T hT (Q x) (Q₁ x) (H x)

Parameter regularity of the genuine transported form on the fixed space.

theorem EulerTransverseParameterRegularity.contDiff_fixedFrameSolver {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) {n : WithTop ℕ∞} (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : P) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hPotential : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) (hH : ContDiff ℝ n H) : ContDiff ℝ n fun (x : P) => EulerTransverseFixedSpaceInverse.fixedFrameSolver T hT (Q x) (Q₁ x) (H x) c hc ⋯ ⋯ K hK ⋯ hsmall

The actual fixed-space forcing-to-solution operator has every prescribed order of coefficient regularity, including smoothness.

theorem EulerTransverseParameterRegularity.contDiff_fixedFrameSolution {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) {n : WithTop ℕ∞} (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : P) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hPotential : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) (hH : ContDiff ℝ n H) (f : P → ↥(EulerTimeLp.TimeLp T E)) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : P) => (EulerTransverseFixedSpaceInverse.fixedFrameSolver T hT (Q x) (Q₁ x) (H x) c hc ⋯ ⋯ K hK ⋯ hsmall) (f x)

Actual parameter regularity for a parameterized forcing.

theorem EulerTransverseParameterRegularity.contDiff_transverse_coordinates {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) {n : WithTop ℕ∞} (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : P) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hPotential : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (m : P → ↑(Set.Icc 0 T) → E) (hTangent : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), inner ℝ (m x t) (((Q x) t) v) = 0) (hRange : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m x t) η = 0 → ∃ (v : U), ((Q x) t) v = η) (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) (hH : ContDiff ℝ n H) (f : P → ↥(EulerTimeLp.TimeLp T E)) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : P) => EulerTransverseCoordinateRegularity.coordinateDerivative T hT (Q x) (Q₁ x) c hc ⋯ ↑((EulerTransverseVariationalInverse.transverseSolver T hT (m x) (H x) K hK ⋯ hsmall) (f x))

The coordinates of the original physical transverse solve inherit the proved parameter regularity through equality with the fixed-space inverse.

theorem EulerTransverseParameterRegularity.contDiff_transverse_velocity {P : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : P → C(↑(Set.Icc 0 T), E →L[ℝ] E)) {n : WithTop ℕ∞} (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : P) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hPotential : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (m : P → ↑(Set.Icc 0 T) → E) (hTangent : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), inner ℝ (m x t) (((Q x) t) v) = 0) (hRange : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m x t) η = 0 → ∃ (v : U), ((Q x) t) v = η) (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) (hH : ContDiff ℝ n H) (f : P → ↥(EulerTimeLp.TimeLp T E)) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : P) => (EulerTimeLp.timeMultiplier T hT (Q x)) (EulerTransverseCoordinateRegularity.coordinateDerivative T hT (Q x) (Q₁ x) c hc ⋯ ↑((EulerTransverseVariationalInverse.transverseSolver T hT (m x) (H x) K hK ⋯ hsmall) (f x)))

The physical velocity of the original constructed inverse has the actual parameter regularity of the prescribed frame and forcing.