InformationTheory.Shannon.FisherInfo.DeBruijnAssembly.Core

Imports 5

Chain-rule and regularity helpers for the per-time assembly #

The named lemmas below are the regularity and chain-rule plumbing the assembly calls to build each atom of debruijnIdentityV2_holds_assembled. Convention: pPath σ x := convDensityAdd pX (gaussianPDFReal 0 ⟨σ, _⟩) x.

theorem

InformationTheory.Shannon.FisherInfo.debruijnIdentityV2_holds_assembled_chain_entDeriv_formula

source

(pX : ℝ → ℝ) {t : ℝ} (ht : 0 < t) (x D : ℝ) (hpos : EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) x ≠ 0) (hpath_deriv : HasDerivAt (fun (s : ℝ) => EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨max s 0, ⋯⟩) x) D t) :

HasDerivAt (fun (s : ℝ) => (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨max s 0, ⋯⟩) x).negMulLog) ((-Real.log (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) x) - 1) * D) t

The per-x entropy-integrand chain rule: at x with pPath t x ≠ 0, (d/ds) negMulLog (pPath s x)|_{s=t} = (- log (pPath t x) - 1) · D, where D is the σ-derivative ∂_s pPath t x supplied as a HasDerivAt witness. Derived via HasDerivAt.comp from Real.hasDerivAt_negMulLog.

@audit:ok

Used by

theorem

InformationTheory.Shannon.FisherInfo.gaussianPDFReal_le_prefactor'

source

(v : NNReal) (u : ℝ) :

ProbabilityTheory.gaussianPDFReal 0 v u ≤ (√(2 * Real.pi * ↑v))⁻¹

The centered Gaussian density is bounded above by its normalizing prefactor (√(2πv))⁻¹.

@audit:ok

Used by

theorem

InformationTheory.Shannon.FisherInfo.convDensityAdd_logFactor_poly_majorant

source

(pX : ℝ → ℝ) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (_hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_mass : ∫ (y : ℝ), pX y = 1) {t : ℝ} (ht : 0 < t) :

∃ (A : ℝ) (B : ℝ), 0 ≤ B ∧ ∀ᵐ (x : ℝ), ∀ (s : ℝ) (hs : s ∈ Set.Ioo (t / 2) (2 * t)), ‖-Real.log (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩) x) - 1‖ ≤ A + B * x ^ 2

On the neighborhood Set.Ioo (t/2) (2*t), the entropy log-factor - log (p_s x) - 1 of the convolution density p_s = convDensityAdd pX g_s admits an s-uniform polynomial-in-x² majorant ‖- log (p_s x) - 1‖ ≤ A + B·x² with B ≥ 0. The upper bound comes from the s-uniform Gaussian lower bound on p_s (convDensityAdd_lower_bound_gaussian_uniformR); the lower bound from the prefactor upper bound on p_s (convDensityAdd_le_prefactor).

@audit:ok

Used by

The `s`-uniform Gaussian-Hessian majorant `gaussHessMaj t` #

noncomputable def

InformationTheory.Shannon.FisherInfo.gaussHessMaj

source

(t u : ℝ) :

ℝ

The s-uniform Gaussian-Hessian kernel majorant on the window s ∈ (t/2, 2t): g_s(u) · |u²/s² − 1/s| ≤ gaussHessMaj t u := (√(πt))⁻¹ · exp(−u²/(4t)) · (4u²/t² + 2/t), a Gaussian times a quadratic.

@audit:ok

Equations

InformationTheory.Shannon.FisherInfo.gaussHessMaj t u = (√(Real.pi * t))⁻¹ * Real.exp (-u ^ 2 / (4 * t)) * (4 * u ^ 2 / t ^ 2 + 2 / t)

Instances For

Used by

theorem

InformationTheory.Shannon.FisherInfo.gaussHessMaj_nonneg

source

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

0 ≤ gaussHessMaj t u

gaussHessMaj t is nonnegative. @audit:ok

Used by

theorem

InformationTheory.Shannon.FisherInfo.gaussHessMaj_bdd

source

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

gaussHessMaj t u ≤ (√(Real.pi * t))⁻¹ * (16 * Real.exp (-1) / t + 2 / t)

gaussHessMaj t is globally bounded.

@audit:ok

Used by

theorem

InformationTheory.Shannon.FisherInfo.gaussHessMaj_integrable

source

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

MeasureTheory.Integrable (gaussHessMaj t) MeasureTheory.volume

gaussHessMaj t is Lebesgue-integrable (Gaussian × quadratic). @audit:ok

Used by

theorem

InformationTheory.Shannon.FisherInfo.gaussHessMaj_polyWeight_integrable

source

{t : ℝ} (ht : 0 < t) (a b : ℝ) :

MeasureTheory.Integrable (fun (u : ℝ) => (a + b * u ^ 2) * gaussHessMaj t u) MeasureTheory.volume

For any constants a b : ℝ, the polynomial-weighted majorant (a + b·u²) · gaussHessMaj t u is Lebesgue-integrable (a Gaussian times a quartic).

@audit:ok

Used by

theorem

InformationTheory.Shannon.FisherInfo.gaussHessMaj_polyWeight_bdd

source

{t : ℝ} (ht : 0 < t) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (u : ℝ) :

(a + b * u ^ 2) * gaussHessMaj t u ≤ a * ((√(Real.pi * t))⁻¹ * (16 * Real.exp (-1) / t + 2 / t)) + b * ((√(Real.pi * t))⁻¹ * (256 * Real.exp (-1) ^ 2 + 8 * Real.exp (-1)))

For nonneg constants a b, the polynomial-weighted majorant (a + b·u²) · gaussHessMaj t u is globally bounded by an explicit constant.

@audit:ok

Used by

theorem

InformationTheory.Shannon.FisherInfo.gaussianHess_le_gaussHessMaj

source

{t : ℝ} (ht : 0 < t) {s : ℝ} (hs : s ∈ Set.Ioo (t / 2) (2 * t)) (u : ℝ) :

ProbabilityTheory.gaussianPDFReal 0 ⟨s, ⋯⟩ u * |u ^ 2 / s ^ 2 - 1 / s| ≤ gaussHessMaj t u

s-uniform pointwise majorant: for s ∈ (t/2, 2t), g_s(u)·|u²/s² − 1/s| ≤ gaussHessMaj t u. @audit:ok

Used by

theorem

InformationTheory.Shannon.FisherInfo.convKernel_envelope_integrable

source

(pX K : ℝ → ℝ) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_meas : Measurable pX) (hK_int : MeasureTheory.Integrable K MeasureTheory.volume) (hK_meas : Measurable K) :

MeasureTheory.Integrable (fun (x : ℝ) => ∫ (y : ℝ), pX y * K (x - y)) MeasureTheory.volume

For an integrable kernel K and an integrable density pX, the convolution-shaped function x ↦ ∫ y, pX y · K (x − y) is Lebesgue-integrable, via Tonelli on the product measure.

@audit:ok

Used by

theorem

InformationTheory.Shannon.FisherInfo.convDensityAdd_envelope_integrable

source

(pX K : ℝ → ℝ) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_meas : Measurable pX) (hK_int : MeasureTheory.Integrable K MeasureTheory.volume) (hK_meas : Measurable K) :

MeasureTheory.Integrable (EPIConvDensity.convDensityAdd pX K) MeasureTheory.volume

Public re-export of convKernel_envelope_integrable on the convDensityAdd shape, so downstream IsRegularDensityV2 producers can reuse it without the private helper: Integrable (convDensityAdd pX K) volume.

@audit:ok

Used by