Density and pairing helpers for Euclidean Lᵖ

This file records the approximation facts used when an operator is first defined on its L² carrier and then extended to lower exponents. The approximants are continuous and compactly supported; in particular they are in every finite Lᵖ space. The pairing estimates are stated in the real integral form supplied by Hölder's inequality, which is convenient when passing a distributional identity to the limit.

theorem CKN.Foundation.Euclidean.memLp_exists_compactSupportContinuous_approx {p : ENNReal} (hp : p ≠ ⊤) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : ∃ (g : ℕ → Parabolic.Vec3 → ℝ), (∀ (n : ℕ), HasCompactSupport (g n) ∧ Continuous (g n) ∧ MeasureTheory.MemLp (g n) p MeasureTheory.volume ∧ MeasureTheory.MemLp (g n) 2 MeasureTheory.volume) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f - g n) p MeasureTheory.volume) Filter.atTop (nhds 0)

Every finite-exponent Lᵖ function has continuous compactly supported approximants converging in eLpNorm. Each approximant is also in L².

theorem CKN.Foundation.Euclidean.memLp_exists_compactSupportContinuous_approx_real {p : ℝ} : 1 ≤ p → ∀ {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume), ∃ (g : ℕ → Parabolic.Vec3 → ℝ), (∀ (n : ℕ), HasCompactSupport (g n) ∧ Continuous (g n) ∧ MeasureTheory.MemLp (g n) (ENNReal.ofReal p) MeasureTheory.volume ∧ MeasureTheory.MemLp (g n) 2 MeasureTheory.volume) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f - g n) (ENNReal.ofReal p) MeasureTheory.volume) Filter.atTop (nhds 0)

The preceding approximation theorem in the real-exponent notation used by the pressure extension: 1 ≤ p < ∞ and MemLp f (ENNReal.ofReal p).

theorem CKN.Foundation.Euclidean.integral_mul_test_le {p q : ℝ} (hpq : p.HolderConjugate q) {g ψ : Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g (ENNReal.ofReal p) MeasureTheory.volume) (hψ : MeasureTheory.MemLp ψ (ENNReal.ofReal q) MeasureTheory.volume) : ‖∫ (x : Parabolic.Vec3), g x * ψ x‖ ≤ (∫ (x : Parabolic.Vec3), ‖g x‖ ^ p) ^ (1 / p) * (∫ (x : Parabolic.Vec3), ‖ψ x‖ ^ q) ^ (1 / q)

Hölder's estimate for the pairing against a fixed Lq test function.

theorem CKN.Foundation.Euclidean.integral_mul_test_sub_le {p q : ℝ} (hpq : p.HolderConjugate q) {g h ψ : Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g (ENNReal.ofReal p) MeasureTheory.volume) (hh : MeasureTheory.MemLp h (ENNReal.ofReal p) MeasureTheory.volume) (hψ : MeasureTheory.MemLp ψ (ENNReal.ofReal q) MeasureTheory.volume) : ‖∫ (x : Parabolic.Vec3), (g x - h x) * ψ x‖ ≤ (∫ (x : Parabolic.Vec3), ‖g x - h x‖ ^ p) ^ (1 / p) * (∫ (x : Parabolic.Vec3), ‖ψ x‖ ^ q) ^ (1 / q)

Hölder's estimate for the difference of two pairings against a fixed Lq test function. This is the quantitative Lᵖ continuity used in the distributional limit.

theorem CKN.Foundation.Euclidean.integral_mul_continuousCompactSupport_le {p q : ℝ} (hpq : p.HolderConjugate q) {g ψ : Parabolic.Vec3 → ℝ} (hg : MeasureTheory.MemLp g (ENNReal.ofReal p) MeasureTheory.volume) (hψc : Continuous ψ) (hψs : HasCompactSupport ψ) : ‖∫ (x : Parabolic.Vec3), g x * ψ x‖ ≤ (∫ (x : Parabolic.Vec3), ‖g x‖ ^ p) ^ (1 / p) * (∫ (x : Parabolic.Vec3), ‖ψ x‖ ^ q) ^ (1 / q)

The pairing estimate when the test is continuous and compactly supported. Such a test is automatically in every finite Lq space.

theorem CKN.Foundation.Euclidean.ae_subsequence_of_eLpNorm_tendsto_zero {p : ENNReal} (hp : p ≠ 0) {f : ℕ → Parabolic.Vec3 → ℝ} {g : Parabolic.Vec3 → ℝ} (hfg : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) p MeasureTheory.volume) Filter.atTop (nhds 0)) : ∃ (ns : ℕ → ℕ), StrictMono ns ∧ ∀ᵐ (x : Parabolic.Vec3), Filter.Tendsto (fun (n : ℕ) => f (ns n) x) Filter.atTop (nhds (g x))

A sequence converging in Lᵖ has a strictly increasing subsequence which converges almost everywhere.

theorem CKN.Foundation.Euclidean.memLp_limit_of_cauchy {p : ENNReal} [hp : Fact (1 ≤ p)] {f : ℕ → Parabolic.Vec3 → ℝ} (hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) p MeasureTheory.volume) (hC : CauchySeq fun (n : ℕ) => MeasureTheory.MemLp.toLp (f n) ⋯) : ∃ (g : Parabolic.Vec3 → ℝ), MeasureTheory.MemLp g p MeasureTheory.volume ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) p MeasureTheory.volume) Filter.atTop (nhds 0)

A Cauchy sequence of Lᵖ representatives has a representative of its limit and converges to it in eLpNorm.