Compactness Approx

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.tendsto_lintegral_prod_sq_of_uniform {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {E : Type u_3} [NormedAddCommGroup E] [ContinuousENorm E] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {f : ℕ → α × β → E} {g : α × β → E} (hconv : ∀ (ε : ENNReal), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (z : α × β), ‖f n z - g z‖ₑ ≤ ε) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (z : α × β), ‖f n z - g z‖ₑ ^ 2 ∂μ.prod ν) Filter.atTop (nhds 0)

Uniform convergence of measurable scalar fields on a finite product measure space implies convergence of their integrated squared errors. This is the estimate used for each fixed finite-rank spatial approximation.