Compactness Weak AELimit

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.ae_eq_of_weak_l2_and_ae_tendsto {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : ℕ → α → E) (g : α → E) (v : ↥(MeasureTheory.Lp E 2 μ)) (hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) 2 μ) (hg : MeasureTheory.MemLp g 2 μ) (hbound : ∃ B < ⊤, ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) 2 μ ≤ B) (hae : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))) (hweak : ∀ (w : ↥(MeasureTheory.Lp E 2 μ)), Filter.Tendsto (fun (n : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (f n) ⋯) w) Filter.atTop (nhds (inner ℝ v w))) : g =ᵐ[μ] fun (x : α) => ↑↑v x

A uniformly bounded L² sequence with a weak limit and an almost everywhere pointwise limit has the same limit in both senses.