LeanPool.NavierStokesAndEuler.Euler.AllOrderCorrectionBudget

Concrete uniform Gevrey budgets for one coherent family of prescribed data.

Whole-interval inviscid correction retaining quantitative Gevrey bounds and its actual finite-Sobolev pressure equation.

source

have Dlow := EulerCorrectionLowerData.lowerData period (EulerCorrectionLowerData.lowerData period D KG1 KL1 KQ1 hG1 hL1 hQ1) KG0 KL0 KQ0 hG0 hL0 hQ0; ∃ (e : C(↑(Set.Icc 0 S), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))), e ⟨0, ⋯⟩ = 0 ∧ (∀ (t : ↑(Set.Icc 0 S)), EulerCylinderSobolevSpace.value period (e t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) ∧ ‖e‖ ≤ EulerGevreyMetricEstimate.metricAmplification K.c * (Δ / 2) / EulerPacketWeights.weight (min (ρ0 / 2) 1) N ∧ (∀ P ≤ N, ∀ (hP : P + 6 ≤ q + 1) (t : ↑(Set.Icc 0 S)), EulerGevreyMetricEstimate.energyNorm period P hP (R t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period K) t) (e t) ≤ 2 * B.residual * Real.exp (3 * C * ↑t) ∧ EulerGevreyMetricEstimate.energyNorm period P hP (R t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period K) t) (e t) ≤ Δ / 2) ∧ ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 S), HasDerivAt (fun (r : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period q) (EulerVolterraConvolution.extendPath S ⋯ e r)) (-EulerCorrectionOperators.CorrectionData.rawSource period Dlow hq ⟨t, ⋯⟩ (e ⟨t, ⋯⟩) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period (Dlow.metric.jet ⟨t, ⋯⟩)) (EulerCorrectionOperators.CorrectionData.pressure period Dlow hq ⟨t, ⋯⟩ (e ⟨t, ⋯⟩))) t

Concrete Gevrey data construct an actual global inviscid correction, retaining both quantitative energy bounds at every surviving cutoff, with its literal signed-pressure derivative in Hq.

source

structure EulerAllOrderCorrectionBudget.Budget (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) :

Type

Actual all-order data budgets with common radius, error size and time interval; these are coefficient/background/residual inequalities, not solution or energy hypotheses.

metric : EulerCorrectionEnergyData.MetricBudget period T ⋯ (EulerAllOrderCorrectionData.Data.atOrder period A 1)
The common actual inverse metric and its genuine time derivative.
radius : C(↑(Set.Icc 0 T), ℝ )
The common positive shrinking-radius path.
boundConstant : ℝ
The common scalar growth coefficient.
delta : ℝ
The common desired error size.
initialRadius : ℝ
The common initial radius.
spatial (q : ℕ) (hq : 6 ≤ q) : EulerCorrectionEnergyData.SpatialBudget period ⋯ (EulerAllOrderCorrectionData.Data.atOrder period A (q + 1 + 1)) (q - 4) self.radius
Genuine coefficient, background and residual bounds at each finite construction cutoff.
constant_bound (q : ℕ) (hq : 6 ≤ q) : EulerCorrectionEnergyMajorants.combinedConstant period (self.spatial q hq) (EulerAllOrderCorrectionData.Data.metricBudget period A ⋯ self.metric (q + 1)) ≤ self.boundConstant
The fixed scalar dominates each proved nonlinear energy constant.
delta_pos : 0 < self.delta
Strictly positive target error size.
delta_le_one : self.delta ≤ 1
The target error is at most one.
radius_pos : 0 < self.initialRadius
Strictly positive initial radius.
decay (q : ℕ) (hq : 6 ≤ q) : 2 * self.boundConstant * ((self.spatial q hq).B0 + self.delta) * T ≤ self.initialRadius / 2
Every construction retains half the common initial radius.
scale (q : ℕ) (hq : 6 ≤ q) : self.initialRadius * (self.spatial q hq).Rc ≤ 1
The coefficient scale fits the common initial radius.
small (q : ℕ) (hq : 6 ≤ q) : 2 * (self.spatial q hq).residual * Real.exp (3 * self.boundConstant * T) ≤ self.delta / 2
The actual residual budgets beat the genuine Gronwall factor.
radius_eq (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : self.radius t = self.initialRadius - 2 * self.boundConstant * ((self.spatial q hq).B0 + self.delta) * ↑t
Every finite construction uses the same actual shrinking radius.
divergence (t : ↑(Set.Icc 0 T)) : A.approximation.field t ∈ EulerLiftedGradientSpace.divergenceFreeSpace period A.κ A.direction
The prescribed approximate field is genuinely lifted divergence-free.

Instances For

source

theorem EulerAllOrderCorrectionBudget.finite_exists (period : ℝ) [Fact (0 < period)] {T : ℝ} (hT : 0 < T) (A : EulerAllOrderCorrectionData.Data period T) (B : Budget period hT A) (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) ∧ (∀ P ≤ q - 4, ∀ (hP : P + 6 ≤ q + 1) (t : ↑(Set.Icc 0 T)), EulerGevreyMetricEstimate.energyNorm period P hP (B.radius t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period B.metric) t) (e t) ≤ B.delta / 2) ∧ ∀ (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

The concrete all-order budgets construct an actual finite-order inviscid correction, with retained Gevrey energy and its actual equation.