InformationTheory.Shannon.FisherInfo.Gaussian

Imports 9

Fisher information — Gaussian discharge #

Discharges the IsRegularDensity predicate of FisherInfo/Basic.lean for the Gaussian case: the smooth representative is the closed-form gaussianPDFReal m v, and the differentiability, positivity, tail-vanishing, and integrability conditions are verified from it.

Main definitions #

isRegularDensity_gaussianReal_of_law — the IsRegularDensity instance for a Gaussian random variable.

Main statements #

pdf_toReal_ae_eq_gaussianPDFReal — (pdf X P volume).toReal =ᵐ gaussianPDFReal m v.
differentiable_gaussianPDFReal / deriv_gaussianPDFReal / logDeriv_gaussianPDFReal — differentiation lemmas for the Gaussian PDF in closed form.
tendsto_gaussianPDFReal_atBot / tendsto_gaussianPDFReal_atTop — tail vanishing.
integrable_deriv_gaussianPDFReal / integral_deriv_gaussianPDFReal_eq_zero — the derivative is integrable and integrates to 0.

The `IsRegularDensity` instance for Gaussian densities #

theorem

InformationTheory.Shannon.pdf_toReal_ae_eq_gaussianPDFReal

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} (X : Ω → ℝ) [MeasureTheory.HasPDF X P MeasureTheory.volume] {m : ℝ} {v : NNReal} (hX_law : MeasureTheory.Measure.map X P = ProbabilityTheory.gaussianReal m v) :

(fun (x : ℝ) => (MeasureTheory.pdf X P MeasureTheory.volume x).toReal) =ᵐ[MeasureTheory.volume ] fun (x : ℝ) => ProbabilityTheory.gaussianPDFReal m v x

(pdf X P volume).toReal =ᵐ[volume] gaussianPDFReal m v for a Gaussian X. Bridges MeasureTheory.pdf_def → rnDeriv_gaussianReal → toReal_gaussianPDF.

Used by

theorem

InformationTheory.Shannon.differentiable_gaussianPDFReal

source

(m : ℝ) (v : NNReal) :

Differentiable ℝ (ProbabilityTheory.gaussianPDFReal m v)

Differentiable ℝ (gaussianPDFReal m v) — the Gaussian pdf is smooth on all of ℝ.

Used by

theorem

InformationTheory.Shannon.deriv_gaussianPDFReal

source

{m : ℝ} {v : NNReal} (hv : v ≠ 0) (x : ℝ) :

deriv (ProbabilityTheory.gaussianPDFReal m v) x = -(x - m) / ↑v * ProbabilityTheory.gaussianPDFReal m v x

deriv (gaussianPDFReal m v) x = -(x - m)/v * gaussianPDFReal m v x.

Used by

theorem

InformationTheory.Shannon.tendsto_gaussianPDFReal_atBot

source

(m : ℝ) {v : NNReal} (hv : v ≠ 0) :

Filter.Tendsto (ProbabilityTheory.gaussianPDFReal m v) Filter.atBot (nhds 0)

gaussianPDFReal m v x → 0 as x → -∞.

Used by

theorem

InformationTheory.Shannon.tendsto_gaussianPDFReal_atTop

source

(m : ℝ) {v : NNReal} (hv : v ≠ 0) :

Filter.Tendsto (ProbabilityTheory.gaussianPDFReal m v) Filter.atTop (nhds 0)

Used by

theorem

InformationTheory.Shannon.integrable_sub_mul_gaussianPDFReal

source

(m : ℝ) {v : NNReal} (hv : v ≠ 0) :

MeasureTheory.Integrable (fun (x : ℝ) => (x - m) * ProbabilityTheory.gaussianPDFReal m v x) MeasureTheory.volume

(x - m) * gaussianPDFReal m v x is Lebesgue-integrable: this is the first moment integrand (against Lebesgue), expressible via integral_gaussianReal_eq_integral_smul.

Used by

theorem

InformationTheory.Shannon.integrable_deriv_gaussianPDFReal

source

(m : ℝ) {v : NNReal} (hv : v ≠ 0) :

MeasureTheory.Integrable (deriv (ProbabilityTheory.gaussianPDFReal m v)) MeasureTheory.volume

deriv (gaussianPDFReal m v) is Lebesgue-integrable.

Used by

theorem

InformationTheory.Shannon.integral_deriv_gaussianPDFReal_eq_zero

source

(m : ℝ) {v : NNReal} (hv : v ≠ 0) :

∫ (x : ℝ), deriv (ProbabilityTheory.gaussianPDFReal m v) x = 0

∫ deriv (gaussianPDFReal m v) x ∂volume = 0. Using deriv f = -(x-m)/v * f, this equals -(1/v) · ∫ (x - m) · f, and the latter is m - m = 0 because ∫ x · f = m (Gaussian mean) and ∫ f = 1.

Used by

noncomputable def