Compactness Energy Lower #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.lintegral_enorm_sq_le_of_weak_l2_bounded
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{μ : MeasureTheory.Measure α}
(f : ℕ → α → E)
(g : ↥(MeasureTheory.Lp E 2 μ))
(hf : ∀ (k : ℕ), MeasureTheory.MemLp (f k) 2 μ)
(hweak :
∀ (w : ↥(MeasureTheory.Lp E 2 μ)),
Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (f k) ⋯) w) Filter.atTop (nhds (inner ℝ g w)))
(B : ENNReal)
(hB : B < ⊤)
(hbound : ∀ (k : ℕ), ∫⁻ (x : α), ‖f k x‖ₑ ^ 2 ∂μ ≤ B)
:
An exact uniform squared-energy bound passes to a weak L² limit.