Smooth dependence of the actual fixed-coordinate history

The coercive inverse, Gram inverse and fixed H¹ reconstruction are the actual ones used in the history solution. Smooth coefficient and forcing parameters therefore give smooth continuous-time coordinate and physical velocities.

theorem EulerTransverseFixedEvolution.velocityLp_contDiff {X : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : X → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : X → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : X) (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 : X) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) {n : WithTop ℕ∞} (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) (hH : ContDiff ℝ n H) (f : X → ↥(EulerTimeLp.TimeLp T E)) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : X) => (velocityLp T hT (Q x) (Q₁ x) (H x) c hc ⋯ ⋯ K hK ⋯ hsmall) (f x)

theorem EulerTransverseFixedEvolution.accelerationLp_contDiff {X : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : X → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : X → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : X) (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 : X) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) {n : WithTop ℕ∞} (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) (hH : ContDiff ℝ n H) (f : X → ↥(EulerTimeLp.TimeLp T E)) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : X) => (accelerationLp T hT (Q x) (Q₁ x) (H x) c hc ⋯ ⋯ K hK ⋯ hsmall) (f x)

theorem EulerTransverseFixedEvolution.velocityPath_contDiff {X : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : X → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : X → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : X) (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 : X) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) {n : WithTop ℕ∞} (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) (hH : ContDiff ℝ n H) (f : X → ↥(EulerTimeLp.TimeLp T E)) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : X) => (velocityPath T hT (Q x) (Q₁ x) (H x) c hc ⋯ ⋯ K hK ⋯ hsmall) (f x)

theorem EulerTransverseFixedEvolution.continuousVelocity_contDiff {X : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : X → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : X → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : X) (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 : X) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) {n : WithTop ℕ∞} (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) (hH : ContDiff ℝ n H) (f : X → C(↑(Set.Icc 0 T), E)) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : X) => (velocityPath T hT (Q x) (Q₁ x) (H x) c hc ⋯ ⋯ K hK ⋯ hsmall) (EulerTimeLp.pathLp T hT (f x))

theorem EulerTransverseFixedEvolution.classicalAcceleration_contDiff {X : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : X → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : X → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : X) (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 : X) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) {n : WithTop ℕ∞} (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) (hH : ContDiff ℝ n H) (f : X → C(↑(Set.Icc 0 T), E)) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : X) => classicalAcceleration T hT (Q x) (Q₁ x) (H x) c hc ⋯ ⋯ K hK ⋯ hsmall (f x)

theorem EulerTransverseFixedEvolution.physicalVelocity_contDiff {X : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : X → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : X → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : X) (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 : X) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) {n : WithTop ℕ∞} (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) (hH : ContDiff ℝ n H) (f : X → C(↑(Set.Icc 0 T), E)) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : X) => physicalVelocityPath T hT (Q x) (Q₁ x) (H x) c hc ⋯ ⋯ K hK ⋯ hsmall (f x)

theorem EulerTransverseFixedEvolution.physicalDerivative_contDiff {X : Type u_1} {U : Type u_2} {E : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : X → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : X → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : X) (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 : X) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) {n : WithTop ℕ∞} (hQ : ContDiff ℝ n Q) (hQ₁ : ContDiff ℝ n Q₁) (hH : ContDiff ℝ n H) (f : X → C(↑(Set.Icc 0 T), E)) (hf : ContDiff ℝ n f) : ContDiff ℝ n fun (x : X) => physicalDerivativePath T hT (Q x) (Q₁ x) (H x) c hc ⋯ ⋯ K hK ⋯ hsmall (f x)