Actual finite correction families and input comparison bounds, independent of any Gevrey radius-loss budget.

def EulerCorrectionAssembly.stabilityBudgetOfBase (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (K : EulerCorrectionEnergyData.MetricBudget period T ⋯ (EulerAllOrderCorrectionData.Data.atOrder period A 1)) (R : C(↑(Set.Icc 0 T), ℝ)) (S : EulerCorrectionEnergyData.SpatialBudget period stabilityBudgetOfBase._proof_1 (EulerAllOrderCorrectionData.Data.atOrder period A 8) 2 R) (q : ℕ) : EulerCorrectionStabilityBudget.StabilityBudget period ⋯ (EulerAllOrderCorrectionData.Data.atOrder period A q)

One genuine inverse metric and actual base coefficient bounds provide stability at every finite Sobolev order. No shrinking-radius condition or smallness of the approximate velocity is required.

Equations

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

structure EulerCorrectionAssembly.ComparisonData (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) : Type

Genuine input bounds sufficient to compare any finite solutions of the same prescribed data. This contains no correction, compatibility, solution-energy or radius-loss assumption.

• metric : EulerCorrectionEnergyData.MetricBudget period T ⋯ (EulerAllOrderCorrectionData.Data.atOrder period A 1)

  The actual common inverse metric and its time derivative.

• radius : C(↑(Set.Icc 0 T), ℝ)

  A radius used solely to state the actual base coefficient bounds.

• spatial : EulerCorrectionEnergyData.SpatialBudget period stabilityBudgetOfBase._proof_1 (EulerAllOrderCorrectionData.Data.atOrder period A 8) 2 self.radius

  Genuine base-order spatial bounds; their background bounds need not be small.

• divergence (t : ↑(Set.Icc 0 T)) : A.approximation.field t ∈ EulerLiftedGradientSpace.divergenceFreeSpace period A.κ A.direction

  The prescribed approximate solution obeys the actual lifted divergence constraint.

def EulerCorrectionAssembly.ComparisonData.stabilityBudget (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (C : ComparisonData period hT A) (q : ℕ) : EulerCorrectionStabilityBudget.StabilityBudget period ⋯ (EulerAllOrderCorrectionData.Data.atOrder period A q)

The supplied genuine comparison data construct a stability budget at any order.

Equations

• EulerCorrectionAssembly.ComparisonData.stabilityBudget period C q = EulerCorrectionAssembly.stabilityBudgetOfBase period hT A C.metric C.radius C.spatial q

structure EulerCorrectionAssembly.FiniteFamily (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) : Type

An actual finite-order correction family supplied by separate finite-existence theorems. Only its paths, zero initial data, divergence constraints and literal PDEs are inputs; compatibility is not assumed.

• solution (q : ℕ) : 6 ≤ q → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))

  A genuine continuous finite Sobolev correction at each order.

• initial (q : ℕ) (hq : 6 ≤ q) : (self.solution q hq) ⟨0, ⋯⟩ = 0

  Every correction starts from zero.

• divergence (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((self.solution q hq) t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period A.κ A.direction

  Every correction satisfies the actual lifted divergence constraint.

• equation (q : ℕ) (hq : 6 ≤ q) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T ⋯ (self.solution q hq) r)) (EulerCylinderSobolevSpace.value period ((EulerCorrectionOperators.CorrectionData.coefficients period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq).apply ⟨t, ⋯⟩ ((self.solution q hq) ⟨t, ⋯⟩))) t

  Every correction satisfies the literal projected inviscid equation at interior times.

noncomputable def EulerCorrectionAssembly.finiteFamilyOfExists (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (H : ∀ (q : ℕ) (hq : 6 ≤ q), ∃ (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))), e ⟨0, ⋯⟩ = 0 ∧ (∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (e t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period A.κ A.direction) ∧ ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T ⋯ e r)) (EulerCylinderSobolevSpace.value period ((EulerCorrectionOperators.CorrectionData.coefficients period (EulerAllOrderCorrectionData.Data.atOrder period A q) hq).apply ⟨t, ⋯⟩ (e ⟨t, ⋯⟩))) t) : FiniteFamily period hT A

Choose an actual finite correction family from proved finite-existence statements. This is an assembly helper conditional on finite existence, not an independent source existence theorem.

Equations

• EulerCorrectionAssembly.finiteFamilyOfExists period hT A H = { solution := fun (q : ℕ) (hq : 6 ≤ q) => Classical.choose ⋯, initial := ⋯, divergence := ⋯, equation := ⋯ }