Density extension for weighted Carleman inequalities

This module extends smooth compactly supported inequalities to compactly supported fields with space-time weak derivatives (lem:carleman-sobolev of the Escauriaza–Seregin–Šverák manuscript).

theorem CKN.zeroExtend_spaceTimeData_memLp {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) {w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Dw : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {D2w : Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → Foundation.Parabolic.Vec3} {Dtw : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hderiv : HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw) (hL2 : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) : MeasureTheory.MemLp (zeroExtendField (Ω ×ˢ I) fun (q : Foundation.Parabolic.Vec3 × ℝ) => w (Foundation.Parabolic.parabolicHomeomorph.symm q)) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (zeroExtendField (Ω ×ˢ I) fun (q : Foundation.Parabolic.Vec3 × ℝ) => Dw (Foundation.Parabolic.parabolicHomeomorph.symm q)) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (zeroExtendField (Ω ×ˢ I) fun (q : Foundation.Parabolic.Vec3 × ℝ) => D2w (Foundation.Parabolic.parabolicHomeomorph.symm q)) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (zeroExtendField (Ω ×ˢ I) fun (q : Foundation.Parabolic.Vec3 × ℝ) => Dtw (Foundation.Parabolic.parabolicHomeomorph.symm q)) 2 MeasureTheory.volume

Finite space-time L² data give global L² zero extensions of the field and its weak derivatives (lem:carleman-sobolev, ESS).

theorem CKN.memLp_pi_component {X : Type u_1} {ι : Type u_2} {E : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [Fintype ι] {μ : MeasureTheory.Measure X} {f : X → ι → E} {p : ENNReal} (hf : MeasureTheory.MemLp f p μ) (i : ι) : MeasureTheory.MemLp (fun (x : X) => f x i) p μ

A finite-coordinate projection preserves MemLp (lem:carleman-sobolev, ESS).

theorem CKN.weightedSq_tendsto {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {ρ : X → ℝ} {C : ℝ} (hC : 0 ≤ C) (hρ : MeasureTheory.AEStronglyMeasurable ρ μ) (hρbound : ∀ᵐ (x : X) ∂μ, ‖ρ x‖ ≤ C) {f : X → ℝ} {fseq : ℕ → X → ℝ} (hf : MeasureTheory.MemLp f 2 μ) (hfseq : ∀ (n : ℕ), MeasureTheory.MemLp (fseq n) 2 μ) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fseq n - f) 2 μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : X), ρ x * fseq n x ^ 2 ∂μ) Filter.atTop (nhds (∫ (x : X), ρ x * f x ^ 2 ∂μ))

A bounded measurable weight preserves quadratic integral convergence under L² convergence (lem:carleman-sobolev, ESS).

theorem CKN.spaceTimeMollifyPi_mem_spaceTimeTestFunction {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {f : Foundation.Parabolic.Vec3 × ℝ → Fin 3 → ℝ} {δ : ℝ} (hδ : 0 < δ) (hf : HasCompactSupport f) (hthick : Metric.closedBall 0 δ + tsupport f ⊆ Ω ×ˢ I) (hloc : ∀ (i : Fin 3), MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.Vec3 × ℝ) => f x i) MeasureTheory.volume) : spaceTimeMollifyPi f δ hδ ∈ spaceTimeTestFunction Ω I

A componentwise space-time mollification is a smooth compactly supported test field when its closed support neighborhood remains inside the product domain (lem:carleman-sobolev, ESS).

theorem CKN.exists_spaceTimeMollifyPi_testSequence {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) {f : Foundation.Parabolic.Vec3 × ℝ → Fin 3 → ℝ} (hf : HasCompactSupport f) (hfsupport : tsupport f ⊆ Ω ×ˢ I) (hloc : ∀ (i : Fin 3), MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.Vec3 × ℝ) => f x i) MeasureTheory.volume) : ∃ (δ : ℕ → ℝ), Filter.Tendsto δ Filter.atTop (nhds 0) ∧ ∀ (n : ℕ), 0 < δ n ∧ ∀ (hδ : 0 < δ n), spaceTimeMollifyPi f (δ n) hδ ∈ spaceTimeTestFunction Ω I

A compactly supported field in an open product domain admits a sequence of smooth compactly supported mollifications in that same domain, with radii tending to zero (lem:carleman-sobolev, ESS).