Explicit Gaussian kernels used by the heat operators. The probability theory needed to establish their mass stays in the proofs, while the kernel formulas remain transparent.

noncomputable def EulerGaussianCylinderHeat.gaussianDensity (μ : ℝ) (v : NNReal) (x : ℝ) : ℝ

The real Gaussian density with mean μ and variance v.

Equations

• EulerGaussianCylinderHeat.gaussianDensity μ v x = (√(2 * Real.pi * ↑v))⁻¹ * Real.exp (-(x - μ) ^ 2 / (2 * ↑v))

noncomputable def EulerGaussianCylinderHeat.gaussianMeasure (μ : ℝ) (v : NNReal) : MeasureTheory.Measure ℝ

The Gaussian measure, with a point mass when its variance is zero.

Equations

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

instance EulerGaussianCylinderHeat.instIsProbabilityMeasureRealGaussianMeasure (μ : ℝ) (v : NNReal) : MeasureTheory.IsProbabilityMeasure (gaussianMeasure μ v)

@[simp]

theorem EulerGaussianCylinderHeat.gaussianMeasure_zero_var (μ : ℝ) : gaussianMeasure μ 0 = MeasureTheory.Measure.dirac μ