InformationTheory.Shannon.GaussianPDFVarianceDerivative

Imports 12

Gaussian PDF variance (time) derivative — de Bruijn FTC core #

The time-derivative half of the de Bruijn identity machinery: the heat equation ∂_t p = (1/2) Δ_x p for the Gaussian heat kernel.

The variance-derivative of gaussianPDFReal is not in Mathlib. This file builds it from scratch via the Real.exp / Real.sqrt chain rule and assembles the full heat equation for the Gaussian kernel.

Main definitions #

gaussianPDFRealVar — real-variance Gaussian density (√(2πv))⁻¹ · exp(−(x−m)²/(2v)).

Main statements #

gaussianPDFRealVar_eq_gaussianPDFReal — for v > 0, agrees with gaussianPDFReal m ⟨v, _⟩.
hasDerivAt_gaussianPDFRealVar_variance — variance-derivative: ∂_v gaussianPDFRealVar m v x = ((x−m)²/(2v²) − 1/(2v)) · gaussianPDFRealVar m v x.
hasDerivAt_heatKernel_time — time-derivative of the heat kernel: ∂_t g_t x = (1/2)(x²/t² − 1/t)·g_t x.
isHeatTimeDerivHyp_gaussian — IsHeatTimeDerivHyp for the Gaussian heat kernel with Δp = spatialLaplacianHeatKernel.

Real-variance Gaussian density #

noncomputable def

InformationTheory.Shannon.gaussianPDFRealVar

source

(m v x : ℝ) :

ℝ

The real-variance Gaussian density (√(2πv))⁻¹ · exp(−(x−m)²/(2v)).

This is gaussianPDFReal m v x with the variance v taken as a real number (rather than ℝ≥0), so that we can differentiate in v. For v > 0 it agrees with gaussianPDFReal m ⟨v, _⟩ (see gaussianPDFRealVar_eq_gaussianPDFReal).

Equations

InformationTheory.Shannon.gaussianPDFRealVar m v x = (√(2 * Real.pi * v))⁻¹ * Real.exp (-(x - m) ^ 2 / (2 * v))

Instances For

Used by

theorem

InformationTheory.Shannon.gaussianPDFRealVar_eq_gaussianPDFReal

source

(m : ℝ) {v : ℝ} (hv : 0 < v) (x : ℝ) :

gaussianPDFRealVar m v x = ProbabilityTheory.gaussianPDFReal m ⟨v, ⋯⟩ x

For v > 0, gaussianPDFRealVar agrees with gaussianPDFReal m ⟨v, _⟩.

Used by

Variance-derivative lemma (the Mathlib gap closure) #

theorem

InformationTheory.Shannon.hasDerivAt_gaussianNorm_variance

source

{v : ℝ} (hv : 0 < v) :

HasDerivAt (fun (v : ℝ) => (√(2 * Real.pi * v))⁻¹) (-(1 / (2 * v)) * (√(2 * Real.pi * v))⁻¹) v

The variance-derivative of the (√(2πv))⁻¹ normalising factor.

∂_v (√(2πv))⁻¹ = -(1/(2v)) · (√(2πv))⁻¹. The √ cancels: the log-derivative of (√(2πv))⁻¹ is rational.

Used by

theorem

InformationTheory.Shannon.hasDerivAt_gaussianExp_variance

source

(m x : ℝ) {v : ℝ} (hv : 0 < v) :

HasDerivAt (fun (v : ℝ) => Real.exp (-(x - m) ^ 2 / (2 * v))) ((x - m) ^ 2 / (2 * v ^ 2) * Real.exp (-(x - m) ^ 2 / (2 * v))) v

The variance-derivative of the exponential factor.

∂_v exp(−(x−m)²/(2v)) = ((x−m)²/(2v²)) · exp(−(x−m)²/(2v)).

Used by

theorem

InformationTheory.Shannon.hasDerivAt_gaussianPDFRealVar_variance

source

(m x : ℝ) {v : ℝ} (hv : 0 < v) :

HasDerivAt (fun (v : ℝ) => gaussianPDFRealVar m v x) (((x - m) ^ 2 / (2 * v ^ 2) - 1 / (2 * v)) * gaussianPDFRealVar m v x) v

The variance-derivative lemma (Mathlib-gap closure).

∂_v gaussianPDFRealVar m v x = ((x−m)²/(2v²) − 1/(2v)) · gaussianPDFRealVar m v x,

for v > 0. Proven from scratch via the Real.exp / Real.sqrt chain rule.

Used by

Heat-kernel time derivative (m = 0) #

theorem

InformationTheory.Shannon.hasDerivAt_heatKernel_time

source

{t : ℝ} (ht : 0 < t) (x : ℝ) :

HasDerivAt (fun (s : ℝ) => FisherInfo.heatKernel s x) (1 / 2 * FisherInfo.spatialLaplacianHeatKernel t x) t

The time-derivative of the Gaussian heat kernel.

∂_t g_t x = (1/2)(x²/t² − 1/t)·g_t x = (1/2) Δ_x g_t x, i.e. g_t solves the heat equation ∂_t p = (1/2) Δ_x p. This is the m = 0 specialization of hasDerivAt_gaussianPDFRealVar_variance, re-expressed against heatKernel and spatialLaplacianHeatKernel.

Used by