The explicit history perturbation estimate yields actual coefficient Lipschitz control.
theorem
EulerTransverseHistoryBounds.historyDifferenceCost_linear
(T c q q₁ d a r x y z : ℝ)
:
historyDifferenceCost T c q q₁ d a r x y z = historyDifferenceCost T c q q₁ d a r 1 0 0 * x + historyDifferenceCost T c q q₁ d a r 0 1 0 * y + historyDifferenceCost T c q q₁ d a r 0 0 1 * z
theorem
EulerTransverseHistoryBounds.historyVelocity_sub_norm_le_of_coefficient_bounds
{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)) (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)
(K : ℝ)
(hK : 0 ≤ K)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2)
(hsmall : K * (T ^ 2 / 2) ≤ 1 / 2)
(P P₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E))
(G : C(↑(Set.Icc 0 T), E →L[ℝ] E))
(hP : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(P t) v‖ ^ 2)
(hp : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT P) (P₁ t) (Set.Icc 0 T) ↑t)
(hG : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((G t) v) v ≤ K * ‖v‖ ^ 2)
(hTpos : 0 < T)
(q q₁ d a r : ℝ)
(hQn : ‖Q‖ ≤ q)
(hPn : ‖P‖ ≤ q)
(hQ₁n : ‖Q₁‖ ≤ q₁)
(hP₁n : ‖P₁‖ ≤ q₁)
(hD : T * ‖Q₁‖ + ‖Q‖ ≤ d)
(hD' : T * ‖P₁‖ + ‖P‖ ≤ d)
(hA : 1 + T ^ 2 * ‖H‖ ≤ a)
(hA' : 1 + T ^ 2 * ‖G‖ ≤ a)
(hr : EulerTimeH1FrameTransport.transportCost T Q Q₁ c ≤ r)
(hr' : EulerTimeH1FrameTransport.transportCost T P P₁ c ≤ r)
(L₀ L₁ LH s : ℝ)
(h₀ : ‖Q - P‖ ≤ L₀ * s)
(h₁ : ‖Q₁ - P₁‖ ≤ L₁ * s)
(hHdiff : ‖H - G‖ ≤ LH * s)
:
‖EulerTransverseEndpointCoordinates.historyVelocity T hT Q Q₁ H c hc hQ hd K hK hH hsmall - EulerTransverseEndpointCoordinates.historyVelocity T hT P P₁ G c hc hP hp K hK hG hsmall‖ ≤ historyDifferenceCost T c q q₁ d a r L₀ L₁ LH * s
The actual history operator inherits a Lipschitz estimate from the given coefficient paths, with an explicit polynomial coefficient.