The actual left inverse of initial-zero moving-frame differentiation. This gives polynomial coordinate estimates for nonzero-terminal paths, including differences between frames, without estimating a forward evolution.

noncomputable def EulerTransverseInitialInverse.initialCoordinateOperator {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)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] ↥(EulerTimeLp.TimeLp T U)

Initial coordinate operator, given by initialProductDerivative T hT (frameLeftInversePath T Q c hc hQ) (frameLeftInverseDerivativePath T Q Q₁ c hc hQ).

Equations

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

theorem EulerTransverseInitialInverse.initialCoordinateOperator_apply {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)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (u : ↥(EulerTimeLp.TimeLp T E)) : (initialCoordinateOperator T hT Q Q₁ c hc hQ) u = EulerTransverseInitialCoordinates.initialCoordinateDerivative T hT Q Q₁ c hc hQ u

theorem EulerTransverseInitialInverse.initialCoordinates_product {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)) (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) (u : ↥(EulerTimeLp.TimeLp T U)) (t : ↑(Set.Icc 0 T)) : EulerTransverseInitialCoordinates.initialCoordinates T hT Q c hc hQ ((EulerInitialTimePrimitive.initialProductDerivative T hT Q Q₁) u) ↑t = EulerInitialTimePrimitive.initialRealPrimitive T u ↑t

theorem EulerTransverseInitialInverse.initialCoordinateOperator_product {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)) (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) (u : ↥(EulerTimeLp.TimeLp T U)) : (initialCoordinateOperator T hT Q Q₁ c hc hQ) ((EulerInitialTimePrimitive.initialProductDerivative T hT Q Q₁) u) = u

Differentiating the true initial primitive proves the left-inverse identity.

theorem EulerTransverseInitialInverse.initialCoordinateOperator_norm_le {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)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) : ‖initialCoordinateOperator T hT Q Q₁ c hc hQ‖ ≤ EulerTimeH1FrameTransport.transportCost T Q Q₁ c

theorem EulerTransverseInitialInverse.norm_le_initialProductDerivative {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)) (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) (u : ↥(EulerTimeLp.TimeLp T U)) : ‖u‖ ≤ EulerTimeH1FrameTransport.transportCost T Q Q₁ c * ‖(EulerInitialTimePrimitive.initialProductDerivative T hT Q Q₁) u‖

theorem EulerTransverseInitialInverse.norm_sub_le_initialProductDerivative {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)) (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) (P P₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (u v : ↥(EulerTimeLp.TimeLp T U)) : ‖u - v‖ ≤ EulerTimeH1FrameTransport.transportCost T Q Q₁ c * (‖(EulerInitialTimePrimitive.initialProductDerivative T hT Q Q₁) u - (EulerInitialTimePrimitive.initialProductDerivative T hT P P₁) v‖ + (T * ‖Q₁ - P₁‖ + ‖Q - P‖) * ‖v‖)

A difference of coordinate derivatives is bounded by the physical difference and the literal change of the frame coefficients.