A common short interval for an Euler family with Cauchy initial H3 data. A fixed tail member supplies the reference solution; the actual stability theorem supplies the uniform H3 bound needed by the limit.

theorem EulerOrdinarySobolev.tensorNorm_le_sub_add (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (s : ℕ) : tensorNorm s A ≤ tensorNorm s (fieldSub A B) + tensorNorm s B

theorem EulerOrdinarySobolev.Evolution.short_uniform_h3 {T : ℝ} {hT : 0 ≤ T} (V : ℕ → Evolution T hT) (hpos : 0 < T) (hCauchy : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (i : ℕ), N ≤ i → ∀ (j : ℕ), N ≤ j → tensorNorm 3 (fieldSub ((V i).velocity ⟨0, ⋯⟩) ((V j).velocity ⟨0, ⋯⟩)) ≤ ε) : ∃ (L : ℝ) (hL : 0 < L) (hLT : L ≤ T) (N : ℕ) (M : ℝ), ∀ (n : ℕ) (t : ↑(Set.Icc 0 L)), tensorNorm 3 (((V (n + N)).restrictTime L ⋯ hLT).velocity t) ≤ M

theorem EulerOrdinarySobolev.exists_local_evolution_of_cauchy {T : ℝ} {hT : 0 ≤ T} (V : ℕ → Evolution T hT) (hpos : 0 < T) (hCauchy : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ (i : ℕ), N ≤ i → ∀ (j : ℕ), N ≤ j → tensorNorm 3 (fieldSub ((V i).velocity ⟨0, ⋯⟩) ((V j).velocity ⟨0, ⋯⟩)) ≤ ε) (hinit : ∀ (q : ℕ), ∃ (R : ℝ), ∀ (n : ℕ), tensorNorm q ((V n).velocity ⟨0, ⋯⟩) ≤ R) (u0 : ↥EulerMeanSolenoidal.L2) (hu0 : Filter.Tendsto (fun (n : ℕ) => ((V n).velocity ⟨0, ⋯⟩).toLp) Filter.atTop (nhds u0)) : ∃ (L : ℝ) (hL : 0 < L), L ≤ T ∧ ∃ (E : Evolution L ⋯), (E.velocity ⟨0, ⋯⟩).toLp = u0