Spatial intertwiners for the actual cylinder history #
These are consequences of the constructed variational inverse and Gram inverse. Subsequent support and translation lemmas discharge the displayed coefficient identities for their actual spatial maps.
Naturality of the genuine continuous Dirichlet velocity #
The constructed coordinate acceleration and its bounded H¹ reconstruction commute with the same spatial intertwiners as the variational inverse. This transports the actual continuous history path, including its endpoint values.
Naturality of the actual fixed-frame Dirichlet inverse #
Bounded spatial maps preserving the coefficients and their adjoint test maps commute with the constructed coercive solve. This covers translations and spatial support projections on actual L², not just pointwise model solutions.
noncomputable def
EulerFixedFrameNaturality.zeroTraceMap
{U : Type u_1}
{V : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
(T : ℝ)
(hT : 0 ≤ T)
(A : U →L[ℝ] V)
:
The genuine bounded spatial map on the fixed zero-trace derivative space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
EulerFixedFrameNaturality.zeroTraceMap_coe
{U : Type u_1}
{V : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
(T : ℝ)
(hT : 0 ≤ T)
(A : U →L[ℝ] V)
(u : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT))
:
theorem
EulerFixedFrameNaturality.zeroTraceMap_norm
{U : Type u_1}
{V : Type u_2}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
(T : ℝ)
(hT : 0 ≤ T)
(A : U →L[ℝ] V)
:
theorem
EulerFixedFrameNaturality.timeMultiplier_intertwines
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
(T : ℝ)
(hT : 0 ≤ T)
(A : U →L[ℝ] V)
(B : E →L[ℝ] F)
(Q : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(R : C(↑(Set.Icc 0 T), V →L[ℝ] F))
(hQR : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R t) (A u) = B ((Q t) u))
(u : ↥(EulerTimeLp.TimeLp T U))
:
(EulerTimeLp.timeMultiplier T hT R) ((EulerTimeLpBoundedMap.timeLift T A) u) = (EulerTimeLpBoundedMap.timeLift T B) ((EulerTimeLp.timeMultiplier T hT Q) u)
theorem
EulerFixedFrameNaturality.productDerivative_intertwines
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
(T : ℝ)
(hT : 0 ≤ T)
(A : U →L[ℝ] V)
(B : E →L[ℝ] F)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(R R₁ : C(↑(Set.Icc 0 T), V →L[ℝ] F))
(hQR : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R t) (A u) = B ((Q t) u))
(hQR₁ : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R₁ t) (A u) = B ((Q₁ t) u))
(u : ↥(EulerTimeLp.TimeLp T U))
:
(EulerTimeH1OperatorProduct.productDerivative T hT R R₁) ((EulerTimeLpBoundedMap.timeLift T A) u) = (EulerTimeLpBoundedMap.timeLift T B) ((EulerTimeH1OperatorProduct.productDerivative T hT Q Q₁) u)
theorem
EulerFixedFrameNaturality.fixedDerivative_intertwines
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
(T : ℝ)
(hT : 0 ≤ T)
(A : U →L[ℝ] V)
(B : E →L[ℝ] F)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(R R₁ : C(↑(Set.Icc 0 T), V →L[ℝ] F))
(hQR : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R t) (A u) = B ((Q t) u))
(hQR₁ : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R₁ t) (A u) = B ((Q₁ t) u))
(u : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT))
:
(EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT R R₁) ((zeroTraceMap T hT A) u) = (EulerTimeLpBoundedMap.timeLift T B) ((EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT Q Q₁) u)
theorem
EulerFixedFrameNaturality.fixedPrimitive_intertwines
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(T : ℝ)
(hT : 0 ≤ T)
(A : U →L[ℝ] V)
(B : E →L[ℝ] F)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(R R₁ : C(↑(Set.Icc 0 T), V →L[ℝ] F))
(hQR : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R t) (A u) = B ((Q t) u))
(hQR₁ : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R₁ t) (A u) = B ((Q₁ t) u))
(u : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT))
:
(EulerTransverseFixedSpaceInverse.fixedFramePrimitive T hT R R₁) ((zeroTraceMap T hT A) u) = (EulerTimeLpBoundedMap.timeLift T B) ((EulerTransverseFixedSpaceInverse.fixedFramePrimitive T hT Q Q₁) u)
theorem
EulerFixedFrameNaturality.fixedFrameSolver_intertwines
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(T : ℝ)
(hT : 0 ≤ T)
(A : U →L[ℝ] V)
(B : E →L[ℝ] F)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(R R₁ : C(↑(Set.Icc 0 T), V →L[ℝ] F))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(J : C(↑(Set.Icc 0 T), F →L[ℝ] F))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (u : U), c * ‖u‖ ^ 2 ≤ ‖(Q t) u‖ ^ 2)
(d : ℝ)
(hd : 0 < d)
(hR : ∀ (t : ↑(Set.Icc 0 T)) (v : V), d * ‖v‖ ^ 2 ≤ ‖(R t) v‖ ^ 2)
(hQtime : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(hRtime : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT R) (R₁ t) (Set.Icc 0 T) ↑t)
(K L : ℝ)
(hK : 0 ≤ K)
(hL : 0 ≤ L)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (u : E), inner ℝ ((H t) u) u ≤ K * ‖u‖ ^ 2)
(hJ : ∀ (t : ↑(Set.Icc 0 T)) (v : F), inner ℝ ((J t) v) v ≤ L * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(hsmall' : L * (T ^ 2 / 2) ≤ 1 / 2)
(hQR : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R t) (A u) = B ((Q t) u))
(hQR₁ : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R₁ t) (A u) = B ((Q₁ t) u))
(hRQ :
∀ (t : ↑(Set.Icc 0 T)) (v : V), (Q t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) ((R t) v))
(hRQ₁ :
∀ (t : ↑(Set.Icc 0 T)) (v : V),
(Q₁ t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) ((R₁ t) v))
(hHJ : ∀ (t : ↑(Set.Icc 0 T)) (u : E), (J t) (B u) = B ((H t) u))
(f : ↥(EulerTimeLp.TimeLp T E))
:
(zeroTraceMap T hT A)
((EulerTransverseFixedSpaceInverse.fixedFrameSolver T hT Q Q₁ H c hc hQ hQtime K hK hH hsmall) f) = (EulerTransverseFixedSpaceInverse.fixedFrameSolver T hT R R₁ J d hd hR hRtime L hL hJ hsmall')
((EulerTimeLpBoundedMap.timeLift T B) f)
A coefficient intertwiner and its adjoint preserve the actual variational solve, as follows by testing against the genuine pulled-back test field.
theorem
EulerFixedFrameNaturality.adjointMultiplier_intertwines
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(T : ℝ)
(hT : 0 ≤ T)
(A : U →L[ℝ] V)
(B : E →L[ℝ] F)
(Q : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(R : C(↑(Set.Icc 0 T), V →L[ℝ] F))
(hRQ :
∀ (t : ↑(Set.Icc 0 T)) (v : V), (Q t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) ((R t) v))
(f : ↥(EulerTimeLp.TimeLp T E))
:
(ContinuousLinearMap.adjoint (EulerTimeLp.timeMultiplier T hT R)) ((EulerTimeLpBoundedMap.timeLift T B) f) = (EulerTimeLpBoundedMap.timeLift T A) ((ContinuousLinearMap.adjoint (EulerTimeLp.timeMultiplier T hT Q)) f)
The backward test intertwiner gives the actual adjoint-multiplier identity.
theorem
EulerFixedFrameNaturality.gramOperator_intertwines
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(T : ℝ)
(hT : 0 ≤ T)
(A : U →L[ℝ] V)
(B : E →L[ℝ] F)
(Q : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(R : C(↑(Set.Icc 0 T), V →L[ℝ] F))
(hQR : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R t) (A u) = B ((Q t) u))
(hRQ :
∀ (t : ↑(Set.Icc 0 T)) (v : V), (Q t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) ((R t) v))
(u : ↥(EulerTimeLp.TimeLp T U))
:
(EulerTimeLpGramInverse.gramOperator T hT R) ((EulerTimeLpBoundedMap.timeLift T A) u) = (EulerTimeLpBoundedMap.timeLift T A) ((EulerTimeLpGramInverse.gramOperator T hT Q) u)
The true Gram operator commutes with compatible rectangular intertwiners.
theorem
EulerFixedFrameNaturality.gramSolver_intertwines
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(T : ℝ)
(hT : 0 ≤ T)
(A : U →L[ℝ] V)
(B : E →L[ℝ] F)
(Q : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(R : C(↑(Set.Icc 0 T), V →L[ℝ] F))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (u : U), c * ‖u‖ ^ 2 ≤ ‖(Q t) u‖ ^ 2)
(d : ℝ)
(hd : 0 < d)
(hR : ∀ (t : ↑(Set.Icc 0 T)) (v : V), d * ‖v‖ ^ 2 ≤ ‖(R t) v‖ ^ 2)
(hQR : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R t) (A u) = B ((Q t) u))
(hRQ :
∀ (t : ↑(Set.Icc 0 T)) (v : V), (Q t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) ((R t) v))
(f : ↥(EulerTimeLp.TimeLp T U))
:
(EulerTimeLpGramInverse.gramSolver T hT R d hd hR) ((EulerTimeLpBoundedMap.timeLift T A) f) = (EulerTimeLpBoundedMap.timeLift T A) ((EulerTimeLpGramInverse.gramSolver T hT Q c hc hQ) f)
The constructed Gram inverse inherits the intertwining identity by its two-sided inverse property.
theorem
EulerFixedFrameNaturality.velocityLp_intertwines
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(T : ℝ)
(hT : 0 ≤ T)
(A : U →L[ℝ] V)
(B : E →L[ℝ] F)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(R R₁ : C(↑(Set.Icc 0 T), V →L[ℝ] F))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(J : C(↑(Set.Icc 0 T), F →L[ℝ] F))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (u : U), c * ‖u‖ ^ 2 ≤ ‖(Q t) u‖ ^ 2)
(d : ℝ)
(hd : 0 < d)
(hR : ∀ (t : ↑(Set.Icc 0 T)) (v : V), d * ‖v‖ ^ 2 ≤ ‖(R t) v‖ ^ 2)
(hQtime : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(hRtime : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT R) (R₁ t) (Set.Icc 0 T) ↑t)
(K L : ℝ)
(hK : 0 ≤ K)
(hL : 0 ≤ L)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (u : E), inner ℝ ((H t) u) u ≤ K * ‖u‖ ^ 2)
(hJ : ∀ (t : ↑(Set.Icc 0 T)) (v : F), inner ℝ ((J t) v) v ≤ L * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(hsmall' : L * (T ^ 2 / 2) ≤ 1 / 2)
(hQR : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R t) (A u) = B ((Q t) u))
(hQR₁ : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R₁ t) (A u) = B ((Q₁ t) u))
(hRQ :
∀ (t : ↑(Set.Icc 0 T)) (v : V), (Q t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) ((R t) v))
(hRQ₁ :
∀ (t : ↑(Set.Icc 0 T)) (v : V),
(Q₁ t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) ((R₁ t) v))
(hHJ : ∀ (t : ↑(Set.Icc 0 T)) (u : E), (J t) (B u) = B ((H t) u))
(f : ↥(EulerTimeLp.TimeLp T E))
:
(EulerTransverseFixedEvolution.velocityLp T hT R R₁ J d hd hR hRtime L hL hJ hsmall')
((EulerTimeLpBoundedMap.timeLift T B) f) = (EulerTimeLpBoundedMap.timeLift T A)
((EulerTransverseFixedEvolution.velocityLp T hT Q Q₁ H c hc hQ hQtime K hK hH hsmall) f)
theorem
EulerFixedFrameNaturality.accelerationLp_intertwines
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(T : ℝ)
(hT : 0 ≤ T)
(A : U →L[ℝ] V)
(B : E →L[ℝ] F)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(R R₁ : C(↑(Set.Icc 0 T), V →L[ℝ] F))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(J : C(↑(Set.Icc 0 T), F →L[ℝ] F))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (u : U), c * ‖u‖ ^ 2 ≤ ‖(Q t) u‖ ^ 2)
(d : ℝ)
(hd : 0 < d)
(hR : ∀ (t : ↑(Set.Icc 0 T)) (v : V), d * ‖v‖ ^ 2 ≤ ‖(R t) v‖ ^ 2)
(hQtime : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(hRtime : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT R) (R₁ t) (Set.Icc 0 T) ↑t)
(K L : ℝ)
(hK : 0 ≤ K)
(hL : 0 ≤ L)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (u : E), inner ℝ ((H t) u) u ≤ K * ‖u‖ ^ 2)
(hJ : ∀ (t : ↑(Set.Icc 0 T)) (v : F), inner ℝ ((J t) v) v ≤ L * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(hsmall' : L * (T ^ 2 / 2) ≤ 1 / 2)
(hQR : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R t) (A u) = B ((Q t) u))
(hQR₁ : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R₁ t) (A u) = B ((Q₁ t) u))
(hRQ :
∀ (t : ↑(Set.Icc 0 T)) (v : V), (Q t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) ((R t) v))
(hRQ₁ :
∀ (t : ↑(Set.Icc 0 T)) (v : V),
(Q₁ t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) ((R₁ t) v))
(hHJ : ∀ (t : ↑(Set.Icc 0 T)) (u : E), (J t) (B u) = B ((H t) u))
(f : ↥(EulerTimeLp.TimeLp T E))
:
(EulerTransverseFixedEvolution.accelerationLp T hT R R₁ J d hd hR hRtime L hL hJ hsmall')
((EulerTimeLpBoundedMap.timeLift T B) f) = (EulerTimeLpBoundedMap.timeLift T A)
((EulerTransverseFixedEvolution.accelerationLp T hT Q Q₁ H c hc hQ hQtime K hK hH hsmall) f)
theorem
EulerFixedFrameNaturality.velocityPath_intertwines
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(T : ℝ)
(hT : 0 ≤ T)
(A : U →L[ℝ] V)
(B : E →L[ℝ] F)
(Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(R R₁ : C(↑(Set.Icc 0 T), V →L[ℝ] F))
(H : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(J : C(↑(Set.Icc 0 T), F →L[ℝ] F))
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (t : ↑(Set.Icc 0 T)) (u : U), c * ‖u‖ ^ 2 ≤ ‖(Q t) u‖ ^ 2)
(d : ℝ)
(hd : 0 < d)
(hR : ∀ (t : ↑(Set.Icc 0 T)) (v : V), d * ‖v‖ ^ 2 ≤ ‖(R t) v‖ ^ 2)
(hQtime : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(hRtime : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT R) (R₁ t) (Set.Icc 0 T) ↑t)
(K L : ℝ)
(hK : 0 ≤ K)
(hL : 0 ≤ L)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (u : E), inner ℝ ((H t) u) u ≤ K * ‖u‖ ^ 2)
(hJ : ∀ (t : ↑(Set.Icc 0 T)) (v : F), inner ℝ ((J t) v) v ≤ L * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(hsmall' : L * (T ^ 2 / 2) ≤ 1 / 2)
(hQR : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R t) (A u) = B ((Q t) u))
(hQR₁ : ∀ (t : ↑(Set.Icc 0 T)) (u : U), (R₁ t) (A u) = B ((Q₁ t) u))
(hRQ :
∀ (t : ↑(Set.Icc 0 T)) (v : V), (Q t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) ((R t) v))
(hRQ₁ :
∀ (t : ↑(Set.Icc 0 T)) (v : V),
(Q₁ t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) ((R₁ t) v))
(hHJ : ∀ (t : ↑(Set.Icc 0 T)) (u : E), (J t) (B u) = B ((H t) u))
(f : ↥(EulerTimeLp.TimeLp T E))
(t : ↑(Set.Icc 0 T))
:
((EulerTransverseFixedEvolution.velocityPath T hT R R₁ J d hd hR hRtime L hL hJ hsmall')
((EulerTimeLpBoundedMap.timeLift T B) f))
t = A (((EulerTransverseFixedEvolution.velocityPath T hT Q Q₁ H c hc hQ hQtime K hK hH hsmall) f) t)
The identity holds at every time, including the endpoint used by the subsequent forward solve.
Compatible spatial maps commute with the genuine positive Gram inverse.
theorem
EulerGramNaturality.adjoint_intertwines
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(A : U →L[ℝ] V)
(B : E →L[ℝ] F)
(Q : U →L[ℝ] E)
(R : V →L[ℝ] F)
(hback : ∀ (v : V), Q ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (R v))
(f : E)
:
theorem
EulerGramNaturality.gram_intertwines
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(A : U →L[ℝ] V)
(B : E →L[ℝ] F)
(Q : U →L[ℝ] E)
(R : V →L[ℝ] F)
(hforward : ∀ (u : U), R (A u) = B (Q u))
(hback : ∀ (v : V), Q ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (R v))
(u : U)
:
theorem
EulerGramNaturality.gramInverse_intertwines
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(A : U →L[ℝ] V)
(B : E →L[ℝ] F)
(Q : U →L[ℝ] E)
(R : V →L[ℝ] F)
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (u : U), c * ‖u‖ ^ 2 ≤ ‖Q u‖ ^ 2)
(d : ℝ)
(hd : 0 < d)
(hR : ∀ (v : V), d * ‖v‖ ^ 2 ≤ ‖R v‖ ^ 2)
(hforward : ∀ (u : U), R (A u) = B (Q u))
(hback : ∀ (v : V), Q ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (R v))
(f : U)
:
(EulerTransverseGramInverse.gramInverse R d hd hR) (A f) = A ((EulerTransverseGramInverse.gramInverse Q c hc hQ) f)
theorem
EulerGramNaturality.acceleration_intertwines
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(A : U →L[ℝ] V)
(B : E →L[ℝ] F)
(Q Q₁ : U →L[ℝ] E)
(R R₁ : V →L[ℝ] F)
(c : ℝ)
(hc : 0 < c)
(hQ : ∀ (u : U), c * ‖u‖ ^ 2 ≤ ‖Q u‖ ^ 2)
(d : ℝ)
(hd : 0 < d)
(hR : ∀ (v : V), d * ‖v‖ ^ 2 ≤ ‖R v‖ ^ 2)
(hforward : ∀ (u : U), R (A u) = B (Q u))
(hforward₁ : ∀ (u : U), R₁ (A u) = B (Q₁ u))
(hback : ∀ (v : V), Q ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (R v))
(f : E)
(v : U)
:
(EulerTransverseGramInverse.gramInverse R d hd hR) ((ContinuousLinearMap.adjoint R) (B f - 2 • R₁ (A v))) = A ((EulerTransverseGramInverse.gramInverse Q c hc hQ) ((ContinuousLinearMap.adjoint Q) (f - 2 • Q₁ v)))
In particular the actual acceleration formula respects a compatible coordinate map and physical map.
theorem
EulerCylinderDirichlet.Coefficients.velocityLp_intertwines
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(D : Coefficients T U E)
(G : Coefficients T V F)
(A : ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P V))
(B : ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P F))
(hQ :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)),
((frame P G) t) (A u) = B (((frame P D) t) u))
(hQ₁ :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)),
((frameDerivative P G) t) (A u) = B (((frameDerivative P D) t) u))
(hback :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)),
((frame P D) t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (((frame P G) t) v))
(hback₁ :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)),
((frameDerivative P D) t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (((frameDerivative P G) t) v))
(hH :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P E)),
((hessian P G) t) (B u) = B (((hessian P D) t) u))
(f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
:
(velocityLp P G) ((EulerTimeLpBoundedMap.timeLift T B) f) = (EulerTimeLpBoundedMap.timeLift T A) ((velocityLp P D) f)
theorem
EulerCylinderDirichlet.Coefficients.accelerationLp_intertwines
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(D : Coefficients T U E)
(G : Coefficients T V F)
(A : ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P V))
(B : ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P F))
(hQ :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)),
((frame P G) t) (A u) = B (((frame P D) t) u))
(hQ₁ :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)),
((frameDerivative P G) t) (A u) = B (((frameDerivative P D) t) u))
(hback :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)),
((frame P D) t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (((frame P G) t) v))
(hback₁ :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)),
((frameDerivative P D) t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (((frameDerivative P G) t) v))
(hH :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P E)),
((hessian P G) t) (B u) = B (((hessian P D) t) u))
(f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
:
(accelerationLp P G) ((EulerTimeLpBoundedMap.timeLift T B) f) = (EulerTimeLpBoundedMap.timeLift T A) ((accelerationLp P D) f)
theorem
EulerCylinderDirichlet.Coefficients.velocityPath_intertwines
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(D : Coefficients T U E)
(G : Coefficients T V F)
(A : ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P V))
(B : ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P F))
(hQ :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)),
((frame P G) t) (A u) = B (((frame P D) t) u))
(hQ₁ :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)),
((frameDerivative P G) t) (A u) = B (((frameDerivative P D) t) u))
(hback :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)),
((frame P D) t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (((frame P G) t) v))
(hback₁ :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)),
((frameDerivative P D) t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (((frameDerivative P G) t) v))
(hH :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P E)),
((hessian P G) t) (B u) = B (((hessian P D) t) u))
(f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(t : ↑(Set.Icc 0 T))
:
theorem
EulerCylinderDirichlet.Coefficients.continuousVelocity_intertwines
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(D : Coefficients T U E)
(G : Coefficients T V F)
(A : ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P V))
(B : ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P F))
(hQ :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)),
((frame P G) t) (A u) = B (((frame P D) t) u))
(hQ₁ :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)),
((frameDerivative P G) t) (A u) = B (((frameDerivative P D) t) u))
(hback :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)),
((frame P D) t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (((frame P G) t) v))
(hback₁ :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)),
((frameDerivative P D) t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (((frameDerivative P G) t) v))
(hH :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P E)),
((hessian P G) t) (B u) = B (((hessian P D) t) u))
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(t : ↑(Set.Icc 0 T))
:
((velocityPath P G) (EulerTimeLp.pathLp T ⋯ ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) B) f))) t = A (((velocityPath P D) (EulerTimeLp.pathLp T ⋯ f)) t)
theorem
EulerCylinderDirichlet.Coefficients.accelerationPath_intertwines
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(D : Coefficients T U E)
(G : Coefficients T V F)
(A : ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P V))
(B : ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P F))
(hQ :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)),
((frame P G) t) (A u) = B (((frame P D) t) u))
(hQ₁ :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)),
((frameDerivative P G) t) (A u) = B (((frameDerivative P D) t) u))
(hback :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)),
((frame P D) t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (((frame P G) t) v))
(hback₁ :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)),
((frameDerivative P D) t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (((frameDerivative P G) t) v))
(hH :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P E)),
((hessian P G) t) (B u) = B (((hessian P D) t) u))
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(t : ↑(Set.Icc 0 T))
:
(accelerationPath P G ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) B) f)) t = A ((accelerationPath P D f) t)
theorem
EulerCylinderDirichlet.Coefficients.physicalVelocity_intertwines
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(D : Coefficients T U E)
(G : Coefficients T V F)
(A : ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P V))
(B : ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P F))
(hQ :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)),
((frame P G) t) (A u) = B (((frame P D) t) u))
(hQ₁ :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)),
((frameDerivative P G) t) (A u) = B (((frameDerivative P D) t) u))
(hback :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)),
((frame P D) t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (((frame P G) t) v))
(hback₁ :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)),
((frameDerivative P D) t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (((frameDerivative P G) t) v))
(hH :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P E)),
((hessian P G) t) (B u) = B (((hessian P D) t) u))
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(t : ↑(Set.Icc 0 T))
:
(physicalVelocity P G ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) B) f)) t = B ((physicalVelocity P D f) t)
theorem
EulerCylinderDirichlet.Coefficients.physicalDerivative_intertwines
(P : ℝ)
[Fact (0 < P)]
{T : ℝ}
{U : Type u_1}
{V : Type u_2}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
[CompleteSpace V]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[CompleteSpace F]
(D : Coefficients T U E)
(G : Coefficients T V F)
(A : ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P V))
(B : ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P F))
(hQ :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)),
((frame P G) t) (A u) = B (((frame P D) t) u))
(hQ₁ :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)),
((frameDerivative P G) t) (A u) = B (((frameDerivative P D) t) u))
(hback :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)),
((frame P D) t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (((frame P G) t) v))
(hback₁ :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLpCylinderTranslation.CylinderL2 P V)),
((frameDerivative P D) t) ((ContinuousLinearMap.adjoint A) v) = (ContinuousLinearMap.adjoint B) (((frameDerivative P G) t) v))
(hH :
∀ (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P E)),
((hessian P G) t) (B u) = B (((hessian P D) t) u))
(f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E)))
(t : ↑(Set.Icc 0 T))
:
(physicalDerivative P G ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) B) f)) t = B ((physicalDerivative P D f) t)