A countable dense family of solenoidal test fields

The space J of def:leray-hopf has a countable set of smooth compactly supported solenoidal fields that is dense in the L² sense. This lets the pressure-free weak equation be tested against every element of J at almost every time (lem:lps-H1-estimate).

def ESS.LpsSolenoidalTest : Set (CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3)

Smooth compactly supported solenoidal vector fields.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev ESS.LpsVecL2 : Type

The L² space of vector fields on ℝ³.

Equations

• ESS.LpsVecL2 = ↥(MeasureTheory.Lp (Fin 3 → ℝ) 2 MeasureTheory.volume)

theorem ESS.lps_exists_countable_solenoidal_dense : ∃ (D : Set (CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3)), D.Countable ∧ D ⊆ LpsSolenoidalTest ∧ ∀ (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3), CKN.IsInJ w → ∀ (ε : ENNReal), 0 < ε → ∃ ψ ∈ D, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => ψ x - w x) 2 MeasureTheory.volume < ε

Countably many smooth compactly supported solenoidal fields approximate every element of J in L².