Pointwise control of the heat orbit and smooth approximation

At a fixed positive time the Gaussian kernel lies in every L^q, q ≥ 1, so Hölder's inequality bounds the heat orbit pointwise by the Lᵖ norm of the datum. Together with smooth compactly supported approximation in Lᵖ this gives the approximation step of lem:pv-heat-critical.

theorem ESS.heatKernel_memLp {t : ℝ} (ht : 0 < t) {q : ℝ} (hq : 1 ≤ q) : MeasureTheory.MemLp (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Heat.heatKernel y t) (ENNReal.ofReal q) MeasureTheory.volume

At a positive time the Gaussian kernel lies in L^q for every q ≥ 1.

theorem ESS.heatConv_integrable_enorm_le {p q : ℝ} (hpq : p.HolderConjugate q) {t : ℝ} (ht : 0 < t) {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume) (x : CKN.Foundation.Parabolic.Vec3) : MeasureTheory.Integrable (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Heat.heatKernel y t * f (x - y)) MeasureTheory.volume ∧ ‖CKN.Foundation.Heat.heatConv t f x‖ₑ ≤ MeasureTheory.eLpNorm (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Heat.heatKernel y t) (ENNReal.ofReal q) MeasureTheory.volume * MeasureTheory.eLpNorm f (ENNReal.ofReal p) MeasureTheory.volume

Hölder's inequality for the Gaussian convolution at one point: the integrand is integrable and the value is bounded by the kernel's L^q norm times the datum's Lᵖ norm.

theorem ESS.heatConv_sub_enorm_le {p q : ℝ} (hpq : p.HolderConjugate q) {t : ℝ} (ht : 0 < t) {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal p) MeasureTheory.volume) (hg : MeasureTheory.MemLp g (ENNReal.ofReal p) MeasureTheory.volume) (x : CKN.Foundation.Parabolic.Vec3) : ‖CKN.Foundation.Heat.heatConv t f x - CKN.Foundation.Heat.heatConv t g x‖ₑ ≤ MeasureTheory.eLpNorm (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Heat.heatKernel y t) (ENNReal.ofReal q) MeasureTheory.volume * MeasureTheory.eLpNorm (f - g) (ENNReal.ofReal p) MeasureTheory.volume

The Gaussian convolution is linear on Lᵖ data and Lipschitz for the Lᵖ norm at each point of positive time.

theorem ESS.vec3_exists_enorm_eq_component (v : CKN.Foundation.Parabolic.Vec3) : ∃ (k : Fin 3), ‖v‖ₑ = ‖v k‖ₑ

A vector in Vec3 has the extended norm of one of its components.

theorem ESS.heatOrbit_sub_enorm_le {p q : ℝ} (hpq : p.HolderConjugate q) {b b' : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hb : MeasureTheory.MemLp b (ENNReal.ofReal p) MeasureTheory.volume) (hb' : MeasureTheory.MemLp b' (ENNReal.ofReal p) MeasureTheory.volume) {x : CKN.Foundation.Parabolic.Vec3} {t : ℝ} (ht : 0 < t) : ‖heatOrbit b (x, t) - heatOrbit b' (x, t)‖ₑ ≤ MeasureTheory.eLpNorm (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Heat.heatKernel y t) (ENNReal.ofReal q) MeasureTheory.volume * MeasureTheory.eLpNorm (b - b') (ENNReal.ofReal p) MeasureTheory.volume

The heat orbit is Lipschitz in the datum for the Lᵖ norm, pointwise at every positive time.

theorem ESS.exists_smooth_compact_tendsto_eLpNorm {p : ENNReal} (hp1 : 1 ≤ p) (hp : p ≠ ⊤) {f : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : ∃ (g : ℕ → CKN.Foundation.Parabolic.Vec3 → ℝ), (∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n) ∧ HasCompactSupport (g n)) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (g n - f) p MeasureTheory.volume) Filter.atTop (nhds 0)

Every Lᵖ function, 1 ≤ p < ∞, is an Lᵖ limit of smooth compactly supported functions.