LeanPool.NavierStokesAndEuler.Euler.DriftGevreyInviscidEnergyCompactness

Drift-aware version: Actual strong inviscid compactness retaining the quantitative Gevrey metric energies.

Actual global-in-time viscous correction from concrete Gevrey coefficient and residual budgets.

The actual nonlinear Gevrey bootstrap applies uniformly to every partial correction solution.

EulerGevreyMetricEstimate.energyNorm period N hN (R ((EulerQuadraticSource.timeInclusion hTS) t)) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period K) ((EulerQuadraticSource.timeInclusion hTS) t)) (e t) ≤ 2 * B.full.residual * Real.exp (3 * C * ↑t) ∧ EulerGevreyMetricEstimate.energyNorm period N hN (R ((EulerQuadraticSource.timeInclusion hTS) t)) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period K) ((EulerQuadraticSource.timeInclusion hTS) t)) (e t) ≤ Δ / 2

Every actual partial solution inherits the same quantitative shrinking-radius estimate from the fixed global data.

source

theorem EulerDriftGlobalGevreyCorrection.exists_global_gevrey_correction (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (S : ℝ) (hS : 0 < S) (D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 S)) (KG : (t : ↑(Set.Icc 0 S)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.metric.coefficient t)) (KL : (t : ↑(Set.Icc 0 S)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (D.linear.coefficient t)) (KQ : (i : Fin 3) → (t : ↑(Set.Icc 0 S)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q ((D.quadratic i).coefficient t)) (hGq : Continuous fun (t : ↑(Set.Icc 0 S)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KG t)) (hLq : Continuous fun (t : ↑(Set.Icc 0 S)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KL t)) (hQq : ∀ (i : Fin 3), Continuous fun (t : ↑(Set.Icc 0 S)) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (KQ i t)) (hG : Continuous fun (t : ↑(Set.Icc 0 S)) => (D.metric.coefficient t).operator) (N : ℕ) (hN : N + 6 ≤ q + 1) (hNfull : q + 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) (ν : ℝ) (hν : 0 < ν) (hν1 : ν ≤ 1) (hz : ∀ (t : ↑(Set.Icc 0 S)), EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) :

∃ (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) ∧ (∀ (t : ↑(Set.Icc 0 S)), e t = EulerQuadraticSource.quadraticDuhamel period ν hν ⋯ ⋯ (EulerCorrectionOperators.CorrectionData.coefficients period (EulerCorrectionLowerData.lowerData period D KG KL KQ hGq hLq hQq) hq) 0 e t) ∧ (∀ (t : ↑(Set.Icc 0 S)), EulerGevreyMetricEstimate.energyNorm period N hN (R t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period K) t) (e t) ≤ 2 * B.full.residual * Real.exp (3 * C * ↑t) ∧ EulerGevreyMetricEstimate.energyNorm period N hN (R t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period K) t) (e t) ≤ Δ / 2) ∧ ‖e‖ ≤ EulerGevreyMetricEstimate.metricAmplification K.c * (Δ / 2) / EulerPacketWeights.weight (min (ρ0 / 2) 1) N

Concrete coefficient and residual bounds yield an actual viscous correction throughout the prescribed interval. The a-priori energy estimate and the continuation bound are proved inside this theorem, not supplied as hypotheses.

Drift-aware version: A genuine uniformly bounded viscous approximation family with a uniformly vanishing PDE viscosity term.

source

∃ (e : ℕ → C(↑(Set.Icc 0 S), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))), (∀ (n : ℕ), (e n) ⟨0, ⋯⟩ = 0 ∧ (∀ (t : ↑(Set.Icc 0 S)), EulerCylinderSobolevSpace.value period ((e n) t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) ∧ (∀ (t : ↑(Set.Icc 0 S)), (e n) t = EulerQuadraticSource.quadraticDuhamel period (EulerViscosityDefect.viscositySequence n) ⋯ ⋯ ⋯ (EulerCorrectionOperators.CorrectionData.coefficients period (EulerCorrectionLowerData.lowerData period D KG KL KQ hGq hLq hQq) hq) 0 (e n) t) ∧ (∀ (t : ↑(Set.Icc 0 S)), EulerGevreyMetricEstimate.energyNorm period N hN (R t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period K) t) ((e n) t) ≤ 2 * B.full.residual * Real.exp (3 * C * ↑t) ∧ EulerGevreyMetricEstimate.energyNorm period N hN (R t) ((EulerCorrectionEnergyData.MetricBudget.operatorPath period K) t) ((e n) t) ≤ Δ / 2) ∧ ‖e n‖ ≤ EulerGevreyMetricEstimate.metricAmplification K.c * (Δ / 2) / EulerPacketWeights.weight (min (ρ0 / 2) 1) N) ∧ Filter.Tendsto (fun (n : ℕ) => EulerViscosityDefect.viscousDefect period ⋯ (EulerViscosityDefect.viscositySequence n) S (e n)) Filter.atTop (nhds 0)

The actual finite-cutoff correction has a viscosity approximation sequence with uniform energy control and a uniformly vanishing literal viscous term. This theorem does not assert convergence of the nonlinear solution sequence itself.

source

@[instance_reducible]

noncomputable def EulerDriftGevreyInviscidEnergyCompactness.energyCompactnessSobolevGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) :

NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The inherited Sobolev normed-group instance for compactness.

Equations

EulerDriftGevreyInviscidEnergyCompactness.energyCompactnessSobolevGroup period q = inferInstance

Instances For

source

@[instance_reducible]

noncomputable def EulerDriftGevreyInviscidEnergyCompactness.energyCompactnessSobolevSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) :

NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The inherited real Sobolev module instance for compactness.

Equations

EulerDriftGevreyInviscidEnergyCompactness.energyCompactnessSobolevSpace period q = inferInstance

Instances For

source

∃ (u : ℕ → C(↑(Set.Icc 0 S), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (e : C(↑(Set.Icc 0 S), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))), (∀ (n : ℕ), (u n) ⟨0, ⋯⟩ = 0 ∧ (∀ (t : ↑(Set.Icc 0 S)), EulerCylinderSobolevSpace.value period ((u n) t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) ∧ (∀ (t : ↑(Set.Icc 0 S)), (u n) t = EulerQuadraticSource.quadraticDuhamel period (EulerViscosityDefect.viscositySequence n) ⋯ ⋯ ⋯ (EulerCorrectionOperators.CorrectionData.coefficients period (EulerCorrectionLowerData.lowerData period D KG KL KQ hGq hLq hQq) hq) 0 (u n) t) ∧ ‖u n‖ ≤ EulerGevreyMetricEstimate.metricAmplification K.c * (Δ / 2) / EulerPacketWeights.weight (min (ρ0 / 2) 1) N) ∧ Filter.Tendsto (fun (n : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 S)) (EulerCylinderSobolevSpace.truncateOperator period q)) (u n)) Filter.atTop (nhds e) ∧ 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) (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

The actual Gevrey correction construction produces its strong inviscid limit with both quantitative energy bounds at every retained cutoff. No convergence, compactness, energy inequality, or comparison estimate is supplied as a hypothesis.