Actual finite inviscid corrections constructed from the all-order drift-aware input budget.
Drift-aware version: Whole-interval inviscid correction retaining quantitative Gevrey bounds and its actual finite-Sobolev pressure equation.
theorem
EulerDriftGlobalInviscidGevrey.exists_global_inviscid_gevrey_PDE
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
(S : ℝ)
(hS : 0 < S)
(D : EulerCorrectionOperators.CorrectionData period (q + 1 + 1) ↑(Set.Icc 0 S))
(KG1 :
(t : ↑(Set.Icc 0 S)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection (q + 1)
(D.metric.coefficient t))
(KL1 :
(t : ↑(Set.Icc 0 S)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection (q + 1)
(D.linear.coefficient t))
(KQ1 :
(i : Fin 3) →
(t : ↑(Set.Icc 0 S)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection (q + 1)
((D.quadratic i).coefficient t))
(hG1 : Continuous fun (t : ↑(Set.Icc 0 S)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KG1 t))
(hL1 : Continuous fun (t : ↑(Set.Icc 0 S)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KL1 t))
(hQ1 :
∀ (i : Fin 3),
Continuous fun (t : ↑(Set.Icc 0 S)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ1 i t))
(KG0 :
(t : ↑(Set.Icc 0 S)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.metric.coefficient t))
(KL0 :
(t : ↑(Set.Icc 0 S)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.linear.coefficient t))
(KQ0 :
(i : Fin 3) →
(t : ↑(Set.Icc 0 S)) →
EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q
((D.quadratic i).coefficient t))
(hG0 : Continuous fun (t : ↑(Set.Icc 0 S)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KG0 t))
(hL0 : Continuous fun (t : ↑(Set.Icc 0 S)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KL0 t))
(hQ0 :
∀ (i : Fin 3),
Continuous fun (t : ↑(Set.Icc 0 S)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ0 i t))
(hG : Continuous fun (t : ↑(Set.Icc 0 S)) => (D.metric.coefficient t).operator)
(N : ℕ)
(hN : N + 6 ≤ q + 1 + 1)
(hNfull : q + 1 + 1 ≤ N + 6)
(R : C(↑(Set.Icc 0 S), ℝ))
(B : EulerDriftCorrectionBudget.Budget period ⋯ D N R)
(K : EulerCorrectionEnergyData.MetricBudget period S ⋯ D)
(C Δ ρ0 : ℝ)
(hC : EulerCorrectionEnergyMajorants.combinedConstant period B.full K ≤ C)
(hΔ : 0 < Δ)
(hΔ1 : Δ ≤ 1)
(hρ0 : 0 < ρ0)
(hdecay : 2 * C * (B.drift + Δ) * S ≤ ρ0 / 2)
(hscale : ρ0 * B.full.Rc ≤ 1)
(hsmall : 2 * B.full.residual * Real.exp (3 * C * S) ≤ Δ / 2)
(hR : ∀ (t : ↑(Set.Icc 0 S)), R t = ρ0 - 2 * C * (B.drift + Δ) * ↑t)
(hz :
∀ (t : ↑(Set.Icc 0 S)),
EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction)
:
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.full.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.
theorem
EulerAllOrderDriftCorrection.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) ≤ 2 * (B.spatial q hq).full.residual * Real.exp (3 * B.growthCoefficient * ↑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
Genuine drift-aware input budgets construct an actual finite-order inviscid correction with quantitative retained Gevrey energy. Finite existence, an energy inequality and convergence are conclusions of the imported actual construction, not hypotheses here.
noncomputable def
EulerAllOrderDriftCorrection.Budget.solution
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(B : Budget period hT A)
(q : ℕ)
(hq : 6 ≤ q)
:
The genuine finite solution chosen from the proved drift-aware construction.
Equations
- EulerAllOrderDriftCorrection.Budget.solution period B q hq = Classical.choose ⋯
Instances For
theorem
EulerAllOrderDriftCorrection.Budget.solution_energy
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(B : Budget period hT A)
(q : ℕ)
(hq : 6 ≤ q)
(P : ℕ)
(hPN : 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) ((solution period B q hq) t) ≤ 2 * (B.spatial q hq).full.residual * Real.exp (3 * B.growthCoefficient * ↑t) ∧ EulerGevreyMetricEstimate.energyNorm period P hP (B.radius t)
((EulerCorrectionEnergyData.MetricBudget.operatorPath period B.metric) t) ((solution period B q hq) t) ≤ B.delta / 2
The actual selected finite solutions retain both residual and target-error energy estimates.
noncomputable def
EulerAllOrderDriftCorrection.Budget.family
(period : ℝ)
[Fact (0 < period)]
{T : ℝ}
{hT : 0 < T}
{A : EulerAllOrderCorrectionData.Data period T}
(B : Budget period hT A)
:
EulerCorrectionAssembly.FiniteFamily period hT A
Actual drift-aware data construct the complete finite correction family; no finite-existence hypothesis is supplied.
Equations
- EulerAllOrderDriftCorrection.Budget.family period B = { solution := EulerAllOrderDriftCorrection.Budget.solution period B, initial := ⋯, divergence := ⋯, equation := ⋯ }