Polynomial uniform-time bounds and neighboring-label estimates for the actual primary history. The terminal coordinate is the same at both labels. historyVelocity_eq identifies the bounded path here with the genuine coordinate velocity of the stationary endpoint solution.

Quantitative operator algebra for the actual fixed-space endpoint solve. The input called R below is an inverse operator; the transverse specialization constructs it by coercivity and discharges all of its norm bounds.

theorem EulerCoerciveEndpointBounds.norm_adjoint_sub {S : Type u_1} {E : Type u_2} [NormedAddCommGroup S] [InnerProductSpace ℝ S] [CompleteSpace S] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (A B : S →L[ℝ] E) : ‖ContinuousLinearMap.adjoint A - ContinuousLinearMap.adjoint B‖ = ‖A - B‖

Taking adjoints preserves the norm of an operator difference.

theorem EulerCoerciveEndpointBounds.norm_comp_sub_le {F : Type u_4} {G : Type u_5} {W : Type u_6} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup W] [NormedSpace ℝ W] (A B : F →L[ℝ] G) (C D : W →L[ℝ] F) : ‖A ∘SL C - B ∘SL D‖ ≤ ‖A - B‖ * ‖C‖ + ‖B‖ * ‖C - D‖

noncomputable def EulerCoerciveEndpointBounds.correctionOperator {S : Type u_1} {E : Type u_2} [NormedAddCommGroup S] [InnerProductSpace ℝ S] [CompleteSpace S] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : S →L[ℝ] E) (R : S →L[ℝ] S) (A : E →L[ℝ] E) : E →L[ℝ] E

The actual algebraic stationary correction in a fixed coordinate space.

Equations

• EulerCoerciveEndpointBounds.correctionOperator D R A = D ∘SL R ∘SL ContinuousLinearMap.adjoint D ∘SL A

noncomputable def EulerCoerciveEndpointBounds.endpointOperator {S : Type u_1} {E : Type u_2} {V : Type u_3} [NormedAddCommGroup S] [InnerProductSpace ℝ S] [CompleteSpace S] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup V] [NormedSpace ℝ V] (D : S →L[ℝ] E) (R : S →L[ℝ] S) (A : E →L[ℝ] E) (L : V →L[ℝ] E) : V →L[ℝ] E

Endpoint operator, given by L - (correctionOperator D R A).comp L.

Equations

• EulerCoerciveEndpointBounds.endpointOperator D R A L = L - EulerCoerciveEndpointBounds.correctionOperator D R A ∘SL L

theorem EulerCoerciveEndpointBounds.correctionOperator_norm_le {S : Type u_1} {E : Type u_2} [NormedAddCommGroup S] [InnerProductSpace ℝ S] [CompleteSpace S] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : S →L[ℝ] E) (R : S →L[ℝ] S) (A : E →L[ℝ] E) (d r a : ℝ) (hd : ‖D‖ ≤ d) (hr : ‖R‖ ≤ r) (ha : ‖A‖ ≤ a) : ‖correctionOperator D R A‖ ≤ d ^ 2 * r * a

theorem EulerCoerciveEndpointBounds.correctionOperator_sub_norm_le {S : Type u_1} {E : Type u_2} [NormedAddCommGroup S] [InnerProductSpace ℝ S] [CompleteSpace S] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D D' : S →L[ℝ] E) (R R' : S →L[ℝ] S) (A A' : E →L[ℝ] E) (d r a δd δr δa : ℝ) (hd : ‖D‖ ≤ d) (hd' : ‖D'‖ ≤ d) (hr : ‖R‖ ≤ r) (hr' : ‖R'‖ ≤ r) (ha : ‖A‖ ≤ a) (_ha' : ‖A'‖ ≤ a) (hδd : ‖D - D'‖ ≤ δd) (hδr : ‖R - R'‖ ≤ δr) (hδa : ‖A - A'‖ ≤ δa) : ‖correctionOperator D R A - correctionOperator D' R' A'‖ ≤ 2 * d * r * a * δd + d ^ 2 * a * δr + d ^ 2 * r * δa

