The packet-sequence form of ordinary Euler compactness: a common H³ bound, uniform initial Sobolev bounds, and initial L² Cauchy data produce an actual smooth Euler limit on the same positive interval.

theorem EulerOrdinarySobolev.wordEnergy_le_tensorNorm (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (m : ℕ) : wordEnergy m A ≤ wordCount m * tensorNorm m A ^ 2

theorem EulerOrdinarySobolev.Evolution.fieldPath_eq_velocityPath {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) : fieldPath U.velocity ⋯ = U.velocityPath

theorem EulerOrdinarySobolev.Evolution.gradient_le_h3 {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (M : ℝ) (hM : ∀ (t : ↑(Set.Icc 0 T)), tensorNorm 3 (U.velocity t) ≤ M) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (U.velocity t).field x‖ ≤ 9 * EulerSmoothSobolev.smoothEmbeddingConstant * M

theorem EulerOrdinarySobolev.Evolution.cauchyPath_of_initial {T : ℝ} {hT : 0 ≤ T} (V : ℕ → Evolution T hT) (M : ℝ) (hM : ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm 3 ((V k).velocity t) ≤ M) (hinit : CauchySeq fun (k : ℕ) => ((V k).velocity ⟨0, ⋯⟩).toLp) : CauchySeq fun (k : ℕ) => fieldPath (V k).velocity ⋯

theorem EulerOrdinarySobolev.Evolution.all_order_bounds_of_h3 {T : ℝ} {hT : 0 ≤ T} (V : ℕ → Evolution T hT) (M : ℝ) (hM : ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm 3 ((V k).velocity t) ≤ M) (hinit : ∀ (q : ℕ), ∃ (R : ℝ), ∀ (k : ℕ), tensorNorm q ((V k).velocity ⟨0, ⋯⟩) ≤ R) (q : ℕ) : ∃ (C : ℝ), ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm q ((V k).velocity t) ≤ C

noncomputable def EulerOrdinarySobolev.limitEvolutionOfH3 {T : ℝ} {hT : 0 ≤ T} (V : ℕ → Evolution T hT) (hpos : 0 < T) (M : ℝ) (hM : ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm 3 ((V k).velocity t) ≤ M) (hinit : ∀ (q : ℕ), ∃ (R : ℝ), ∀ (k : ℕ), tensorNorm q ((V k).velocity ⟨0, ⋯⟩) ≤ R) (hcauchy : CauchySeq fun (k : ℕ) => ((V k).velocity ⟨0, ⋯⟩).toLp) : Evolution T hT

Limit evolution of H3, given by limitEvolution V hpos (Evolution.all_order_bounds_of_h3 V M hM hinit) (Evolution.cauchyPath_of_initial V M hM hcauchy).

Equations

• EulerOrdinarySobolev.limitEvolutionOfH3 V hpos M hM hinit hcauchy = EulerOrdinarySobolev.limitEvolution V hpos ⋯ ⋯

theorem EulerOrdinarySobolev.limitEvolutionOfH3_convergence {T : ℝ} {hT : 0 ≤ T} (V : ℕ → Evolution T hT) (hpos : 0 < T) (M : ℝ) (hM : ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm 3 ((V k).velocity t) ≤ M) (hinit : ∀ (q : ℕ), ∃ (R : ℝ), ∀ (k : ℕ), tensorNorm q ((V k).velocity ⟨0, ⋯⟩) ≤ R) (hcauchy : CauchySeq fun (k : ℕ) => ((V k).velocity ⟨0, ⋯⟩).toLp) (q : ℕ) : Filter.Tendsto (fun (k : ℕ) => jetPath (V k).velocity ⋯ q) Filter.atTop (nhds (jetPath (limitEvolutionOfH3 V hpos M hM hinit hcauchy).velocity ⋯ q))

theorem EulerOrdinarySobolev.limitEvolutionOfH3_initial {T : ℝ} {hT : 0 ≤ T} (V : ℕ → Evolution T hT) (hpos : 0 < T) (M : ℝ) (hM : ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm 3 ((V k).velocity t) ≤ M) (hinit : ∀ (q : ℕ), ∃ (R : ℝ), ∀ (k : ℕ), tensorNorm q ((V k).velocity ⟨0, ⋯⟩) ≤ R) (hcauchy : CauchySeq fun (k : ℕ) => ((V k).velocity ⟨0, ⋯⟩).toLp) (u0 : ↥EulerMeanSolenoidal.L2) (hu0 : Filter.Tendsto (fun (k : ℕ) => ((V k).velocity ⟨0, ⋯⟩).toLp) Filter.atTop (nhds u0)) : ((limitEvolutionOfH3 V hpos M hM hinit hcauchy).velocity ⟨0, ⋯⟩).toLp = u0