Transport of actual H¹ derivative spaces by a moving frame

The forward map is the actual derivative of Q(t) Jv(t). Its left inverse is the actual derivative after applying the constructed Gram left inverse. This places parameter-dependent transverse variational problems on one fixed Hilbert space before coefficient differentiation or all-order estimates.

theorem EulerTimeH1FrameTransport.coordinateDerivative_productDerivative {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) (v : ↥(EulerTimeLp.TimeLp T U)) : EulerTransverseCoordinateRegularity.coordinateDerivative T hT Q Q₁ c hc hQ ((EulerTimeH1OperatorProduct.productDerivative T hT Q Q₁) v) = v

Differentiating the constructed left inverse recovers every coordinate H¹ derivative. No initial condition is needed for this transport identity.

noncomputable def EulerTimeH1FrameTransport.transportCost {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) : ℝ

A strictly positive polynomial transport cost from the inverse-frame bounds.

Equations

• EulerTimeH1FrameTransport.transportCost T Q Q₁ c = 1 + ((2 * c⁻¹ ^ 2 * ‖Q‖ ^ 2 * ‖Q₁‖ + c⁻¹ * ‖Q₁‖) * T + c⁻¹ * ‖Q‖)

theorem EulerTimeH1FrameTransport.transportCost_pos {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) : 0 < transportCost T Q Q₁ c

The transport cost is positive even in a degenerate zero-dimensional space.

theorem EulerTimeH1FrameTransport.norm_le_transportCost_productDerivative {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) (v : ↥(EulerTimeLp.TimeLp T U)) : ‖v‖ ≤ transportCost T Q Q₁ c * ‖(EulerTimeH1OperatorProduct.productDerivative T hT Q Q₁) v‖

The coordinate derivative norm is bounded by the physical derivative norm.

theorem EulerTimeH1FrameTransport.productDerivative_norm_sq_lower {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) (v : ↥(EulerTimeLp.TimeLp T U)) : (transportCost T Q Q₁ c)⁻¹ ^ 2 * ‖v‖ ^ 2 ≤ ‖(EulerTimeH1OperatorProduct.productDerivative T hT Q Q₁) v‖ ^ 2

A quantitative lower bound for the transported kinetic energy.

noncomputable def EulerTimeH1FrameTransport.zeroTraceDerivatives {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) : Submodule ℝ ↥(EulerTimeLp.TimeLp T U)

The fixed Hilbert space of coordinate derivatives with zero initial trace. Terminal zero is already supplied by the primitive.

Equations

• EulerTimeH1FrameTransport.zeroTraceDerivatives T hT = (↑(EulerTerminalTimePrimitive.initialTrace T hT)).ker

instance EulerTimeH1FrameTransport.zeroTraceDerivatives_complete {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (T : ℝ) (hT : 0 ≤ T) : CompleteSpace ↥(zeroTraceDerivatives T hT)

The fixed zero-trace coordinate space is complete.

noncomputable def EulerTimeH1FrameTransport.transverseForward {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)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (m : ↑(Set.Icc 0 T) → E) (hTangent : ∀ (t : ↑(Set.Icc 0 T)) (x : U), inner ℝ (m t) ((Q t) x) = 0) : ↥(zeroTraceDerivatives T hT) →L[ℝ] ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m)

Actual differentiation transports the fixed coordinate space to the physical zero-endpoint moving-plane space.

Equations

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

noncomputable def EulerTimeH1FrameTransport.transverseBackward {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) (m : ↑(Set.Icc 0 T) → E) : ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m) →L[ℝ] ↥(zeroTraceDerivatives T hT)

Applying the constructed inverse-frame derivative transports back to the same fixed coordinate space.

Equations

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

theorem EulerTimeH1FrameTransport.transverseBackward_forward {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) (m : ↑(Set.Icc 0 T) → E) (hTangent : ∀ (t : ↑(Set.Icc 0 T)) (x : U), inner ℝ (m t) ((Q t) x) = 0) (v : ↥(zeroTraceDerivatives T hT)) : (transverseBackward T hT Q Q₁ c hc hQ hd m) ((transverseForward T hT Q Q₁ hd m hTangent) v) = v

The backward transport is the actual inverse on every fixed coordinate derivative.

theorem EulerTimeH1FrameTransport.transverseForward_backward {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) (m : ↑(Set.Icc 0 T) → E) (hTangent : ∀ (t : ↑(Set.Icc 0 T)) (x : U), inner ℝ (m t) ((Q t) x) = 0) (hRange : ∀ (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m t) η = 0 → ∃ (x : U), (Q t) x = η) (u : ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m)) : (transverseForward T hT Q Q₁ hd m hTangent) ((transverseBackward T hT Q Q₁ c hc hQ hd m) u) = u

The forward transport recovers every physical transverse derivative.

noncomputable def EulerTimeH1FrameTransport.transverseEquiv {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) (m : ↑(Set.Icc 0 T) → E) (hTangent : ∀ (t : ↑(Set.Icc 0 T)) (x : U), inner ℝ (m t) ((Q t) x) = 0) (hRange : ∀ (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m t) η = 0 → ∃ (x : U), (Q t) x = η) : ↥(zeroTraceDerivatives T hT) ≃L[ℝ] ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m)

A proved bounded linear equivalence to a parameter-independent Hilbert space.

Equations

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