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.
theorem
EulerPartialCorrectionBootstrap.partial_correction_bootstrap
(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)
(R : C(↑(Set.Icc 0 S), ℝ))
(B : EulerCorrectionEnergyData.SpatialBudget period ⋯ D N R)
(K : EulerCorrectionEnergyData.MetricBudget period S hS D)
(C Δ ρ0 : ℝ)
(hC : EulerCorrectionEnergyMajorants.combinedConstant period B K ≤ C)
(hΔ : 0 < Δ)
(hΔ1 : Δ ≤ 1)
(hρ0 : 0 < ρ0)
(hdecay : 2 * C * (B.B0 + Δ) * S ≤ ρ0 / 2)
(hscale : ρ0 * B.Rc ≤ 1)
(hsmall : 2 * B.residual * Real.exp (3 * C * S) ≤ Δ / 2)
(hR : ∀ (t : ↑(Set.Icc 0 S)), R t = ρ0 - 2 * C * (B.B0 + Δ) * ↑t)
(ν : ℝ)
(hν : 0 < ν)
(hν1 : ν ≤ 1)
(hz :
∀ (t : ↑(Set.Icc 0 S)),
EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction)
(T : ℝ)
(hT : 0 ≤ T)
(hTS : T ≤ S)
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(hsol :
∀ (t : ↑(Set.Icc 0 T)),
e t = EulerQuadraticSource.quadraticDuhamel period ν hν hT hTS
(EulerCorrectionOperators.CorrectionData.coefficients period
(EulerCorrectionLowerData.lowerData period D KG KL KQ hGq hLq hQq) hq)
0 e t)
(t : ↑(Set.Icc 0 T))
:
EulerGevreyMetricEstimate.energyNorm period N hN (R ((EulerQuadraticSource.timeInclusion hTS) t))
((EulerCorrectionEnergyData.MetricBudget.operatorPath period K) ((EulerQuadraticSource.timeInclusion hTS) t))
(e t) ≤ 2 * B.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.
theorem
EulerGlobalGevreyCorrection.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 : EulerCorrectionEnergyData.SpatialBudget period ⋯ D N R)
(K : EulerCorrectionEnergyData.MetricBudget period S ⋯ D)
(C Δ ρ0 : ℝ)
(hC : EulerCorrectionEnergyMajorants.combinedConstant period B K ≤ C)
(hΔ : 0 < Δ)
(hΔ1 : Δ ≤ 1)
(hρ0 : 0 < ρ0)
(hdecay : 2 * C * (B.B0 + Δ) * S ≤ ρ0 / 2)
(hscale : ρ0 * B.Rc ≤ 1)
(hsmall : 2 * B.residual * Real.exp (3 * C * S) ≤ Δ / 2)
(hR : ∀ (t : ↑(Set.Icc 0 S)), R t = ρ0 - 2 * C * (B.B0 + Δ) * ↑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.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.
A genuine uniformly bounded viscous approximation family with a uniformly vanishing PDE viscosity term.
theorem
EulerViscousCorrectionFamily.exists_viscous_correction_family
(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 : EulerCorrectionEnergyData.SpatialBudget period ⋯ D N R)
(K : EulerCorrectionEnergyData.MetricBudget period S ⋯ D)
(C Δ ρ0 : ℝ)
(hC : EulerCorrectionEnergyMajorants.combinedConstant period B K ≤ C)
(hΔ : 0 < Δ)
(hΔ1 : Δ ≤ 1)
(hρ0 : 0 < ρ0)
(hdecay : 2 * C * (B.B0 + Δ) * S ≤ ρ0 / 2)
(hscale : ρ0 * B.Rc ≤ 1)
(hsmall : 2 * B.residual * Real.exp (3 * C * S) ≤ Δ / 2)
(hR : ∀ (t : ↑(Set.Icc 0 S)), R t = ρ0 - 2 * C * (B.B0 + Δ) * ↑t)
(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)))),
(∀ (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.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.
@[instance_reducible]
noncomputable def
EulerGevreyInviscidEnergyCompactness.energyCompactnessSobolevGroup
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
The inherited Sobolev normed-group instance for compactness.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerGevreyInviscidEnergyCompactness.energyCompactnessSobolevSpace
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)
The inherited real Sobolev module instance for compactness.
Equations
Instances For
theorem
EulerGevreyInviscidEnergyCompactness.exists_gevrey_inviscid_energy_limit
(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 : EulerCorrectionEnergyData.SpatialBudget period ⋯ D N R)
(K : EulerCorrectionEnergyData.MetricBudget period S ⋯ D)
(C Δ ρ0 : ℝ)
(hC : EulerCorrectionEnergyMajorants.combinedConstant period B K ≤ C)
(hΔ : 0 < Δ)
(hΔ1 : Δ ≤ 1)
(hρ0 : 0 < ρ0)
(hdecay : 2 * C * (B.B0 + Δ) * S ≤ ρ0 / 2)
(hscale : ρ0 * B.Rc ≤ 1)
(hsmall : 2 * B.residual * Real.exp (3 * C * S) ≤ Δ / 2)
(hR : ∀ (t : ↑(Set.Icc 0 S)), R t = ρ0 - 2 * C * (B.B0 + Δ) * ↑t)
(hz :
∀ (t : ↑(Set.Icc 0 S)),
EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction)
:
∃ (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.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.