Continuous coordinate velocity of the actual fixed Dirichlet inverse

The acceleration is constructed by the true Gram inverse. The weak solve proves it is the derivative of the solved coordinate velocity; bounded H¹ reconstruction then supplies the actual continuous history path.

noncomputable def EulerTransverseFixedEvolution.velocityLp {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] ↥(EulerTimeLp.TimeLp T U)

Velocity Lᵖ, given by (zeroTraceDerivatives (U := U) T hT).subtypeL.comp (fixedFrameSolver T hT Q Q₁ H c hc hQ hd K hK hH hsmall).

Equations

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

noncomputable def EulerTransverseFixedEvolution.accelerationLp {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] ↥(EulerTimeLp.TimeLp T U)

Acceleration Lᵖ as an element of TimeLp T E →L[ℝ] TimeLp T U.

Equations

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

noncomputable def EulerTransverseFixedEvolution.velocityPath {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] C(↑(Set.Icc 0 T), U)

Velocity path as an element of TimeLp T E →L[ℝ] C(Icc (0 : ℝ) T,U).

Equations

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

theorem EulerTransverseFixedEvolution.velocityLp_zero_trace {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T E)) : (EulerTerminalTimePrimitive.initialTrace T hT) ((velocityLp T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f) = 0

theorem EulerTransverseFixedEvolution.accelerationLp_ae {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T E)) : ↑↑((accelerationLp T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => (EulerTransverseGramInverse.gramInverse (Q (Set.projIcc 0 T hT t)) c hc ⋯) ((ContinuousLinearMap.adjoint (Q (Set.projIcc 0 T hT t))) (↑↑f t - 2 • (Q₁ (Set.projIcc 0 T hT t)) (↑↑((velocityLp T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f) t)))

theorem EulerTransverseFixedEvolution.accelerationLp_equation {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T E)) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, (EulerTransverseGramInverse.gram (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑((accelerationLp T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f) t) = (ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑f t - 2 • (EulerVolterraConvolution.extendPath T hT Q₁ t) (↑↑((velocityLp T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f) t))

theorem EulerTransverseFixedEvolution.velocityLp_h1 {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t) (hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t) (hTpos : 0 < T) (f : ↥(EulerTimeLp.TimeLp T E)) : ∃ (v : ℝ → U), AbsolutelyContinuousOnInterval v 0 T ∧ ↑↑((velocityLp T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f) =ᵐ[EulerTimeLp.timeMeasure T] v ∧ ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt v (↑↑((accelerationLp T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f) t) t

theorem EulerTransverseFixedEvolution.velocityPath_eq {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (hTpos : 0 < T) (f : ↥(EulerTimeLp.TimeLp T E)) (v : ℝ → U) (hv : AbsolutelyContinuousOnInterval v 0 T) (hrep : ↑↑((velocityLp T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f) =ᵐ[EulerTimeLp.timeMeasure T] v) (hder : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt v (↑↑((accelerationLp T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f) t) t) (t : ↑(Set.Icc 0 T)) : ((velocityPath T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f) t = v ↑t

theorem EulerTransverseFixedEvolution.velocityPath_ae {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t) (hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t) (hTpos : 0 < T) (f : ↥(EulerTimeLp.TimeLp T E)) : ↑↑((velocityLp T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT ((velocityPath T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f)