theorem EulerCoerciveEndpointBounds.endpointOperator_norm_le {S : Type u_1} {E : Type u_2} {V : Type u_3} [NormedAddCommGroup S] [InnerProductSpace ℝ S] [CompleteSpace S] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup V] [NormedSpace ℝ V] (D : S →L[ℝ] E) (R : S →L[ℝ] S) (A : E →L[ℝ] E) (L : V →L[ℝ] E) (d r a l : ℝ) (hd : ‖D‖ ≤ d) (hr : ‖R‖ ≤ r) (ha : ‖A‖ ≤ a) (hl : ‖L‖ ≤ l) : ‖endpointOperator D R A L‖ ≤ (1 + d ^ 2 * r * a) * l

theorem EulerCoerciveEndpointBounds.endpointOperator_sub_norm_le {S : Type u_1} {E : Type u_2} {V : Type u_3} [NormedAddCommGroup S] [InnerProductSpace ℝ S] [CompleteSpace S] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup V] [NormedSpace ℝ V] (D D' : S →L[ℝ] E) (R R' : S →L[ℝ] S) (A A' : E →L[ℝ] E) (L L' : V →L[ℝ] E) (d r a l δd δr δa δl : ℝ) (hd : ‖D‖ ≤ d) (hd' : ‖D'‖ ≤ d) (hr : ‖R‖ ≤ r) (hr' : ‖R'‖ ≤ r) (ha : ‖A‖ ≤ a) (ha' : ‖A'‖ ≤ a) (hl : ‖L‖ ≤ l) (hδd : ‖D - D'‖ ≤ δd) (hδr : ‖R - R'‖ ≤ δr) (hδa : ‖A - A'‖ ≤ δa) (hδl : ‖L - L'‖ ≤ δl) : ‖endpointOperator D R A L - endpointOperator D' R' A' L'‖ ≤ (1 + d ^ 2 * r * a) * δl + (2 * d * r * a * δd + d ^ 2 * a * δr + d ^ 2 * r * δa) * l

noncomputable def EulerCoerciveEndpointBounds.formOperator {S : Type u_1} {E : Type u_2} [NormedAddCommGroup S] [InnerProductSpace ℝ S] [CompleteSpace S] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D : S →L[ℝ] E) (A : E →L[ℝ] E) : S →L[ℝ] S

The transported quadratic form used by the fixed-coordinate inverse.

Equations

• EulerCoerciveEndpointBounds.formOperator D A = ContinuousLinearMap.adjoint D ∘SL A ∘SL D

theorem EulerCoerciveEndpointBounds.formOperator_sub_norm_le {S : Type u_1} {E : Type u_2} [NormedAddCommGroup S] [InnerProductSpace ℝ S] [CompleteSpace S] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (D D' : S →L[ℝ] E) (A A' : E →L[ℝ] E) (d a δd δa : ℝ) (hd : ‖D‖ ≤ d) (hd' : ‖D'‖ ≤ d) (ha : ‖A‖ ≤ a) (ha' : ‖A'‖ ≤ a) (hδd : ‖D - D'‖ ≤ δd) (hδa : ‖A - A'‖ ≤ δa) : ‖formOperator D A - formOperator D' A'‖ ≤ 2 * d * a * δd + d ^ 2 * δa

The neighboring-label estimate for the actual nonzero-terminal inverse. The inverse is the same coercive inverse as the packet construction. All constants below bound coefficients or their explicit frame-transport cost; no bound on an unknown inverse or on a supplied solution is assumed.

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

An abbreviation of the actual fixed-coordinate inverse, with its proved coercivity.

Equations

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

