Gaussian densities and complex-kernel estimates

For c > 0, the function t ↦ c exp (-(c t)²) / √π is the density of the centred Gaussian law of variance (2 c²)⁻¹, that is, of width c⁻¹. This file identifies the density with Mathlib’s Gaussian probability density and records that its total mass is one.

This file also records the complex Gaussian estimates needed to differentiate integrals against the translated kernel z ↦ exp (-(c (t - z))²) under the integral sign: a Gaussian bound in t, uniform for z in a ball, and the complex derivative in z.

Main definitions

• Real.gaussianDensity: the function t ↦ c exp (-(c t)²) / √π.

Main statements

• Real.gaussianDensity_eq_gaussianPDFReal: for c > 0 it is Mathlib's Gaussian density ProbabilityTheory.gaussianPDFReal with mean 0 and variance (2 c²)⁻¹.
• Real.integral_gaussianDensity: for c > 0 it has total mass one.
• Complex.norm_cexp_neg_mul_sub_sq_le: the Gaussian bound ‖exp (-(c (t - z))²)‖ ≤ exp (c² D²) exp (-(c² / 2) t²) for ‖z‖ ≤ D.
• Complex.hasDerivAt_cexp_neg_mul_sub_sq: the complex derivative of z ↦ exp (-(c (t - z))²).

noncomputable def Real.gaussianDensity (c t : ℝ) : ℝ

The real Gaussian density t ↦ c exp (-(c t)²) / √π of width c⁻¹. It is odd in c, and for c > 0 it is the density of the centred Gaussian law of variance (2 c²)⁻¹.

theorem Real.gaussianDensity_def (c t : ℝ) : c.gaussianDensity t = c * ((√Real.pi)⁻¹ * exp (-(c * t) ^ 2))

The defining formula of the Gaussian density.

theorem Real.gaussianDensity_nonneg {c : ℝ} (hc : 0 ≤ c) (t : ℝ) : 0 ≤ c.gaussianDensity t

For c ≥ 0 the Gaussian density is nonnegative.

theorem Real.gaussianDensity_eq_gaussianPDFReal {c : ℝ} (hc : 0 < c) : c.gaussianDensity = ProbabilityTheory.gaussianPDFReal 0 (2 * c ^ 2)⁻¹.toNNReal

For c > 0, the Gaussian density of width c⁻¹ is the centred Gaussian probability density of variance (2 c²)⁻¹.

theorem Real.integral_gaussianDensity {c : ℝ} (hc : 0 < c) : ∫ (t : ℝ), c.gaussianDensity t = 1

For c > 0, the Gaussian density of width c⁻¹ has total mass one.

theorem Complex.norm_cexp_neg_mul_sub_sq_le (c t : ℝ) {z : ℂ} {D : ℝ} (hz : ‖z‖ ≤ D) : ‖exp (-(↑c * (↑t - z)) ^ 2)‖ ≤ Real.exp (c ^ 2 * D ^ 2) * Real.exp (-(c ^ 2 / 2) * t ^ 2)

The Gaussian bound ‖exp (-(c (t - z))²)‖ ≤ exp (c² D²) exp (-(c² / 2) t²) for ‖z‖ ≤ D.

theorem Complex.hasDerivAt_cexp_neg_mul_sub_sq (c t : ℝ) (z : ℂ) : HasDerivAt (fun (z : ℂ) => exp (-(↑c * (↑t - z)) ^ 2)) (exp (-(↑c * (↑t - z)) ^ 2) * (2 * ↑c ^ 2 * (↑t - z))) z

The complex derivative of the translated Gaussian z ↦ exp (-(c (t - z))²).