Quantitative bounds for the actual transverse coordinate inverse

These bounds use the lower frame constant and coefficient norms. In particular no exponential dependence on the undifferentiated coefficient norm is introduced.

theorem EulerTransverseStrongEstimates.gramInversePath_norm {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (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) : ‖EulerTransverseGramPath.gramInversePath T Q c hc hQ‖ ≤ c⁻¹

The genuine inverse coefficient has the uniform coercive inverse bound.

theorem EulerTransverseStrongEstimates.gramDerivativePath_norm {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)) : ‖EulerTransverseGramPath.gramDerivativePath T Q Q₁‖ ≤ 2 * ‖Q‖ * ‖Q₁‖

The Gram derivative is controlled by the actual frame and frame derivative norms.

theorem EulerTransverseStrongEstimates.gramInverseDerivativePath_norm {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) : ‖EulerTransverseGramPath.gramInverseDerivativePath T Q Q₁ c hc hQ‖ ≤ 2 * c⁻¹ ^ 2 * ‖Q‖ * ‖Q₁‖

The derivative of the inverse pays two inverse factors and one coefficient derivative.

theorem EulerTransverseStrongEstimates.frameLeftInversePath_norm {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (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) : ‖EulerTransverseGramPath.frameLeftInversePath T Q c hc hQ‖ ≤ c⁻¹ * ‖Q‖

Recovering coordinates has one inverse factor.

theorem EulerTransverseStrongEstimates.frameLeftInverseDerivativePath_norm {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) : ‖EulerTransverseGramPath.frameLeftInverseDerivativePath T Q Q₁ c hc hQ‖ ≤ 2 * c⁻¹ ^ 2 * ‖Q‖ ^ 2 * ‖Q₁‖ + c⁻¹ * ‖Q₁‖

Differentiating coordinate recovery has polynomial coefficient cost.

theorem EulerTransverseStrongEstimates.coordinateDerivative_norm {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (hT : 0 ≤ T) (u : ↥(EulerTimeLp.TimeLp T E)) : ‖EulerTransverseCoordinateRegularity.coordinateDerivative T hT Q Q₁ c hc hQ u‖ ≤ ((2 * c⁻¹ ^ 2 * ‖Q‖ ^ 2 * ‖Q₁‖ + c⁻¹ * ‖Q₁‖) * T + c⁻¹ * ‖Q‖) * ‖u‖

Explicit polynomial bound for the actual coordinate derivative.

theorem EulerTransverseStrongEstimates.transverseCoordinateDerivative_norm {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (hT : 0 ≤ T) (m : ↑(Set.Icc 0 T) → E) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (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)) : ‖EulerTransverseCoordinateRegularity.coordinateDerivative T hT Q Q₁ c hc hQ ↑((EulerTransverseVariationalInverse.transverseSolver T hT m H K hK hH hsmall) f)‖ ≤ ((2 * c⁻¹ ^ 2 * ‖Q‖ ^ 2 * ‖Q₁‖ + c⁻¹ * ‖Q₁‖) * T + c⁻¹ * ‖Q‖) * (2 * T * ‖f‖)

The actual coercive forcing-to-coordinate-velocity map has a polynomial bound.

theorem EulerTransverseStrongEstimates.acceleration_eq_inverse {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (hT : 0 ≤ T) (v a : ↥(EulerTimeLp.TimeLp T U)) (f : ↥(EulerTimeLp.TimeLp T E)) (heq : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, (EulerTransverseGramInverse.gram (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑a t) = (ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑f t - 2 • (EulerVolterraConvolution.extendPath T hT Q₁ t) (↑↑v t))) : a = (EulerTimeLp.timeMultiplier T hT (EulerTransverseGramPath.gramInversePath T Q c hc hQ)) ((ContinuousLinearMap.adjoint (EulerTimeLp.timeMultiplier T hT Q)) (f - 2 • (EulerTimeLp.timeMultiplier T hT Q₁) v))

Inverting the projected strong equation is an exact equality of actual L² fields.

theorem EulerTransverseStrongEstimates.acceleration_norm {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (hT : 0 ≤ T) (v a : ↥(EulerTimeLp.TimeLp T U)) (f : ↥(EulerTimeLp.TimeLp T E)) (heq : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, (EulerTransverseGramInverse.gram (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑a t) = (ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT Q t)) (↑↑f t - 2 • (EulerVolterraConvolution.extendPath T hT Q₁ t) (↑↑v t))) : ‖a‖ ≤ c⁻¹ * ‖Q‖ * (‖f‖ + 2 * ‖Q₁‖ * ‖v‖)

The strong acceleration bound pays one inverse Gram factor and no derivative of the Hessian or extra undifferentiated time-growth factor.

theorem EulerTransverseStrongEstimates.transverseCoordinateSecondDerivative_norm {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)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hT : 0 < T) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ Q) (Q₁ t) (Set.Icc 0 T) ↑t) (hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ Q₁) (Q₂ t) (Set.Icc 0 T) ↑t) (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 = η) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (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) (hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t) (f : ↥(EulerTimeLp.TimeLp T E)) : have u := ↑((EulerTransverseVariationalInverse.transverseSolver T ⋯ m H K hK hH hsmall) f); ‖EulerTransverseStrongEquation.coordinateSecondDerivative T ⋯ Q Q₁ Q₂ c hc hQ H u f‖ ≤ c⁻¹ * ‖Q‖ * (‖f‖ + 2 * ‖Q₁‖ * ‖EulerTransverseCoordinateRegularity.coordinateDerivative T ⋯ Q Q₁ c hc hQ u‖)

Applying the strong bound to the actual variational solver gives a polynomial acceleration estimate in terms of its already bounded coordinate velocity.