The normalized Gaussian on ordinary three-dimensional space. The estimates below concern the literal Bochner integral, including its L²-to-uniform bound. The parameterization exp(-|x|²/t) has heat generator one quarter of the Laplacian.

noncomputable def EulerWholeSpaceGaussian.normalization (t : ℝ) : ℝ

Normalization, given by (Real.pi*t)^(-(3:ℝ)/2).

Equations

• EulerWholeSpaceGaussian.normalization t = (Real.pi * t) ^ (-3 / 2)

noncomputable def EulerWholeSpaceGaussian.kernel (t : ℝ) (x : EulerSmoothLimit.Space) : ℝ

Kernel, given by normalization t * Real.exp (-t⁻¹*‖x‖^2).

Equations

• EulerWholeSpaceGaussian.kernel t x = EulerWholeSpaceGaussian.normalization t * Real.exp (-t⁻¹ * ‖x‖ ^ 2)

theorem EulerWholeSpaceGaussian.normalization_pos {t : ℝ} (ht : 0 < t) : 0 < normalization t

theorem EulerWholeSpaceGaussian.kernel_pos {t : ℝ} (ht : 0 < t) (x : EulerSmoothLimit.Space) : 0 < kernel t x

theorem EulerWholeSpaceGaussian.kernel_nonneg {t : ℝ} (ht : 0 < t) (x : EulerSmoothLimit.Space) : 0 ≤ kernel t x

theorem EulerWholeSpaceGaussian.kernel_le_normalization {t : ℝ} (ht : 0 < t) (x : EulerSmoothLimit.Space) : kernel t x ≤ normalization t

theorem EulerWholeSpaceGaussian.kernel_smooth (t : ℝ) : ContDiff ℝ (↑⊤) (kernel t)

theorem EulerWholeSpaceGaussian.exp_integrable {b : ℝ} (hb : 0 < b) : MeasureTheory.Integrable (fun (x : EulerSmoothLimit.Space) => Real.exp (-b * ‖x‖ ^ 2)) MeasureTheory.volume

theorem EulerWholeSpaceGaussian.kernel_integrable {t : ℝ} (ht : 0 < t) : MeasureTheory.Integrable (kernel t) MeasureTheory.volume

theorem EulerWholeSpaceGaussian.integral_kernel {t : ℝ} (ht : 0 < t) : ∫ (x : EulerSmoothLimit.Space), kernel t x = 1

theorem EulerWholeSpaceGaussian.kernel_sq_integrable {t : ℝ} (ht : 0 < t) : MeasureTheory.Integrable (fun (x : EulerSmoothLimit.Space) => kernel t x ^ 2) MeasureTheory.volume

theorem EulerWholeSpaceGaussian.kernel_memLp {t : ℝ} (ht : 0 < t) : MeasureTheory.MemLp (kernel t) 2 MeasureTheory.volume

theorem EulerWholeSpaceGaussian.integral_kernel_sq_le {t : ℝ} (ht : 0 < t) : ∫ (x : EulerSmoothLimit.Space), kernel t x ^ 2 ≤ normalization t

theorem EulerWholeSpaceGaussian.sqrt_normalization {t : ℝ} (ht : 0 < t) : √(normalization t) = (Real.pi * t) ^ (-3 / 4)

theorem EulerWholeSpaceGaussian.sqrt_normalization_le {t : ℝ} (ht : 0 < t) : √(normalization t) ≤ t ^ (-3 / 4)

noncomputable def EulerWholeSpaceGaussian.average {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (t : ℝ) (f : EulerSmoothLimit.Space → V) (x : EulerSmoothLimit.Space) : V

The actual whole-space Gaussian average, with no periodic identification.

Equations

• EulerWholeSpaceGaussian.average t f x = ∫ (y : EulerSmoothLimit.Space), EulerWholeSpaceGaussian.kernel t y • f (x + y)

theorem EulerWholeSpaceGaussian.average_integrable_of_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {t : ℝ} (ht : 0 < t) (f : EulerSmoothLimit.Space → V) (hf : Continuous f) (C : ℝ) (hb : ∀ (x : EulerSmoothLimit.Space), ‖f x‖ ≤ C) (x : EulerSmoothLimit.Space) : MeasureTheory.Integrable (fun (y : EulerSmoothLimit.Space) => kernel t y • f (x + y)) MeasureTheory.volume

theorem EulerWholeSpaceGaussian.average_norm_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {t : ℝ} (ht : 0 < t) (f : EulerSmoothLimit.Space → V) (C : ℝ) (hb : ∀ (x : EulerSmoothLimit.Space), ‖f x‖ ≤ C) (x : EulerSmoothLimit.Space) : ‖average t f x‖ ≤ C

theorem EulerWholeSpaceGaussian.norm_integral_smul_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (k : EulerSmoothLimit.Space → ℝ) (f : EulerSmoothLimit.Space → V) (hk : MeasureTheory.MemLp k 2 MeasureTheory.volume) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ‖∫ (x : EulerSmoothLimit.Space), k x • f x‖ ≤ √(∫ (x : EulerSmoothLimit.Space), ‖k x‖ ^ 2) * (MeasureTheory.eLpNorm f 2 MeasureTheory.volume).toReal

Cauchy--Schwarz for scalar multiplication, in a form that retains the ordinary L² norm of a Banach-valued field.

theorem EulerWholeSpaceGaussian.average_norm_le_L2 {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {t : ℝ} (ht : 0 < t) (f : EulerSmoothLimit.Space → V) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (x : EulerSmoothLimit.Space) : ‖average t f x‖ ≤ t ^ (-3 / 4) * (MeasureTheory.eLpNorm f 2 MeasureTheory.volume).toReal

The three-dimensional smoothing power t^(-3/4) is proved from the normalized Gaussian density and the ordinary whole-space L² norm.

theorem EulerWholeSpaceGaussian.average_smoothField_norm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {t : ℝ} (ht : 0 < t) (A : EulerLpTranslation.SmoothL2Field V) (x : EulerSmoothLimit.Space) : ‖average t A.field x‖ ≤ t ^ (-3 / 4) * ‖A.toLp‖