Stability Weighted Gradient Scalar #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.stability_weighted_gradient_scalar
{α : Type u_1}
[MeasurableSpace α]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(F : ℕ → α → ℝ)
(G ψ : α → ℝ)
(hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) 2 μ)
(hG : MeasureTheory.MemLp G 2 μ)
(hψ : MeasureTheory.MemLp ψ ⊤ μ)
(hψnonneg : ∀ᵐ (x : α) ∂μ, 0 ≤ ψ x)
(hweak :
∀ (w : α → ℝ),
MeasureTheory.MemLp w 2 μ →
Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), F n x * w x ∂μ) Filter.atTop (nhds (∫ (x : α), G x * w x ∂μ)))
:
A nonnegative bounded weight converts weak L² convergence into
convergence of the mixed energy and a weighted square inequality.