A fixed shrinking compact mollifier and distributional scalar harmonicity.

Actual compact mollification on R³ is smooth and contractive on scalar L².

noncomputable def EulerMeanHarmonic.scalarMollification (φ : ContDiffBump 0) (f : EulerSmoothLimit.Space → ℝ) : EulerSmoothLimit.Space → ℝ

Scalar mollification, given by φ.normed volume ⋆[ContinuousLinearMap.lsmul ℝ ℝ, volume] f.

Equations

• EulerMeanHarmonic.scalarMollification φ f = MeasureTheory.convolution (φ.normed MeasureTheory.volume) f (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

theorem EulerMeanHarmonic.scalarMollification_smooth (φ : ContDiffBump 0) (f : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ContDiff ℝ (↑⊤) (scalarMollification φ f)

theorem EulerMeanHarmonic.scalarMollification_sq_le (φ : ContDiffBump 0) (f : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (x : EulerSmoothLimit.Space) : scalarMollification φ f x ^ 2 ≤ scalarMollification φ (fun (y : EulerSmoothLimit.Space) => f y ^ 2) x

The elementary variance inequality for the actual normalized convolution.

theorem EulerMeanHarmonic.scalarMollification_sq_integrable (φ : ContDiffBump 0) (f : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : EulerSmoothLimit.Space) => scalarMollification φ f x ^ 2) MeasureTheory.volume

theorem EulerMeanHarmonic.scalarMollification_memLp (φ : ContDiffBump 0) (f : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.MemLp (scalarMollification φ f) 2 MeasureTheory.volume

theorem EulerMeanHarmonic.scalarMollification_energy_le (φ : ContDiffBump 0) (f : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.lpNorm (scalarMollification φ f) 2 MeasureTheory.volume ^ 2 ≤ MeasureTheory.lpNorm f 2 MeasureTheory.volume ^ 2

theorem EulerMeanHarmonic.scalarMollification_norm_le (φ : ContDiffBump 0) (f : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.lpNorm (scalarMollification φ f) 2 MeasureTheory.volume ≤ MeasureTheory.lpNorm f 2 MeasureTheory.volume

def EulerMeanHarmonic.ScalarWeakHarmonicOn (U : Set EulerSmoothLimit.Space) (f : EulerSmoothLimit.Space → ℝ) : Prop

Harmonicity tested against genuine smooth compactly supported scalar functions.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EulerMeanHarmonic.interiorMollifier (n : ℕ) : ContDiffBump 0

Interior mollifier, bundling rIn, rOut, rIn_pos, rIn_lt_rOut and the required compatibility proofs.

Equations

• EulerMeanHarmonic.interiorMollifier n = { rIn := 1 / 16 * EulerNoncompactTransport.cutoffScale n, rOut := 1 / 8 * EulerNoncompactTransport.cutoffScale n, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

theorem EulerMeanHarmonic.interiorMollifier_rOut_le (n : ℕ) : (interiorMollifier n).rOut ≤ 1 / 4

theorem EulerMeanHarmonic.interiorMollifier_rOut_tendsto : Filter.Tendsto (fun (n : ℕ) => (interiorMollifier n).rOut) Filter.atTop (nhds 0)

theorem EulerMeanHarmonic.interiorMollifier_shape (n : ℕ) : (interiorMollifier n).rOut ≤ 2 * (interiorMollifier n).rIn

theorem EulerMeanHarmonic.scalarMollification_ae_tendsto (f : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ∀ᵐ (x : EulerSmoothLimit.Space), Filter.Tendsto (fun (n : ℕ) => scalarMollification (interiorMollifier n) f x) Filter.atTop (nhds (f x))

The classical smooth convolutions recover every scalar L² function almost everywhere.

theorem EulerMeanHarmonic.ae_bound_of_scalarMollification_bound (f : EulerSmoothLimit.Space → ℝ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (U : Set EulerSmoothLimit.Space) (C : ℝ) (hbound : ∀ (n : ℕ), ∀ x ∈ U, scalarMollification (interiorMollifier n) f x ^ 2 ≤ C) : ∀ᵐ (x : EulerSmoothLimit.Space), x ∈ U → f x ^ 2 ≤ C

A uniform squared pointwise bound passes from these genuine mollifiers to f.