The ball Poincare inequality for representative-level W^{1,p} functions

The proof uses interior mollification on compactly contained balls and then exhausts the original ball.

theorem CKN.integral_rpow_norm_eq_lpNorm_rpow {p : ENNReal} (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) {f : Vec 3 → ℝ} {μ : MeasureTheory.Measure (Vec 3)} (hf : MeasureTheory.MemLp f p μ) : ∫ (x : Vec 3), ‖f x‖ ^ p.toReal ∂μ = MeasureTheory.lpNorm f p μ ^ p.toReal

theorem CKN.tendsto_integral_rpow_norm_of_tendsto_lpNorm {p : ENNReal} (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) {f : Vec 3 → ℝ} {μ : MeasureTheory.Measure (Vec 3)} (hf : MeasureTheory.MemLp f p μ) {g : ℕ → Vec 3 → ℝ} (hg : ∀ (n : ℕ), MeasureTheory.MemLp (g n) p μ) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.lpNorm (g n) p μ) Filter.atTop (nhds (MeasureTheory.lpNorm f p μ))) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : Vec 3), ‖g n x‖ ^ p.toReal ∂μ) Filter.atTop (nhds (∫ (x : Vec 3), ‖f x‖ ^ p.toReal ∂μ))

theorem CKN.tendsto_lpNorm_zero_of_tendsto_eLpNorm_zero {p : ENNReal} {μ : MeasureTheory.Measure (Vec 3)} {f : ℕ → Vec 3 → ℝ} (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n) p μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.lpNorm (f n) p μ) Filter.atTop (nhds 0)