Actual moving-frame coordinates for initial-zero H¹ paths with arbitrary terminal value. The coordinate derivative is constructed in Bochner L². The physical reconstruction and its differentiated identity follow from the coefficient left inverse, the H¹ product rule and uniqueness of derivatives.
noncomputable def
EulerTransverseInitialCoordinates.initialCoordinates
{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 : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(u : ↥(EulerTimeLp.TimeLp T E))
(t : ℝ)
:
U
Initial coordinates, given by extendPath T hT (frameLeftInversePath T Q c hc hQ) t (initialRealPrimitive T u t).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerTransverseInitialCoordinates.initialCoordinateField
{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 : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(u : ↥(EulerTimeLp.TimeLp T E))
:
↥(EulerTimeLp.TimeLp T U)
Initial coordinate field, given by timeMultiplier T hT (frameLeftInversePath T Q c hc hQ) (initialPrimitiveTimeLp T hT u).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerTransverseInitialCoordinates.initialCoordinateDerivative
{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))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(u : ↥(EulerTimeLp.TimeLp T E))
:
↥(EulerTimeLp.TimeLp T U)
Initial coordinate derivative, constructed using fieldProductDerivative.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTransverseInitialCoordinates.initialCoordinates_initial
{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 : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(u : ↥(EulerTimeLp.TimeLp T E))
:
theorem
EulerTransverseInitialCoordinates.initialCoordinateField_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 : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(u : ↥(EulerTimeLp.TimeLp T E))
:
↑↑(initialCoordinateField T hT Q c hc hQ u) =ᵐ[EulerTimeLp.timeMeasure T] initialCoordinates T hT Q c hc hQ u
theorem
EulerTransverseInitialCoordinates.initialCoordinates_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))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(u : ↥(EulerTimeLp.TimeLp T E))
:
AbsolutelyContinuousOnInterval (initialCoordinates T hT Q c hc hQ u) 0 T ∧ ↑↑(initialCoordinateField T hT Q c hc hQ u) =ᵐ[EulerTimeLp.timeMeasure T] initialCoordinates T hT Q c hc hQ u ∧ ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (initialCoordinates T hT Q c hc hQ u) (↑↑(initialCoordinateDerivative T hT Q Q₁ c hc hQ u) t) t
theorem
EulerTransverseInitialCoordinates.initialCoordinates_reconstruct
{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 : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(u : ↥(EulerTimeLp.TimeLp T E))
(huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerInitialTimePrimitive.initialRealPrimitive T u ↑t)
(t : ↑(Set.Icc 0 T))
:
(Q t) (initialCoordinates T hT Q c hc hQ u ↑t) = EulerInitialTimePrimitive.initialRealPrimitive T u ↑t
The constructed coordinates reconstruct the actual nonzero-terminal path.
theorem
EulerTransverseInitialCoordinates.initialCoordinateDerivative_reconstruct_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))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2)
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(u : ↥(EulerTimeLp.TimeLp T E))
(huRange : ∀ (t : ↑(Set.Icc 0 T)), ∃ (x : U), (Q t) x = EulerInitialTimePrimitive.initialRealPrimitive T u ↑t)
:
∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, ↑↑u t = (EulerVolterraConvolution.extendPath T hT Q₁ t) (initialCoordinates T hT Q c hc hQ u t) + (EulerVolterraConvolution.extendPath T hT Q t) (↑↑(initialCoordinateDerivative T hT Q Q₁ c hc hQ u) t)
Differentiating reconstruction gives the literal physical velocity a.e.