Uniform H³ comparison and the actual no-gradient-escape consequence for genuine ordinary Euler evolutions. No energy inequality is assumed.

A regularized H³ norm of the actual Euler difference satisfies the quadratic stability inequality. The regularization only removes the square-root singularity at a vanishing difference.

The scalar comparison lemma with genuine one-sided endpoint derivatives.

theorem EulerOrdinarySobolev.quadratic_stability_within (X X' : ℝ → ℝ) (C ε T : ℝ) (hC : 0 < C) (hε : 0 < ε) (_hT : 0 ≤ T) (hsmall : 2 * ε * Real.exp (3 * C * T) ≤ 1 / 2) (hcont : ContinuousOn X (Set.Icc 0 T)) (hinit : X 0 ≤ ε) (hder : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt X (X' t) (Set.Icc 0 T) t) (hineq : ∀ t ∈ Set.Ico 0 T, X' t ≤ C * (X t + X t ^ 2)) (t : ℝ) : t ∈ Set.Icc 0 T → X t ≤ 2 * ε * Real.exp (3 * C * T)

noncomputable def EulerOrdinarySobolev.stabilityConstant (M : ℝ) : ℝ

Stability constant, given by 1+1800*h3ProductConstant*(1+M).

Equations

• EulerOrdinarySobolev.stabilityConstant M = 1 + 1800 * EulerOrdinarySobolev.h3ProductConstant * (1 + M)

theorem EulerOrdinarySobolev.stabilityConstant_pos {M : ℝ} (hM : 0 ≤ M) : 0 < stabilityConstant M

theorem EulerOrdinarySobolev.regularized_energy_bound (e ep M δ : ℝ) (he : 0 ≤ e) (hM : 0 ≤ M) (hδ : 0 < δ) (hp : ep ≤ 3600 * h3ProductConstant * (M + √e) * e) : 20 * ep / √(e + δ ^ 2) ≤ stabilityConstant M * (40 * √(e + δ ^ 2) + (40 * √(e + δ ^ 2)) ^ 2)

noncomputable def EulerOrdinarySobolev.Evolution.normEnvelope {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (δ : ℝ) : C(↑(Set.Icc 0 T), ℝ)

Norm envelope, given by ⟨fun t => 40*sqrt (U.energyPath V t+δ^2), continuous_const.mul (((U.energyPath V).continuous.add continuous_const).sqrt)⟩.

Equations

• U.normEnvelope V δ = { toFun := fun (t : ↑(Set.Icc 0 T)) => 40 * √((U.energyPath V) t + δ ^ 2), continuous_toFun := ⋯ }

noncomputable def EulerOrdinarySobolev.Evolution.envelopeDerivative {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (δ : ℝ) (t : ↑(Set.Icc 0 T)) : ℝ

Envelope derivative, given by 20*U.energyDerivative V t/sqrt (U.energyPath V t+δ^2).

Equations

• U.envelopeDerivative V δ t = 20 * U.energyDerivative V t / √((U.energyPath V) t + δ ^ 2)

theorem EulerOrdinarySobolev.Evolution.energyPath_nonneg {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (t : ↑(Set.Icc 0 T)) : 0 ≤ (U.energyPath V) t

theorem EulerOrdinarySobolev.Evolution.normEnvelope_nonneg {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (δ : ℝ) (t : ↑(Set.Icc 0 T)) : 0 ≤ (U.normEnvelope V δ) t

theorem EulerOrdinarySobolev.Evolution.normEnvelope_hasDerivWithinAt {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (δ : ℝ) (hδ : 0 < δ) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (U.normEnvelope V δ)) (U.envelopeDerivative V δ t) (Set.Icc 0 T) ↑t

theorem EulerOrdinarySobolev.Evolution.envelopeDerivative_bound {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (M δ : ℝ) (hM : ∀ (t : ↑(Set.Icc 0 T)), WordBound 4 M (U.velocity t)) (hδ : 0 < δ) (t : ↑(Set.Icc 0 T)) : U.envelopeDerivative V δ t ≤ stabilityConstant M * ((U.normEnvelope V δ) t + (U.normEnvelope V δ) t ^ 2)

theorem EulerOrdinarySobolev.Evolution.normEnvelope_majorizes {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (δ : ℝ) (t : ↑(Set.Icc 0 T)) : tensorNorm 3 (U.difference V t) ≤ (U.normEnvelope V δ) t

theorem EulerOrdinarySobolev.Evolution.normEnvelope_initial {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (ε : ℝ) (hε : 0 < ε) (hinit : tensorNorm 3 (U.difference V ⟨0, ⋯⟩) ≤ ε) : (U.normEnvelope V ε) ⟨0, ⋯⟩ ≤ 320 * ε

theorem EulerOrdinarySobolev.Evolution.h3_stability {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (M ε : ℝ) (hM : ∀ (t : ↑(Set.Icc 0 T)), WordBound 4 M (U.velocity t)) (hε : 0 < ε) (hinit : tensorNorm 3 (U.difference V ⟨0, ⋯⟩) ≤ ε) (hsmall : 640 * ε * Real.exp (3 * stabilityConstant M * T) ≤ 1 / 2) (t : ↑(Set.Icc 0 T)) : tensorNorm 3 (U.difference V t) ≤ 640 * ε * Real.exp (3 * stabilityConstant M * T)

noncomputable def EulerOrdinarySobolev.Evolution.referenceNormPath {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) : C(↑(Set.Icc 0 T), ℝ)

Reference norm path, given by ⟨fun t => tensorNorm 4 (U.velocity t),by apply continuous_finsetSum intro n _ exact (U.velocity_continuous n).norm⟩.

Equations

• U.referenceNormPath = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerOrdinarySobolev.tensorNorm 4 (U.velocity t), continuous_toFun := ⋯ }

noncomputable def EulerOrdinarySobolev.Evolution.referenceSize {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) : ℝ

Reference size, given by ‖U.referenceNormPath‖.

Equations

• U.referenceSize = ‖U.referenceNormPath‖

theorem EulerOrdinarySobolev.Evolution.referenceSize_nonneg {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) : 0 ≤ U.referenceSize

theorem EulerOrdinarySobolev.Evolution.referenceWordBound {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : WordBound 4 U.referenceSize (U.velocity t)

theorem EulerOrdinarySobolev.Evolution.gradient_continuous {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (x : EulerSmoothLimit.Space) : Continuous fun (t : ↑(Set.Icc 0 T)) => fderiv ℝ (U.velocity t).field x

theorem EulerOrdinarySobolev.Evolution.eventually_h3_bound {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (V : ℕ → Evolution T hT) (ε : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hlim : Filter.Tendsto ε Filter.atTop (nhds 0)) (hinit : ∀ (n : ℕ), tensorNorm 3 (U.difference (V n) ⟨0, ⋯⟩) ≤ ε n) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (t : ↑(Set.Icc 0 T)), tensorNorm 3 (U.difference (V n) t) ≤ 640 * ε n * Real.exp (3 * stabilityConstant U.referenceSize * T)

theorem EulerOrdinarySobolev.Evolution.sampled_h3_tendsto_zero {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (V : ℕ → Evolution T hT) (ε : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hlim : Filter.Tendsto ε Filter.atTop (nhds 0)) (hinit : ∀ (n : ℕ), tensorNorm 3 (U.difference (V n) ⟨0, ⋯⟩) ≤ ε n) (times : ℕ → ↑(Set.Icc 0 T)) : Filter.Tendsto (fun (n : ℕ) => tensorNorm 3 (U.difference (V n) (times n))) Filter.atTop (nhds 0)

theorem EulerOrdinarySobolev.Evolution.no_gradient_escape {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (V : ℕ → Evolution T hT) (ε : ℕ → ℝ) (hε : ∀ (n : ℕ), 0 < ε n) (hlim : Filter.Tendsto ε Filter.atTop (nhds 0)) (hinit : ∀ (n : ℕ), tensorNorm 3 (U.difference (V n) ⟨0, ⋯⟩) ≤ ε n) (times : ℕ → ↑(Set.Icc 0 T)) : ¬Filter.Tendsto (fun (n : ℕ) => ‖fderiv ℝ ((V n).velocity (times n)).field 0‖) Filter.atTop Filter.atTop