Compactness Weak Lower #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.eLpNorm_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 : ℕ), MeasureTheory.eLpNorm (f k) 2 μ ≤ B)
:
A finite uniform L² seminorm bound passes to a weak Hilbert-space limit with the same constant.