theorem EulerTransverseEndpointDifference.fixedInverse_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)) (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) (r : ℝ) (hr : EulerTimeH1FrameTransport.transportCost T Q Q₁ c ≤ r) : ‖fixedInverse T hT Q Q₁ H c hc hQ hd K hK hH hsmall‖ ≤ 2 * r ^ 2

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

The literal coefficient distance for differentiating moving-frame paths.

Equations

• EulerTransverseEndpointDifference.derivativeDistance T Q Q₁ P P₁ = T * ‖Q₁ - P₁‖ + ‖Q - P‖

theorem EulerTransverseEndpointDifference.derivativeDistance_nonneg {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ P P₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : 0 ≤ derivativeDistance T Q Q₁ P P₁

theorem EulerTransverseEndpointDifference.fixedFrameOperator_sub_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)) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (P P₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (G : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (d a : ℝ) (hD : T * ‖Q₁‖ + ‖Q‖ ≤ d) (hD' : T * ‖P₁‖ + ‖P‖ ≤ d) (hA : 1 + T ^ 2 * ‖H‖ ≤ a) (hA' : 1 + T ^ 2 * ‖G‖ ≤ a) : ‖EulerTransverseFixedSpaceInverse.fixedFrameOperator T hT Q Q₁ H - EulerTransverseFixedSpaceInverse.fixedFrameOperator T hT P P₁ G‖ ≤ 2 * d * a * derivativeDistance T Q Q₁ P P₁ + d ^ 2 * (T ^ 2 * ‖H - G‖)

theorem EulerTransverseEndpointDifference.fixedInverse_sub_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)) (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) (d a r : ℝ) (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) : ‖fixedInverse T hT Q Q₁ H c hc hQ hd K hK hH hsmall - fixedInverse T hT P P₁ G c hc hP hp K hK hG hsmall‖ ≤ (2 * r ^ 2) ^ 2 * (2 * d * a * derivativeDistance T Q Q₁ P P₁ + d ^ 2 * (T ^ 2 * ‖H - G‖))

def EulerTransverseEndpointDifference.endpointDifferenceCost (d i a δd δa : ℝ) : ℝ

The polynomial sensitivity of an affine terminal-coordinate solve.

Equations

• EulerTransverseEndpointDifference.endpointDifferenceCost d i a δd δa = (1 + 3 * d ^ 2 * i * a + 2 * d ^ 4 * i ^ 2 * a ^ 2) * δd + (d ^ 3 * i + d ^ 5 * i ^ 2 * a) * δa

theorem EulerTransverseEndpointDifference.fixedAffineEndpoint_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)) (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) (d a r : ℝ) (hD : T * ‖Q₁‖ + ‖Q‖ ≤ d) (hA : 1 + T ^ 2 * ‖H‖ ≤ a) (hr : EulerTimeH1FrameTransport.transportCost T Q Q₁ c ≤ r) : ‖EulerTransverseFixedEndpoint.fixedEndpointDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall (EulerTransverseEndpointParameter.affineTrial T hT Q Q₁)‖ ≤ (1 + d ^ 2 * (2 * r ^ 2) * a) * (EulerTransverseEndpointBounds.affineCost T * d)

theorem EulerTransverseEndpointDifference.fixedAffineEndpoint_sub_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)) (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) (d a r : ℝ) (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) : ‖EulerTransverseFixedEndpoint.fixedEndpointDerivative T hT Q Q₁ H c hc hQ hd K hK hH hsmall (EulerTransverseEndpointParameter.affineTrial T hT Q Q₁) - EulerTransverseFixedEndpoint.fixedEndpointDerivative T hT P P₁ G c hc hP hp K hK hG hsmall (EulerTransverseEndpointParameter.affineTrial T hT P P₁)‖ ≤ EulerTransverseEndpointBounds.affineCost T * endpointDifferenceCost d (2 * r ^ 2) a (derivativeDistance T Q Q₁ P P₁) (T ^ 2 * ‖H - G‖)

