Compactness Representative

Supporting estimates for the Navier–Stokes development.

noncomputable def CKN.Leray.compactnessMollifiedLimit (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (σ : ℕ → ℕ) : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3

Successive limits of spatial mollifications define a field at every space-time point.

Equations

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

theorem CKN.Leray.measurable_compactnessMollifiedLimit (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (σ : ℕ → ℕ) (hu : ∀ (n : ℕ), Measurable (u n)) : Measurable (compactnessMollifiedLimit u σ)

The mollified limit is jointly measurable for every sequence of jointly measurable fields.