The actual viscous term vanishes uniformly for a uniformly Sobolev-bounded approximation family.

noncomputable def EulerViscosityDefect.viscositySequence (n : ℕ) : ℝ

A concrete strictly positive sequence of viscosities tending to zero.

Equations

• EulerViscosityDefect.viscositySequence n = 1 / (↑n + 1)

theorem EulerViscosityDefect.viscositySequence_pos (n : ℕ) : 0 < viscositySequence n

Each concrete approximation viscosity is strictly positive.

theorem EulerViscosityDefect.viscositySequence_le_one (n : ℕ) : viscositySequence n ≤ 1

Each concrete approximation viscosity lies in the fixed unit interval.

theorem EulerViscosityDefect.viscositySequence_tendsto : Filter.Tendsto viscositySequence Filter.atTop (nhds 0)

The actual chosen viscosity sequence converges to zero.

noncomputable def EulerViscosityDefect.viscousDefect (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (ν T : ℝ) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period))

The literal viscosity times the spatial Laplacian, as a continuous L² time path.

Equations

• EulerViscosityDefect.viscousDefect period hq ν T e = ν • (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerSobolevHeatGenerator.laplacianEvaluation period q hq)) e

theorem EulerViscosityDefect.viscousDefect_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (ν T : ℝ) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : ‖viscousDefect period hq ν T e‖ ≤ 4 * |ν| * ‖e‖

The actual viscous PDE term is uniformly bounded by the complete Sobolev path norm.

theorem EulerViscosityDefect.viscousDefect_tendsto_zero (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (T M : ℝ) (e : ℕ → C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (he : ∀ (n : ℕ), ‖e n‖ ≤ M) : Filter.Tendsto (fun (n : ℕ) => viscousDefect period hq (viscositySequence n) T (e n)) Filter.atTop (nhds 0)

Every uniformly bounded genuine Sobolev approximation family has a uniformly vanishing viscous PDE defect.