The actual transverse inverse on a fixed Hilbert space

The domain is the kernel of the ordinary time initial-trace operator, independent of the spatial label, angle, or frame. The transported form and its actual coercive inverse are constructed here and identified with the original physical transverse solve. This is the fixed-space starting point for parameter estimates.

noncomputable def EulerTransverseFixedSpaceInverse.fixedFrameDerivative {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)) : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT) →L[ℝ] ↥(EulerTimeLp.TimeLp T E)

The actual physical derivative associated to a fixed zero-trace coordinate derivative.

Equations

• EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT Q Q₁ = EulerTimeH1OperatorProduct.productDerivative T hT Q Q₁ ∘SL (EulerTimeH1FrameTransport.zeroTraceDerivatives T hT).subtypeL

noncomputable def EulerTransverseFixedSpaceInverse.fixedFramePrimitive {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)) : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT) →L[ℝ] ↥(EulerTimeLp.TimeLp T E)

The actual physical displacement associated to a fixed coordinate derivative.

Equations

• EulerTransverseFixedSpaceInverse.fixedFramePrimitive T hT Q Q₁ = EulerTerminalTimePrimitive.primitiveTimeLp T hT ∘SL EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT Q Q₁

noncomputable def EulerTransverseFixedSpaceInverse.fixedFrameOperator {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)) : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT) →L[ℝ] ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT)

The transported Dirichlet operator on the fixed coordinate Hilbert space.

Equations

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

theorem EulerTransverseFixedSpaceInverse.fixedFrameOperator_inner {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)) (u v : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT)) : inner ℝ ((fixedFrameOperator T hT Q Q₁ H) u) v = inner ℝ ((fixedFrameDerivative T hT Q Q₁) u) ((fixedFrameDerivative T hT Q Q₁) v) - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((fixedFramePrimitive T hT Q Q₁) u)) ((fixedFramePrimitive T hT Q Q₁) v)

The transported operator has exactly the source displacement form.

noncomputable def EulerTransverseFixedSpaceInverse.fixedCoercivity {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 polynomial quantitative coercivity constant on the fixed coordinate space.

Equations

• EulerTransverseFixedSpaceInverse.fixedCoercivity T Q Q₁ c = (EulerTimeH1FrameTransport.transportCost T Q Q₁ c)⁻¹ ^ 2 / 2

theorem EulerTransverseFixedSpaceInverse.fixedCoercivity_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 < fixedCoercivity T Q Q₁ c

The transported coercivity constant is strictly positive.

theorem EulerTransverseFixedSpaceInverse.fixedFrameOperator_coercive {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)) (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) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x : E), inner ℝ ((H t) x) x ≤ K * ‖x‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (v : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT)) : fixedCoercivity T Q Q₁ c * ‖v‖ ^ 2 ≤ inner ℝ ((fixedFrameOperator T hT Q Q₁ H) v) v

The actual transported form is coercive, with a proved coefficient-only constant.

noncomputable def EulerTransverseFixedSpaceInverse.fixedFrameSolver {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)) (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) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x : E), inner ℝ ((H t) x) x ≤ K * ‖x‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT)

The genuine fixed-space inverse, constructed from the transported coercive form.

Equations

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

theorem EulerTransverseFixedSpaceInverse.fixedFrameSolver_weak {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)) (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) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x : E), inner ℝ ((H t) x) x ≤ K * ‖x‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T E)) (v : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT)) : have u := (fixedFrameSolver T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f; inner ℝ ((fixedFrameDerivative T hT Q Q₁) u) ((fixedFrameDerivative T hT Q Q₁) v) - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((fixedFramePrimitive T hT Q Q₁) u)) ((fixedFramePrimitive T hT Q Q₁) v) = -inner ℝ f ((fixedFramePrimitive T hT Q Q₁) v)

The actual fixed-space solution obeys the entire source variational form.

theorem EulerTransverseFixedSpaceInverse.fixedFrameSolver_unique {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)) (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) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x : E), inner ℝ ((H t) x) x ≤ K * ‖x‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T E)) (u : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT)) (hu : ∀ (v : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT)), inner ℝ ((fixedFrameDerivative T hT Q Q₁) u) ((fixedFrameDerivative T hT Q Q₁) v) - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((fixedFramePrimitive T hT Q Q₁) u)) ((fixedFramePrimitive T hT Q Q₁) v) = -inner ℝ f ((fixedFramePrimitive T hT Q Q₁) v)) : u = (fixedFrameSolver T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f

The fixed-space variational inverse is unique.

theorem EulerTransverseFixedSpaceInverse.fixedFrameSolver_eq_transverse {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)) (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) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x : E), inner ℝ ((H t) x) x ≤ K * ‖x‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (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 = η) (f : ↥(EulerTimeLp.TimeLp T E)) : (fixedFrameSolver T hT Q Q₁ H c hc hQ hd K hK hH hsmall) f = (EulerTimeH1FrameTransport.transverseBackward T hT Q Q₁ c hc hQ hd m) ((EulerTransverseVariationalInverse.transverseSolver T hT m H K hK hH hsmall) f)

The new fixed-space inverse is exactly the coordinates of the original physical transverse solve, rather than a separate unconnected construction.