Intervals and tails of real Gaussian distributions

Three estimates for the real Gaussian distribution gaussianReal μ v:

• Peak density. The density is largest at the mean, where it is 1 / √(2πv) (gaussianPDFReal_le), so a nondegenerate Gaussian gives each set at most 1 / √(2πv) times its Lebesgue measure (gaussianReal_le_ofReal_mul_volume).
• Anderson's inequality on the line. Among the intervals of a given length, the one centered at the mean has the largest mass (gaussianReal_Icc_le). For an interval [c - w, c + w] with c ≥ μ, the two intervals share [c - w, μ + w], and translation by 2 w carries the rest [μ - w, c - w] of the centered interval onto the rest [μ + w, c + w] of the shifted one, without increasing the density there.
• Chebyshev's inequality. The deviation from the mean is at least c with probability at most v / c ^ 2 (gaussianReal_meas_ge_le).

Main results

• ProbabilityTheory.gaussianPDFReal_le: the Gaussian density is at most 1 / √(2πv).
• ProbabilityTheory.gaussianReal_le_ofReal_mul_volume: the Gaussian measure of a set is at most 1 / √(2πv) times its Lebesgue measure.
• ProbabilityTheory.gaussianReal_Icc_le: Anderson's inequality on the line.
• ProbabilityTheory.gaussianReal_meas_ge_le: Chebyshev's inequality for a Gaussian.

theorem ProbabilityTheory.gaussianPDFReal_le (μ : ℝ) (v : NNReal) (x : ℝ) : gaussianPDFReal μ v x ≤ (√(2 * Real.pi * ↑v))⁻¹

The Gaussian density is at most its value 1 / √(2πv) at the mean.

theorem ProbabilityTheory.gaussianReal_le_ofReal_mul_volume (μ : ℝ) {v : NNReal} (hv : v ≠ 0) (s : Set ℝ) : (gaussianReal μ v) s ≤ ENNReal.ofReal (√(2 * Real.pi * ↑v))⁻¹ * MeasureTheory.volume s

A nondegenerate Gaussian gives each set at most the peak density 1 / √(2πv) times its Lebesgue measure.

theorem ProbabilityTheory.gaussianReal_Icc_le (μ : ℝ) (v : NNReal) (c w : ℝ) : (gaussianReal μ v) (Set.Icc (c - w) (c + w)) ≤ (gaussianReal μ v) (Set.Icc (μ - w) (μ + w))

Anderson's inequality on the line. A Gaussian gives an interval of radius w the most mass when it is centered at the mean.

theorem ProbabilityTheory.gaussianReal_meas_ge_le (μ : ℝ) (v : NNReal) {c : ℝ} (hc : 0 < c) : (gaussianReal μ v) {x : ℝ | c ≤ |x - μ|} ≤ ENNReal.ofReal (↑v / c ^ 2)

Chebyshev's inequality for a Gaussian. A Gaussian deviates from its mean by at least c > 0 with probability at most v / c ^ 2.