LeanPool.NavierStokesAndEuler.Euler.GevreyPathNorm

Related estimates used together by the same construction modules.

A genuine metric Gevrey bound supplies the uniform Banach norm used in actual continuation.

Actual complete-Sobolev control from a positive-radius finite Gevrey bound, for parabolic continuation.

theorem EulerGevreyContinuationNorm.weight_lower (ρ δ : ℝ) (hδ : 0 < δ) (hδρ : δ ≤ ρ) (hδ1 : δ ≤ 1) (n N : ℕ) (hn : n ≤ N) :

EulerPacketWeights.weight δ N ≤ EulerPacketWeights.weight ρ n

At every retained derivative order, the Gevrey weight is bounded below by one positive fixed-cutoff weight.

source

theorem EulerGevreyContinuationNorm.word_le_level (period : ℝ) [Fact (0 < period)] {s : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (w : EulerCylinderSobolevSpace.SobolevWord s) :

‖↑u w‖ ≤ EulerJetProductBounds.levelNorm period (EulerCylinderSobolevSpace.toJet period u) ↑w.fst

Each actual derivative coordinate is bounded by its genuine homogeneous derivative-sum norm.

source

theorem EulerGevreyContinuationNorm.level_le_block (period : ℝ) [Fact (0 < period)] {s : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (N m : ℕ) (hm : m ≤ N + 6) :

EulerJetProductBounds.levelNorm period (EulerCylinderSobolevSpace.toJet period u) m ≤ EulerH6Pressure.blockNorm period (EulerCylinderSobolevSpace.toJet period u) 6 (min m N)

Every derivative coordinate through the full energy order is contained in one retained external/base block.

source

theorem EulerGevreyContinuationNorm.norm_le_weighted (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (hS : s ≤ N + 6) (ρ δ : ℝ) (hδ : 0 < δ) (hδρ : δ ≤ ρ) (hδ1 : δ ≤ 1) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) :

‖u‖ ≤ EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u / EulerPacketWeights.weight δ N

A finite actual Gevrey bound controls the complete energy-order Sobolev norm on every positive-radius interval.

source

theorem EulerGevreyContinuationNorm.norm_le_metric (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (hN : N + 6 ≤ s) (hS : s ≤ N + 6) (ρ δ : ℝ) (hδ : 0 < δ) (hδρ : δ ≤ ρ) (hδ1 : δ ≤ 1) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (c : ℝ) (hc : 0 < c) (hK : ∀ (v : ↥(EulerLiftedGradientSpace.LiftL2 period)), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (K v) v) :

‖u‖ ≤ EulerGevreyMetricEstimate.metricAmplification c * EulerGevreyMetricEstimate.energyNorm period N hN ρ K u / EulerPacketWeights.weight δ N

A metric Gevrey bound gives the actual finite-Sobolev state bound needed by the uniform local restart theorem.

source

theorem EulerGevreyPathNorm.norm_le_of_energy_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (N : ℕ) (hN : N + 6 ≤ q + 1) (hS : q + 1 ≤ N + 6) (T : ℝ) (R : C(↑(Set.Icc 0 T), ℝ )) (K : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (c δ E : ℝ) (hc : 0 < c) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hE : 0 ≤ E) (hR : ∀ (t : ↑(Set.Icc 0 T)), δ ≤ R t) (hK : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLiftedGradientSpace.LiftL2 period)), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ ((K t) v) v) (he : ∀ (t : ↑(Set.Icc 0 T)), (EulerEnergyMetricPaths.energyPath period N hN T R K e) t ≤ E) :

‖e‖ ≤ EulerGevreyMetricEstimate.metricAmplification c * E / EulerPacketWeights.weight δ N

A uniform metric-energy bound controls the actual continuous Sobolev path norm.

Quantitative finite Gevrey bounds survive the actual strong time-path limit.

The actual finite Gevrey metric energy passes to strong Sobolev limits.

source

theorem EulerGevreyEnergyLimit.energyValues_continuous (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) :

Continuous (EulerGevreyMetricComparison.energyValues period q N hN)

Actual energy coordinates depend continuously on the Sobolev field.

source

theorem EulerGevreyEnergyLimit.energyNorm_continuous (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ ] ↥(EulerLiftedGradientSpace.LiftL2 period)) :

