Actual first and second Gaussian kernels and their integrable bounds.

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

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

Equations

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

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

First kernel, given by (-2*t⁻¹*⟪x,a⟫_ℝ) * kernel t x.

Equations

• EulerWholeSpaceGaussian.firstKernel t a x = -2 * t⁻¹ * inner ℝ x a * EulerWholeSpaceGaussian.kernel t x

noncomputable def EulerWholeSpaceGaussian.secondKernel (t : ℝ) (a b x : EulerSmoothLimit.Space) : ℝ

Second kernel, given by (4*t⁻¹^2*⟪x,a⟫_ℝ*⟪x,b⟫_ℝ - 2*t⁻¹*⟪a,b⟫_ℝ) * kernel t x.

Equations

• EulerWholeSpaceGaussian.secondKernel t a b x = (4 * t⁻¹ ^ 2 * inner ℝ x a * inner ℝ x b - 2 * t⁻¹ * inner ℝ a b) * EulerWholeSpaceGaussian.kernel t x

theorem EulerWholeSpaceGaussian.firstKernel_smooth (t : ℝ) (a : EulerSmoothLimit.Space) : ContDiff ℝ (↑⊤) (firstKernel t a)

theorem EulerWholeSpaceGaussian.secondKernel_smooth (t : ℝ) (a b : EulerSmoothLimit.Space) : ContDiff ℝ (↑⊤) (secondKernel t a b)

theorem EulerWholeSpaceGaussian.kernel_fderiv (t : ℝ) (a x : EulerSmoothLimit.Space) : (fderiv ℝ (kernel t) x) a = firstKernel t a x

theorem EulerWholeSpaceGaussian.firstKernel_fderiv (t : ℝ) (a b x : EulerSmoothLimit.Space) : (fderiv ℝ (firstKernel t a) x) b = secondKernel t a b x

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

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

theorem EulerWholeSpaceGaussian.integral_wideKernel {t : ℝ} (ht : 0 < t) : ∫ (x : EulerSmoothLimit.Space), wideKernel t x = 2 ^ (3 / 2)

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

theorem EulerWholeSpaceGaussian.norm_sq_kernel_le {t : ℝ} (ht : 0 < t) (x : EulerSmoothLimit.Space) : ‖x‖ ^ 2 * kernel t x ≤ 2 * t * wideKernel t x

A Gaussian absorbs its quadratic factor at twice the spatial variance.

theorem EulerWholeSpaceGaussian.norm_kernel_le {t : ℝ} (ht : 0 < t) (x : EulerSmoothLimit.Space) : ‖x‖ * kernel t x ≤ (1 + 2 * t) * wideKernel t x

theorem EulerWholeSpaceGaussian.firstKernel_bound {t : ℝ} (ht : 0 < t) (a x : EulerSmoothLimit.Space) : ‖firstKernel t a x‖ ≤ 2 * t⁻¹ * (1 + 2 * t) * ‖a‖ * wideKernel t x

theorem EulerWholeSpaceGaussian.secondKernel_bound {t : ℝ} (ht : 0 < t) (a b x : EulerSmoothLimit.Space) : ‖secondKernel t a b x‖ ≤ 10 * t⁻¹ * ‖a‖ * ‖b‖ * wideKernel t x

theorem EulerWholeSpaceGaussian.firstKernel_integrable {t : ℝ} (ht : 0 < t) (a : EulerSmoothLimit.Space) : MeasureTheory.Integrable (firstKernel t a) MeasureTheory.volume

theorem EulerWholeSpaceGaussian.secondKernel_integrable {t : ℝ} (ht : 0 < t) (a b : EulerSmoothLimit.Space) : MeasureTheory.Integrable (secondKernel t a b) MeasureTheory.volume

theorem EulerWholeSpaceGaussian.secondKernel_L1_bound {t : ℝ} (ht : 0 < t) (a b : EulerSmoothLimit.Space) : ∫ (x : EulerSmoothLimit.Space), ‖secondKernel t a b x‖ ≤ 10 * 2 ^ (3 / 2) * t⁻¹ * ‖a‖ * ‖b‖

The actual two-derivative Gaussian kernel has the essential 1/t L¹ bound.