Polynomial source envelopes for all transverse inverse radius guards. The input inverse bound is derived from determinant-one deformation data; no inverse solver norm or forcing-dependent constant appears in the final radius.

def EulerPacketParentTransverseCosts.curvatureAmplitude (C C₂ : ℝ) : ℝ

Curvature amplitude, given by 27*C^2*C₂.

Equations

• EulerPacketParentTransverseCosts.curvatureAmplitude C C₂ = 27 * C ^ 2 * C₂

def EulerPacketParentTransverseCosts.historyCost (q : ℕ) (T R C C₁ C₂ : ℝ) : ℝ

History cost, constructed using inverseBlockCost.

Equations

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

def EulerPacketParentTransverseCosts.accelerationCost (q : ℕ) (R C C₁ V : ℝ) : ℝ

Acceleration cost, given by inverseBlockCost (Fin 4) q (gramInverseEnvelope C) R (3*C^2) (accelerationBlockAmplitude (Fin 4) q R C C₁ 1 V).

Equations

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

def EulerPacketParentTransverseCosts.inverseRadius (R C : ℝ) : ℝ

Inverse radius, given by 2*(1+gramInverseEnvelope C*(3*C^2+2))*(R+1).

Equations

• EulerPacketParentTransverseCosts.inverseRadius R C = 2 * (1 + EulerPacketParentMeanCoercivity.gramInverseEnvelope C * (3 * C ^ 2 + 2)) * (R + 1)

def EulerPacketParentTransverseCosts.forwardCost (q : ℕ) (S Ti R C C₁ Cp : ℝ) : ℝ

Forward cost, constructed using forwardSobolevCost.

Equations

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

def EulerPacketParentTransverseCosts.radius (q : ℕ) (T S Ti R C C₁ C₂ Cp : ℝ) : ℝ

Radius as an element of ℝ.

Equations

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

theorem EulerPacketParentTransverseCosts.inverseCost_le (T C C₁ c : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hc : 0 < c) (hi : c⁻¹ ≤ EulerPacketParentMeanCoercivity.gramInverseEnvelope C) : EulerTransverseGevreyInverse.inverseCost T C C₁ c ≤ EulerPacketParentMeanCoercivity.inverseEnvelope C C₁

theorem EulerPacketParentTransverseCosts.historyCost_nonneg (q : ℕ) (T R C C₁ C₂ : ℝ) (hT : 0 ≤ T) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) : 0 ≤ historyCost q T R C C₁ C₂

theorem EulerPacketParentTransverseCosts.accelerationCost_nonneg (q : ℕ) (R C C₁ V : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hV : 0 ≤ V) : 0 ≤ accelerationCost q R C C₁ V

theorem EulerPacketParentTransverseCosts.inverseRadius_nonneg (R C : ℝ) (hR : 0 ≤ R) : 0 ≤ inverseRadius R C

theorem EulerPacketParentTransverseCosts.forwardCost_nonneg (q : ℕ) (S Ti R C C₁ Cp : ℝ) (hS : 0 ≤ S) (hTi : 0 ≤ Ti) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hCp : 0 ≤ Cp) : 0 ≤ forwardCost q S Ti R C C₁ Cp

theorem EulerPacketParentTransverseCosts.historyCost_bound (q : ℕ) (T R C C₁ C₂ c : ℝ) (hT : 0 ≤ T) (hT1 : T ≤ 1) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) (hc : 0 < c) (hi : c⁻¹ ≤ EulerPacketParentMeanCoercivity.gramInverseEnvelope C) : EulerTransverseFixedSobolev.blockCost (Fin 4) q T R C C₁ (curvatureAmplitude C C₂) c 1 ≤ historyCost q T R C C₁ C₂

theorem EulerPacketParentTransverseCosts.accelerationCost_bound (q : ℕ) (R C C₁ c V W : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hc : 0 < c) (hi : c⁻¹ ≤ EulerPacketParentMeanCoercivity.gramInverseEnvelope C) (hV : 0 ≤ V) (hVW : V ≤ W) : EulerTimeLpGramSobolev.gramBlockCost (Fin 4) q c R C (EulerParameterWordGevrey.accelerationBlockAmplitude (Fin 4) q R C C₁ 1 V) ≤ accelerationCost q R C C₁ W

theorem EulerPacketParentTransverseCosts.inverseRadius_bound (R C c : ℝ) (hR : 0 ≤ R) (hi : c⁻¹ ≤ EulerPacketParentMeanCoercivity.gramInverseEnvelope C) : 2 * EulerTimeLpGramGevrey.gramCost c C 1 * (R + 1) ≤ inverseRadius R C

theorem EulerPacketParentTransverseCosts.traceCost_le (T Ti : ℝ) (hT : 0 < T) (hT1 : T ≤ 1) (hi : T⁻¹ ≤ Ti) : EulerFixedEvolutionSobolev.traceCost T ≤ Ti + 2

theorem EulerPacketParentTransverseCosts.forwardCost_bound (q : ℕ) (S Ti R C C₁ Cp V : ℝ) (hS : 0 ≤ S) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hCp : 0 ≤ Cp) (hV : V ≤ Ti + 2) : EulerLinearDuhamel.forwardSobolevCost (Fin 4) q S Cp V (EulerSourceCylinderForwardSobolev.forcingCost (Fin 4) q (inverseRadius R C) C) (18 * inverseRadius R C * C * C₁) (4 * inverseRadius R C) ≤ forwardCost q S Ti R C C₁ Cp

theorem EulerPacketParentTransverseCosts.radius_guards (q : ℕ) (T S Ti R C C₁ C₂ Cp : ℝ) (hT : 0 ≤ T) (hS : 0 ≤ S) (hTi : 0 ≤ Ti) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) (hCp : 0 ≤ Cp) : 2 * historyCost q T R C C₁ C₂ * (EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) R + 1) ≤ radius q T S Ti R C C₁ C₂ Cp ∧ 2 * accelerationCost q R C C₁ 1 * (EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) R + 1) ≤ radius q T S Ti R C C₁ C₂ Cp ∧ 2 * accelerationCost q R C C₁ (Ti + 2) * (EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) R + 1) ≤ radius q T S Ti R C C₁ C₂ Cp ∧ EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) (4 * inverseRadius R C) ≤ radius q T S Ti R C C₁ C₂ Cp ∧ 2 * forwardCost q S Ti R C C₁ Cp * (EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) (4 * inverseRadius R C) + 1) ≤ radius q T S Ti R C C₁ C₂ Cp