Stability Slice Zero

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_ae_slice_integral_zero_of_setIntegral_tendsto {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (F : ℕ → X × ℝ → ℝ) (G : X × ℝ → ℝ) (hF : ∀ (n : ℕ), MeasureTheory.Integrable (F n) (μ.prod ν)) (hG : MeasureTheory.Integrable G (μ.prod ν)) (hzero : ∀ (n : ℕ), ∀ᵐ (t : ℝ) ∂ν, ∫ (x : X), F n (x, t) ∂μ = 0) (hconv : ∀ (s : Set ℝ), MeasurableSet s → ν s < ⊤ → Filter.Tendsto (fun (n : ℕ) => ∫ (z : X × ℝ) in Set.univ ×ˢ s, F n z ∂μ.prod ν) Filter.atTop (nhds (∫ (z : X × ℝ) in Set.univ ×ˢ s, G z ∂μ.prod ν))) : ∀ᵐ (t : ℝ) ∂ν, ∫ (x : X), G (x, t) ∂μ = 0

A space-time integral limit preserves a zero identity on almost every time slice, provided it holds for the approximants and every measurable time restriction.