Local Energy Mollifier Convergence

Local energy identities and limit passages for the endpoint regularity proof.

theorem ESS.localEnergyConvergenceVolumeIsAddHaarMeasure : MeasureTheory.volume.IsAddHaarMeasure

theorem ESS.localEnergyConvergenceVolumeIsAddLeftInvariant : MeasureTheory.volume.IsAddLeftInvariant

@[reducible, inline]

abbrev ESS.LocalEnergyVec4 : Type

The four-dimensional Euclidean coordinate space for local energy integrals.

Equations

• ESS.LocalEnergyVec4 = CKN.Vec 4

def ESS.localEnergySpaceTimeCoord : LocalEnergyVec4 ≃ᵐ CKN.Foundation.Parabolic.Vec3 × ℝ

The measurable identification of four coordinates with space followed by time.

Equations

• ESS.localEnergySpaceTimeCoord = (MeasurableEquiv.piFinSuccAbove (fun (x : Fin 4) => ℝ) (Fin.last 3)).trans MeasurableEquiv.prodComm

theorem ESS.localEnergy_spaceTimeMollify_eLpNorm_le {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {δ : ℝ} {p : ENNReal} (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hδ : 0 < δ) (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : MeasureTheory.eLpNorm (CKN.spaceTimeMollify f δ hδ) p MeasureTheory.volume ≤ MeasureTheory.eLpNorm f p MeasureTheory.volume

The space-time kernel contracts every finite-exponent Lebesgue norm, by transport to four Euclidean coordinates and the normalized convolution estimate.

theorem ESS.tendsto_eLpNorm_sub_zero_spaceTimeMollify_lp {g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {p : ENNReal} (hp : 1 ≤ p) (hpTop : p ≠ ⊤) (hg : MeasureTheory.MemLp g p MeasureTheory.volume) {ε : ℕ → ℝ} (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) (hε_pos : ∀ (n : ℕ), 0 < ε n) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spaceTimeMollify g (ε n) ⋯ x - g x) p MeasureTheory.volume) Filter.atTop (nhds 0)