A genuine mean-solver budget from parent deformation jets. All inverse costs and the final radius are explicit finite polynomials in those jets, the initial boundary size, and an upper bound for the inverse time length.

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

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

Equations

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

noncomputable def EulerPacketParentMeanBudget.operatorCost (q : ℕ) (T R C C₁ C₂ L : ℝ) : ℝ

Operator cost, given by operatorBlockAmplitude (Fin 4) q T R C C₁ (curvatureAmplitude C C₂) C₁ scaledBoundaryOperatorAmplitude L.

Equations

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

def EulerPacketParentMeanBudget.forcingCost (q : ℕ) (T R C C₁ : ℝ) : ℝ

Forcing cost, given by forcingBlockAmplitude (Fin 4) q T R C C₁ 1.

Equations

• EulerPacketParentMeanBudget.forcingCost q T R C C₁ = EulerMeanFixedSobolevGevrey.forcingBlockAmplitude (Fin 4) q T R C C₁ 1

noncomputable def EulerPacketParentMeanBudget.weakCost (q : ℕ) (T R C C₁ C₂ L : ℝ) : ℝ

Weak cost as an element of ℝ.

Equations

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

def EulerPacketParentMeanBudget.gramCost (q : ℕ) (R C C₁ V : ℝ) : ℝ

Gram 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.

noncomputable def EulerPacketParentMeanBudget.radius (q : ℕ) (T Ti R C C₁ C₂ L : ℝ) : ℝ

Radius, given by 1+2*(weakCost q T R C C₁ C₂ L+gramCost q R C C₁ 1+gramCost q R C C₁ (Ti+2)) * (sobolevCoefficientRadius (Fin 4) R+1).

Equations

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

theorem EulerPacketParentMeanBudget.operatorCost_nonneg (q : ℕ) (T R C C₁ C₂ L : ℝ) (hT : 0 ≤ T) (hR : 0 ≤ R) (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) : 0 ≤ operatorCost q T R C C₁ C₂ L

theorem EulerPacketParentMeanBudget.forcingCost_nonneg (q : ℕ) (T R C C₁ : ℝ) (hT : 0 ≤ T) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) : 0 ≤ forcingCost q T R C C₁

theorem EulerPacketParentMeanBudget.weakCost_one_le (q : ℕ) (T R C C₁ C₂ L : ℝ) (hT : 0 ≤ T) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) : 1 ≤ weakCost q T R C C₁ C₂ L

theorem EulerPacketParentMeanBudget.gramCost_nonneg (q : ℕ) (R C C₁ V : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hV : 0 ≤ V) : 0 ≤ gramCost q R C C₁ V

theorem EulerPacketParentMeanBudget.radius_guards (q : ℕ) (T Ti R C C₁ C₂ L : ℝ) (hT : 0 ≤ T) (hTi : 0 ≤ Ti) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) : 2 * weakCost q T R C C₁ C₂ L * (EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) R + 1) ≤ radius q T Ti R C C₁ C₂ L ∧ 2 * gramCost q R C C₁ 1 * (EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) R + 1) ≤ radius q T Ti R C C₁ C₂ L ∧ 2 * gramCost q R C C₁ (Ti + 2) * (EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) R + 1) ≤ radius q T Ti R C C₁ C₂ L

noncomputable def EulerPacketParentMeanBudget.sourceMeanBudget (D : EulerMeanPacketProvider.Data) (q : ℕ) (Ti R C C₁ C₂ : ℝ) (hT : D.T ≤ 1) (hTi : D.T⁻¹ ≤ Ti) (hR : 1024 ≤ R) (hC : 0 ≤ C) (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) (hF₂ : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F₂.field t)) x‖ ≤ C₂ * EulerGevrey.majorant R 0 n) : EulerMeanPacketProvider.Budget D q (radius q D.T Ti R C C₁ C₂ D.L)

Source mean budget as an element of EulerMeanPacketProvider.Budget D q (radius q D.T Ti R C C₁ C₂ D.L).

Equations

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