Continuous (EulerGevreyMetricEstimate.energyNorm period N hN ρ K)

The actual finite Gevrey metric energy is continuous in its Sobolev field, including zero energy.

source

theorem EulerGevreyEnergyLimit.energyNorm_restrict (period : ℝ) [Fact (0 < period)] {p q : ℕ} (hqp : q ≤ p) (N : ℕ) (hN : N + 6 ≤ q) (ρ : ℝ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) :

EulerGevreyMetricEstimate.energyNorm period N hN ρ K ((EulerCylinderSobolevSpace.restrictOperator period hqp) u) = EulerGevreyMetricEstimate.energyNorm period N ⋯ ρ K u

Restriction preserving the derivative cutoff leaves the actual Gevrey energy unchanged.

source

theorem EulerGevreyEnergyLimit.energyNorm_limit_bound (period : ℝ) [Fact (0 < period)] {p q : ℕ} (hqp : q ≤ p) (N : ℕ) (hN : N + 6 ≤ q) (ρ : ℝ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (u : ℕ → ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (h : Filter.Tendsto (fun (n : ℕ) => (EulerCylinderSobolevSpace.restrictOperator period hqp) (u n)) Filter.atTop (nhds e)) (M : ℝ) (hb : ∀ (n : ℕ), EulerGevreyMetricEstimate.energyNorm period N ⋯ ρ K (u n) ≤ M) :

EulerGevreyMetricEstimate.energyNorm period N hN ρ K e ≤ M

A genuine strong lower-order limit retains every finite metric-energy bound whose derivative cutoff is retained.

Monotonicity of the actual finite Gevrey metric energy in the external cutoff.

source

def EulerGevreyEnergyCutoff.externalWordInclusion {N M : ℕ} (hNM : N ≤ M) (I : EulerGevreyMetricComparison.ExternalWord N) :

EulerGevreyMetricComparison.ExternalWord M

The literal inclusion of external words into a larger cutoff.

Equations

EulerGevreyEnergyCutoff.externalWordInclusion hNM I = ⟨Fin.castLE ⋯ I.fst, I.snd⟩

Instances For

source

theorem EulerGevreyEnergyCutoff.externalWordInclusion_injective {N M : ℕ} (hNM : N ≤ M) :

Function.Injective (externalWordInclusion hNM)

Increasing the cutoff does not identify distinct derivative words.

source

theorem EulerGevreyEnergyCutoff.energyValues_inclusion (period : ℝ) [Fact (0 < period)] {s N M q : ℕ} (hNM : N ≤ M) (hM : M + q ≤ s) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (I : EulerGevreyMetricComparison.ExternalWord N) :

EulerGevreyMetricComparison.energyValues period q M hM u (externalWordInclusion hNM I) = EulerGevreyMetricComparison.energyValues period q N ⋯ u I

The retained energy coordinates are identical in a larger cutoff.

source

theorem EulerGevreyEnergyCutoff.energyNorm_cutoff_mono (period : ℝ) [Fact (0 < period)] {s N M : ℕ} (hNM : N ≤ M) (hM : M + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) :

EulerGevreyMetricEstimate.energyNorm period N ⋯ ρ K u ≤ EulerGevreyMetricEstimate.energyNorm period M hM ρ K u

The literal finite Gevrey metric energy increases with its external derivative cutoff.

source

theorem EulerGevreyEnergyPathLimit.energyNorm_path_limit_bound (period : ℝ) [Fact (0 < period)] {p q N : ℕ} (hqp : q ≤ p) (hN : N + 6 ≤ p) (T : ℝ) (ρ : ↑(Set.Icc 0 T) → ℝ) (hρ : ∀ (t : ↑(Set.Icc 0 T)), 0 < ρ t) (K : ↑(Set.Icc 0 T) → ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (u : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period p))) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (hconv : Filter.Tendsto (fun (n : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.restrictOperator period hqp)) (u n)) Filter.atTop (nhds e)) (B : ↑(Set.Icc 0 T) → ℝ) (hb : ∀ (n : ℕ) (t : ↑(Set.Icc 0 T)), EulerGevreyMetricEstimate.energyNorm period N hN (ρ t) (K t) ((u n) t) ≤ B t) (P : ℕ) (hPN : P ≤ N) (hP : P + 6 ≤ q) (t : ↑(Set.Icc 0 T)) :

