Common-interval smooth Euler limits under a uniform bound on the actual time integral of the velocity gradient. The H³ bound, all higher bounds, and path Cauchy convergence are derived from the true equations.

noncomputable def EulerOrdinarySobolev.gradientTensorBound (R G : ℝ) : ℝ

Gradient tensor bound, given by wordCount 3*Real.sqrt (wordCount 3*R^2*Real.exp (gradientEnergyConstant*G)).

Equations

• EulerOrdinarySobolev.gradientTensorBound R G = EulerOrdinarySobolev.wordCount 3 * √(EulerOrdinarySobolev.wordCount 3 * R ^ 2 * Real.exp (EulerOrdinarySobolev.gradientEnergyConstant * G))

theorem EulerOrdinarySobolev.Evolution.h3_tensorNorm_gradient_uniform {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (R G : ℝ) (hR : tensorNorm 3 (U.velocity ⟨0, ⋯⟩) ≤ R) (hG : ∀ (t : ↑(Set.Icc 0 T)), U.gradientIntegral t ≤ G) (t : ↑(Set.Icc 0 T)) : tensorNorm 3 (U.velocity t) ≤ gradientTensorBound R G

theorem EulerOrdinarySobolev.Evolution.cauchyPath_of_initial_gradient {T : ℝ} {hT : 0 ≤ T} (V : ℕ → Evolution T hT) (G : ℝ) (hG : ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), (V k).gradientIntegral t ≤ G) (hinit : CauchySeq fun (k : ℕ) => ((V k).velocity ⟨0, ⋯⟩).toLp) : CauchySeq fun (k : ℕ) => fieldPath (V k).velocity ⋯

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

Limit evolution of gradient integral, constructed using limitEvolution.

Equations

• EulerOrdinarySobolev.limitEvolutionOfGradientIntegral V hpos R G hR hG hinit hcauchy = EulerOrdinarySobolev.limitEvolution V hpos ⋯ ⋯

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

theorem EulerOrdinarySobolev.limitEvolutionOfGradientIntegral_initial {T : ℝ} {hT : 0 ≤ T} (V : ℕ → Evolution T hT) (hpos : 0 < T) (R G : ℝ) (hR : ∀ (k : ℕ), tensorNorm 3 ((V k).velocity ⟨0, ⋯⟩) ≤ R) (hG : ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), (V k).gradientIntegral t ≤ G) (hinit : ∀ (q : ℕ), ∃ (C : ℝ), ∀ (k : ℕ), tensorNorm q ((V k).velocity ⟨0, ⋯⟩) ≤ C) (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)) : ((limitEvolutionOfGradientIntegral V hpos R G hR hG hinit hcauchy).velocity ⟨0, ⋯⟩).toLp = u0