The normal/pressure/corrector budget follows from the actual deformation and its first time derivative. Its radius is an explicit polynomial in their Gevrey radius and amplitudes; no inverse or strain jet bound is an input.

def EulerPacketParentNormalBudget.amplitude (C C₁ : ℝ) : ℝ

Amplitude, given by 9*C^2+27*C^2*C₁.

Equations

• EulerPacketParentNormalBudget.amplitude C C₁ = 9 * C ^ 2 + 27 * C ^ 2 * C₁

def EulerPacketParentNormalBudget.inverseRadius (R C C₁ : ℝ) : ℝ

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

Equations

• EulerPacketParentNormalBudget.inverseRadius R C C₁ = 2 * (1 + (1 + C) ^ 2 * (3 * EulerPacketParentNormalBudget.amplitude C C₁ ^ 2 + 2)) * (R + 1)

def EulerPacketParentNormalBudget.radius (R C C₁ : ℝ) : ℝ

Radius, given by 16*(R+4*inverseRadius R C C₁+1).

Equations

• EulerPacketParentNormalBudget.radius R C C₁ = 16 * (R + 4 * EulerPacketParentNormalBudget.inverseRadius R C C₁ + 1)

theorem EulerPacketParentNormalBudget.amplitude_nonneg (C C₁ : ℝ) (hC₁ : 0 ≤ C₁) : 0 ≤ amplitude C C₁

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

theorem EulerPacketParentNormalBudget.radius_nonneg (R C C₁ : ℝ) (hR : 0 ≤ R) : 0 ≤ radius R C C₁

theorem EulerPacketParentNormalBudget.inverse_guard {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R C C₁ : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) : 2 * EulerTimeLpGramGevrey.gramCost D.normalLower (amplitude C C₁) 1 * (R + 1) ≤ inverseRadius R C C₁

def EulerPacketParentNormalBudget.sourceNormalBudget {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R C C₁ : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (hF₁ : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant R 0 n) (q : ℕ) : EulerTransversePacketJoin.NormalBudget D q (radius R C C₁)

Source normal budget, bundling Rc, C, Ri, Rc_nonneg and the required compatibility proofs.

Equations

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