EulerGevreyMetricEstimate.energyNorm period P hP (ρ t) (K t) (e t) ≤ B t

Every retained Gevrey cutoff of the actual strong path limit keeps the genuine uniform approximation bound.

Actual divergence-free continuation of the concrete viscous correction equation.

Genuine finite-time continuation of actual viscous mild solutions from an a priori Sobolev bound.

source

theorem EulerBoundedMildContinuation.advance_time_eq (a δ S : ℝ) :

a + min δ (S - a) = min (a + δ) S

The next actual time window ends at the smaller of one full step and the terminal time.

source

theorem EulerBoundedMildContinuation.advance_grid (S δ a : ℝ) (hδ : 0 ≤ δ) (n : ℕ) (hgrid : min (↑n * δ) S ≤ a) :

min (↑(n + 1) * δ) S ≤ a + min δ (S - a)

Repeated genuine local windows reach each successive point of a fixed finite time grid.

source

theorem EulerBoundedMildContinuation.exists_global_mild_of_bound (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν : ℝ) (hν : 0 < ν) (S : ℝ) (hS : 0 < S) (R : ℝ) (hR : 0 ≤ R) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (hu₀ : ‖u₀‖ ≤ R) (C : EulerQuadraticSource.Coefficients ↑(Set.Icc 0 S) ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hbound : ∀ (T : ℝ) (hT : 0 ≤ T) (hTS : T ≤ S) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))), (∀ (t : ↑(Set.Icc 0 T)), u t = EulerQuadraticSource.quadraticDuhamel period ν hν hT hTS C u₀ u t) → ‖u‖ ≤ R) :

∃ (u : C(↑(Set.Icc 0 S), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))), ‖u‖ ≤ R ∧ u ⟨0, ⋯⟩ = u₀ ∧ ∀ (t : ↑(Set.Icc 0 S)), u t = EulerQuadraticSource.quadraticDuhamel period ν hν ⋯ ⋯ C u₀ u t

An actual uniform Sobolev bound on partial solutions yields a genuine solution on the whole prescribed interval. The continuation is constructed by finitely many actual local heat solves and exact nonlinear pasting.

source

theorem EulerCorrectionContinuation.correction_mild_divergenceFree (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (ν : ℝ) (hν : 0 < ν) {T S : ℝ} (hT : 0 ≤ T) (hTS : T ≤ S) (D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 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 D hq) 0 e t) (t : ↑(Set.Icc 0 T)) :

EulerCylinderSobolevSpace.value period (e t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction

Every actual partial zero-initial correction solution preserves the lifted divergence constraint.

source

theorem EulerCorrectionContinuation.exists_global_correction_of_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (ν : ℝ) (hν : 0 < ν) (S : ℝ) (hS : 0 < S) (R : ℝ) (hR : 0 ≤ R) (D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 S)) (hbound : ∀ (T : ℝ) (hT : 0 ≤ T) (hTS : T ≤ S) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))), (∀ (t : ↑(Set.Icc 0 T)), e t = EulerQuadraticSource.quadraticDuhamel period ν hν hT hTS (EulerCorrectionOperators.CorrectionData.coefficients period D hq) 0 e t) → ‖e‖ ≤ R) :

∃ (e : C(↑(Set.Icc 0 S), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))), ‖e‖ ≤ R ∧ 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 D hq) 0 e t

A genuine a-priori Sobolev bound continues the actual zero-initial viscous Euler correction across the prescribed interval.

Applying the concrete Gevrey budgets to a genuinely bounded viscous correction family.

source

∃ (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))), Filter.Tendsto (fun (n : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period q)) (u n)) Filter.atTop (nhds e) ∧ e ⟨0, ⋯⟩ = 0 ∧ (∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (e t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) ∧ ‖e‖ ≤ M

Concrete Gevrey and inverse-metric budgets turn a genuinely bounded correction family into its actual strong lower-order limit.