theorem EulerTransverseEndpointDifference.affineEndpoint_sub_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)) (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) (m n : ↑(Set.Icc 0 T) → E) (hm : ∀ (t : ↑(Set.Icc 0 T)) (v : U), inner ℝ (m t) ((Q t) v) = 0) (hn : ∀ (t : ↑(Set.Icc 0 T)) (v : U), inner ℝ (n t) ((P t) v) = 0) (hRange : ∀ (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m t) η = 0 → ∃ (v : U), (Q t) v = η) (hRange' : ∀ (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (n t) η = 0 → ∃ (v : U), (P t) v = η) (d a r : ℝ) (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) : ‖EulerTransverseEndpointEnergy.endpointDerivative T hT m H K hK hH hsmall (EulerTransverseEndpointParameter.affineTrial T hT Q Q₁) - EulerTransverseEndpointEnergy.endpointDerivative T hT n G K hK hG hsmall (EulerTransverseEndpointParameter.affineTrial T hT P P₁)‖ ≤ EulerTransverseEndpointBounds.affineCost T * endpointDifferenceCost d (2 * r ^ 2) a (derivativeDistance T Q Q₁ P P₁) (T ^ 2 * ‖H - G‖)

A genuine neighboring-label bound on the physical endpoint solutions.

Polynomial size and coefficient sensitivity of the actual source (10) generator.

theorem EulerTransverseGeneratorDifference.gram_sub_norm_le {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (A B : U →L[ℝ] E) (q : ℝ) (hA : ‖A‖ ≤ q) (hB : ‖B‖ ≤ q) : ‖EulerTransverseGramInverse.gram A - EulerTransverseGramInverse.gram B‖ ≤ 2 * q * ‖A - B‖

theorem EulerTransverseGeneratorDifference.gramInverse_sub_norm_le {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (A B : U →L[ℝ] E) (c : ℝ) (hc : 0 < c) (hA : ∀ (u : U), c * ‖u‖ ^ 2 ≤ ‖A u‖ ^ 2) (hB : ∀ (u : U), c * ‖u‖ ^ 2 ≤ ‖B u‖ ^ 2) (q : ℝ) (hAn : ‖A‖ ≤ q) (hBn : ‖B‖ ≤ q) : ‖EulerTransverseGramInverse.gramInverse A c hc hA - EulerTransverseGramInverse.gramInverse B c hc hB‖ ≤ 2 * c⁻¹ ^ 2 * q * ‖A - B‖

theorem EulerTransverseGeneratorDifference.generator_norm_le {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (u : U), c * ‖u‖ ^ 2 ≤ ‖(Q t) u‖ ^ 2) (q r : ℝ) (hQn : ‖Q‖ ≤ q) (hQ₁n : ‖Q₁‖ ≤ r) : ‖EulerTransverseForwardInverse.generator T Q Q₁ c hc hQ‖ ≤ 2 * c⁻¹ * q * r

noncomputable def EulerTransverseGeneratorDifference.generatorDifferenceCost (c q r δq δr : ℝ) : ℝ

Only frame differences occur in the genuine generator difference.

Equations

• EulerTransverseGeneratorDifference.generatorDifferenceCost c q r δq δr = (4 * c⁻¹ ^ 2 * q ^ 2 * r + 2 * c⁻¹ * r) * δq + 2 * c⁻¹ * q * δr

theorem EulerTransverseGeneratorDifference.generator_sub_norm_le {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q Q₁ P P₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (u : U), c * ‖u‖ ^ 2 ≤ ‖(Q t) u‖ ^ 2) (hP : ∀ (t : ↑(Set.Icc 0 T)) (u : U), c * ‖u‖ ^ 2 ≤ ‖(P t) u‖ ^ 2) (q r : ℝ) (hQn : ‖Q‖ ≤ q) (hPn : ‖P‖ ≤ q) (hQ₁n : ‖Q₁‖ ≤ r) (_hP₁n : ‖P₁‖ ≤ r) : ‖EulerTransverseForwardInverse.generator T Q Q₁ c hc hQ - EulerTransverseForwardInverse.generator T P P₁ c hc hP‖ ≤ generatorDifferenceCost c q r ‖Q - P‖ ‖Q₁ - P₁‖

Uniform-time polynomial bounds from an actual L² value and generator derivative.

noncomputable def EulerTimeH1GeneratorBounds.generatorTrace {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (B : C(↑(Set.Icc 0 T), U →L[ℝ] U)) : ↥(EulerTimeLp.TimeLp T U) →L[ℝ] C(↑(Set.Icc 0 T), U)

Reconstruct from the L² value and its prescribed generator derivative.

Equations

• EulerTimeH1GeneratorBounds.generatorTrace T hT B = EulerTimeH1Reconstruction.valuePart T hT + EulerTimeH1Reconstruction.derivativePart T hT ∘SL EulerTimeLp.timeMultiplier T hT B

noncomputable def EulerTimeH1GeneratorBounds.traceCost (T b : ℝ) : ℝ

Trace cost, given by (1+T) * (T⁻¹ + 2*b).

Equations

• EulerTimeH1GeneratorBounds.traceCost T b = (1 + T) * (T⁻¹ + 2 * b)

theorem EulerTimeH1GeneratorBounds.sqrt_le_one_add (T : ℝ) (hT : 0 ≤ T) : √T ≤ 1 + T

theorem EulerTimeH1GeneratorBounds.generatorTrace_norm_le {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (hTpos : 0 < T) (B : C(↑(Set.Icc 0 T), U →L[ℝ] U)) (b : ℝ) (hB : ‖B‖ ≤ b) : ‖generatorTrace T hT B‖ ≤ traceCost T b

theorem EulerTimeH1GeneratorBounds.generatorTrace_sub_norm_le {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (hTpos : 0 < T) (B B' : C(↑(Set.Icc 0 T), U →L[ℝ] U)) : ‖generatorTrace T hT B - generatorTrace T hT B'‖ ≤ 2 * (1 + T) * ‖B - B'‖

theorem EulerTimeH1GeneratorBounds.continuousMultiplier_sub_norm_le {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (Q P : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : ‖EulerContinuousTimeIntegral.multiplier Q - EulerContinuousTimeIntegral.multiplier P‖ ≤ ‖Q - P‖

theorem EulerTimeH1GeneratorBounds.transportedTrace_norm_le {U : Type u_1} {E : Type u_2} {V : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (hTpos : 0 < T) (Q : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (B : C(↑(Set.Icc 0 T), U →L[ℝ] U)) (S : V →L[ℝ] ↥(EulerTimeLp.TimeLp T U)) (q b s : ℝ) (hQ : ‖Q‖ ≤ q) (hB : ‖B‖ ≤ b) (hS : ‖S‖ ≤ s) : ‖EulerContinuousTimeIntegral.multiplier Q ∘SL generatorTrace T hT B ∘SL S‖ ≤ q * traceCost T b * s

theorem EulerTimeH1GeneratorBounds.transportedTrace_sub_norm_le {U : Type u_1} {E : Type u_2} {V : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (hTpos : 0 < T) (Q P : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (B B' : C(↑(Set.Icc 0 T), U →L[ℝ] U)) (S S' : V →L[ℝ] ↥(EulerTimeLp.TimeLp T U)) (q b s δq δb δs : ℝ) (hP : ‖P‖ ≤ q) (hB : ‖B‖ ≤ b) (hB' : ‖B'‖ ≤ b) (hS : ‖S‖ ≤ s) (hδq : ‖Q - P‖ ≤ δq) (hδb : ‖B - B'‖ ≤ δb) (hδs : ‖S - S'‖ ≤ δs) : ‖EulerContinuousTimeIntegral.multiplier Q ∘SL generatorTrace T hT B ∘SL S - EulerContinuousTimeIntegral.multiplier P ∘SL generatorTrace T hT B' ∘SL S'‖ ≤ δq * traceCost T b * s + q * (2 * (1 + T) * δb * s + traceCost T b * δs)

noncomputable def EulerTransverseHistoryBounds.slopeCost (T d a r : ℝ) : ℝ

Slope cost, given by r * (1+d^2*(2*r^2)*a) * (affineCost T*d).

Equations

• EulerTransverseHistoryBounds.slopeCost T d a r = r * (1 + d ^ 2 * (2 * r ^ 2) * a) * (EulerTransverseEndpointBounds.affineCost T * d)

noncomputable def EulerTransverseHistoryBounds.slopeDifferenceCost (T d a r δd δa : ℝ) : ℝ

Slope difference cost, given by r * (affineCost T * endpointDifferenceCost d (2*r^2) a δd δa + δd * slopeCost T d a r).

Equations

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

theorem EulerTransverseHistoryBounds.coordinateSlope_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)) (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) (d a r : ℝ) (hD : T * ‖Q₁‖ + ‖Q‖ ≤ d) (hA : 1 + T ^ 2 * ‖H‖ ≤ a) (hr : EulerTimeH1FrameTransport.transportCost T Q Q₁ c ≤ r) : ‖EulerTransverseEndpointCoordinates.coordinateSlope T hT Q Q₁ H c hc hQ hd K hK hH hsmall‖ ≤ slopeCost T d a r

theorem EulerTransverseHistoryBounds.coordinateSlope_sub_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)) (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) (d a r : ℝ) (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) : ‖EulerTransverseEndpointCoordinates.coordinateSlope T hT Q Q₁ H c hc hQ hd K hK hH hsmall - EulerTransverseEndpointCoordinates.coordinateSlope T hT P P₁ G c hc hP hp K hK hG hsmall‖ ≤ slopeDifferenceCost T d a r (EulerTransverseEndpointDifference.derivativeDistance T Q Q₁ P P₁) (T ^ 2 * ‖H - G‖)

noncomputable def EulerTransverseHistoryBounds.historyCost (T c q q₁ d a r : ℝ) : ℝ

History cost, given by q * traceCost T (2*c⁻¹*q*q₁) * slopeCost T d a r.

Equations

• EulerTransverseHistoryBounds.historyCost T c q q₁ d a r = q * EulerTimeH1GeneratorBounds.traceCost T (2 * c⁻¹ * q * q₁) * EulerTransverseHistoryBounds.slopeCost T d a r

noncomputable def EulerTransverseHistoryBounds.historyDifferenceCost (T c q q₁ d a r δq δq₁ δH : ℝ) : ℝ

History difference cost, constructed using δq.

Equations

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

theorem EulerTransverseHistoryBounds.historyVelocity_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)) (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) (hTpos : 0 < T) (q q₁ d a r : ℝ) (hQn : ‖Q‖ ≤ q) (hQ₁n : ‖Q₁‖ ≤ q₁) (hD : T * ‖Q₁‖ + ‖Q‖ ≤ d) (hA : 1 + T ^ 2 * ‖H‖ ≤ a) (hr : EulerTimeH1FrameTransport.transportCost T Q Q₁ c ≤ r) : ‖EulerTransverseEndpointCoordinates.historyVelocity T hT Q Q₁ H c hc hQ hd K hK hH hsmall‖ ≤ historyCost T c q q₁ d a r

theorem EulerTransverseHistoryBounds.historyVelocity_sub_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)) (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) : ‖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 ‖Q - P‖ ‖Q₁ - P₁‖ ‖H - G‖

The primary history has a polynomial, uniform-in-time coefficient sensitivity. In particular coefficient Lipschitz bounds give the source's physical-label Lipschitz bound with the same fixed terminal coordinate.