Actual parameter regularity of the nonzero-terminal transverse inverse. The initial-zero energy and fixed-coordinate correction depend smoothly on the coefficient paths. An explicit affine coordinate trial implements the same terminal coordinate at neighboring labels.
The nonzero-terminal variational inverse on the same fixed coordinate Hilbert space used by the packet inverse. The zero-trace correction is an actual coercive solve. Full-range frame transport proves exact equality with the physical endpoint solution, rather than introducing a second unrelated solve.
theorem
EulerTransverseFixedEndpoint.fixedFrameDerivative_trace_zero
{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)
(v : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT))
:
(EulerTerminalTimePrimitive.initialTrace T hT) ((EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT Q Q₁) v) = 0
theorem
EulerTransverseFixedEndpoint.fixedFrame_energy
{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))
(hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t)
(u v : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT))
:
inner ℝ
((EulerTransverseEndpointEnergy.energyOperator T hT H)
((EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT Q Q₁) u))
((EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT Q Q₁) v) = inner ℝ ((EulerTransverseFixedSpaceInverse.fixedFrameOperator T hT Q Q₁ H) u) v
The fixed coordinate form is exactly the restriction of the physical initial-zero form.
noncomputable def
EulerTransverseFixedEndpoint.fixedEndpointCorrection
{U : Type u_1}
{E : Type u_2}
{V : Type u_3}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(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)
(L : V →L[ℝ] ↥(EulerTimeLp.TimeLp T E))
:
Fixed endpoint correction as an element of V →L[ℝ] zeroTraceDerivatives (U := U) T hT.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerTransverseFixedEndpoint.fixedEndpointDerivative
{U : Type u_1}
{E : Type u_2}
{V : Type u_3}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(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)
(L : V →L[ℝ] ↥(EulerTimeLp.TimeLp T E))
:
Fixed endpoint derivative, given by L - (fixedFrameDerivative T hT Q Q₁).comp (fixedEndpointCorrection T hT Q Q₁ H c hc hQ hd K hK hH hsmall L).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTransverseFixedEndpoint.fixedEndpointCorrection_equation
{U : Type u_1}
{E : Type u_2}
{V : Type u_3}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(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)
(L : V →L[ℝ] ↥(EulerTimeLp.TimeLp T E))
(Y : V)
(v : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT))
:
inner ℝ
((EulerTransverseEndpointEnergy.energyOperator T hT H)
((EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT Q Q₁)
((fixedEndpointCorrection T hT Q Q₁ H c hc hQ hd K hK hH hsmall L) Y)))
((EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT Q Q₁) v) = inner ℝ ((EulerTransverseEndpointEnergy.energyOperator T hT H) (L Y))
((EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT Q Q₁) v)
theorem
EulerTransverseFixedEndpoint.fixedEndpointDerivative_orthogonal
{U : Type u_1}
{E : Type u_2}
{V : Type u_3}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(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)
(L : V →L[ℝ] ↥(EulerTimeLp.TimeLp T E))
(Y : V)
(v : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT))
:
inner ℝ
((EulerTransverseEndpointEnergy.energyOperator T hT H)
((fixedEndpointDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall L) Y))
((EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT Q Q₁) v) = 0
theorem
EulerTransverseFixedEndpoint.fixedEndpointDerivative_sub_mem
{U : Type u_1}
{E : Type u_2}
{V : Type u_3}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(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)
(hm : ∀ (t : ↑(Set.Icc 0 T)) (x : U), inner ℝ (m t) ((Q t) x) = 0)
(L : V →L[ℝ] ↥(EulerTimeLp.TimeLp T E))
(Y : V)
:
(fixedEndpointDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall L) Y - L Y ∈ EulerTransverseVariationalInverse.transverseDerivatives T hT m
theorem
EulerTransverseFixedEndpoint.fixedEndpointDerivative_physical_orthogonal
{U : Type u_1}
{E : Type u_2}
{V : Type u_3}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(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)
(hm : ∀ (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 = η)
(L : V →L[ℝ] ↥(EulerTimeLp.TimeLp T E))
(Y : V)
(v : ↥(EulerTransverseVariationalInverse.transverseDerivatives T hT m))
:
inner ℝ
((EulerTransverseEndpointEnergy.energyOperator T hT H)
((fixedEndpointDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall L) Y))
↑v = 0
theorem
EulerTransverseFixedEndpoint.fixedEndpointDerivative_eq_endpoint
{U : Type u_1}
{E : Type u_2}
{V : Type u_3}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(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)
(hm : ∀ (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 = η)
(L : V →L[ℝ] ↥(EulerTimeLp.TimeLp T E))
:
fixedEndpointDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall L = EulerTransverseEndpointEnergy.endpointDerivative T hT m H K hK hH hsmall L
The fixed-space solve is the same nonzero-terminal inverse used by activation.
theorem
EulerTransverseEndpointParameter.contDiff_initialEnergy
{P : Type u_1}
{E : Type u_3}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(H : P → C(↑(Set.Icc 0 T), E →L[ℝ] E))
{n : WithTop ℕ∞}
(hH : ContDiff ℝ n H)
:
ContDiff ℝ n fun (x : P) => EulerTransverseEndpointEnergy.energyOperator T hT (H x)
theorem
EulerTransverseEndpointParameter.contDiff_initialProductDerivative
{P : Type u_1}
{U : Type u_2}
{E : Type u_3}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E))
{n : WithTop ℕ∞}
(hQ : ContDiff ℝ n Q)
(hQ₁ : ContDiff ℝ n Q₁)
:
ContDiff ℝ n fun (x : P) => EulerInitialTimePrimitive.initialProductDerivative T hT (Q x) (Q₁ x)
theorem
EulerTransverseEndpointParameter.contDiff_fixedEndpointCorrection
{P : Type u_1}
{U : Type u_2}
{E : Type u_3}
{V : Type u_4}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : P → C(↑(Set.Icc 0 T), E →L[ℝ] E))
{n : WithTop ℕ∞}
(c : ℝ)
(hc : 0 < c)
(hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2)
(hd :
∀ (x : P) (t : ↑(Set.Icc 0 T)),
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hPotential : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(hQ : ContDiff ℝ n Q)
(hQ₁ : ContDiff ℝ n Q₁)
(hH : ContDiff ℝ n H)
(L : P → V →L[ℝ] ↥(EulerTimeLp.TimeLp T E))
(hL : ContDiff ℝ n L)
:
ContDiff ℝ n fun (x : P) =>
EulerTransverseFixedEndpoint.fixedEndpointCorrection T hT (Q x) (Q₁ x) (H x) c hc ⋯ ⋯ K hK ⋯ hsmall (L x)
theorem
EulerTransverseEndpointParameter.contDiff_fixedEndpointDerivative
{P : Type u_1}
{U : Type u_2}
{E : Type u_3}
{V : Type u_4}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : P → C(↑(Set.Icc 0 T), E →L[ℝ] E))
{n : WithTop ℕ∞}
(c : ℝ)
(hc : 0 < c)
(hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2)
(hd :
∀ (x : P) (t : ↑(Set.Icc 0 T)),
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hPotential : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(hQ : ContDiff ℝ n Q)
(hQ₁ : ContDiff ℝ n Q₁)
(hH : ContDiff ℝ n H)
(L : P → V →L[ℝ] ↥(EulerTimeLp.TimeLp T E))
(hL : ContDiff ℝ n L)
:
ContDiff ℝ n fun (x : P) =>
EulerTransverseFixedEndpoint.fixedEndpointDerivative T hT (Q x) (Q₁ x) (H x) c hc ⋯ ⋯ K hK ⋯ hsmall (L x)
theorem
EulerTransverseEndpointParameter.contDiff_endpointDerivative
{P : Type u_1}
{U : Type u_2}
{E : Type u_3}
{V : Type u_4}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : P → C(↑(Set.Icc 0 T), E →L[ℝ] E))
{n : WithTop ℕ∞}
(c : ℝ)
(hc : 0 < c)
(hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2)
(hd :
∀ (x : P) (t : ↑(Set.Icc 0 T)),
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hPotential : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(hQ : ContDiff ℝ n Q)
(hQ₁ : ContDiff ℝ n Q₁)
(hH : ContDiff ℝ n H)
(L : P → V →L[ℝ] ↥(EulerTimeLp.TimeLp T E))
(hL : ContDiff ℝ n L)
(m : P → ↑(Set.Icc 0 T) → E)
(hm : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), inner ℝ (m x t) (((Q x) t) v) = 0)
(hRange : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m x t) η = 0 → ∃ (v : U), ((Q x) t) v = η)
:
ContDiff ℝ n fun (x : P) => EulerTransverseEndpointEnergy.endpointDerivative T hT (m x) (H x) K hK ⋯ hsmall (L x)
The physical endpoint solution inherits the proved parameter regularity.
noncomputable def
EulerTransverseEndpointParameter.affineTrial
{U : Type u_2}
{E : Type u_3}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
(T : ℝ)
(hT : 0 ≤ T)
(A A₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
:
The exact derivative of (t/T) Q(t) ξT.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTransverseEndpointParameter.affineTrial_primitive
{U : Type u_2}
{E : Type u_3}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(A A₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(hA : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (A₁ t) (Set.Icc 0 T) ↑t)
(ξT : U)
(t : ↑(Set.Icc 0 T))
:
((EulerInitialTimePrimitive.initialPrimitive T hT) ((affineTrial T hT A A₁) ξT)) t = (A t) ((↑t / T) • ξT)
theorem
EulerTransverseEndpointParameter.affineTrial_terminal
{U : Type u_2}
{E : Type u_3}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(A A₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(hTpos : 0 < T)
(hA : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (A₁ t) (Set.Icc 0 T) ↑t)
(ξT : U)
:
((EulerInitialTimePrimitive.initialPrimitive T hT) ((affineTrial T hT A A₁) ξT)) ⟨T, ⋯⟩ = (A ⟨T, ⋯⟩) ξT
theorem
EulerTransverseEndpointParameter.affineTrial_tangent
{U : Type u_2}
{E : Type u_3}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(A A₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(hA : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT A) (A₁ t) (Set.Icc 0 T) ↑t)
(m : ↑(Set.Icc 0 T) → E)
(hm : ∀ (t : ↑(Set.Icc 0 T)) (v : U), inner ℝ (m t) ((A t) v) = 0)
(ξT : U)
(t : ↑(Set.Icc 0 T))
:
inner ℝ (m t) (((EulerInitialTimePrimitive.initialPrimitive T hT) ((affineTrial T hT A A₁) ξT)) t) = 0
theorem
EulerTransverseEndpointParameter.contDiff_affineTrial
{P : Type u_1}
{U : Type u_2}
{E : Type u_3}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E))
{n : WithTop ℕ∞}
(hQ : ContDiff ℝ n Q)
(hQ₁ : ContDiff ℝ n Q₁)
:
ContDiff ℝ n fun (x : P) => affineTrial T hT (Q x) (Q₁ x)
theorem
EulerTransverseEndpointParameter.contDiff_affineEndpoint
{P : Type u_1}
{U : Type u_2}
{E : Type u_3}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
(T : ℝ)
(hT : 0 ≤ T)
(Q Q₁ : P → C(↑(Set.Icc 0 T), U →L[ℝ] E))
(H : P → C(↑(Set.Icc 0 T), E →L[ℝ] E))
{n : WithTop ℕ∞}
(c : ℝ)
(hc : 0 < c)
(hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2)
(hd :
∀ (x : P) (t : ↑(Set.Icc 0 T)),
HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t)
(K : ℝ)
(hK : 0 ≤ K)
(hPotential : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(hQ : ContDiff ℝ n Q)
(hQ₁ : ContDiff ℝ n Q₁)
(hH : ContDiff ℝ n H)
(m : P → ↑(Set.Icc 0 T) → E)
(hm : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), inner ℝ (m x t) (((Q x) t) v) = 0)
(hRange : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m x t) η = 0 → ∃ (v : U), ((Q x) t) v = η)
(ξT : U)
:
ContDiff ℝ n fun (x : P) =>
(EulerTransverseEndpointEnergy.endpointDerivative T hT (m x) (H x) K hK ⋯ hsmall (affineTrial T hT (Q x) (Q₁ x))) ξT
Neighboring labels use precisely the same terminal coordinate, and the resulting physical derivatives have the coefficient parameter regularity.