InformationTheory.Shannon.StamGaussianBound

Imports 6

Stam convex Fisher bound — Gaussian instance #

EPI follow-up to the Stam inequality core J(X+Y) ≤ λ² J(X) + (1-λ)² J(Y).

Keyed on the V2 Fisher information fisherInfoOfMeasureV2, which evaluates to the closed form 1/v for a Gaussian with variance v. The proof reduces the convex Fisher bound to the arithmetic kernel 1/(a+b) ≤ λ²/a + (1-λ)²/b, with equality at λ* = a/(a+b).

Scope: only the Gaussian instance. The general case (heat-flow + de Bruijn) is out of scope here.

Main statements #

stam_fisher_arith — arithmetic kernel 1/(a+b) ≤ λ²/a + (1-λ)²/b
stam_fisher_arith_eq_at_opt — equality at λ* = a/(a+b)
stam_convex_fisher_bound_gaussian — Gaussian convex Fisher bound (closed form)
stam_convex_fisher_bound_gaussian_indep — independent-RV form via gaussianReal_add_gaussianReal_of_indepFun

§1 — Arithmetic kernel (Gaussian-independent) #

theorem

InformationTheory.Shannon.FisherInfo.stam_fisher_arith

source

(a b lam : ℝ) (ha : 0 < a) (hb : 0 < b) (hlo : 0 ≤ lam) (hhi : lam ≤ 1) :

1 / (a + b) ≤ lam ^ 2 / a + (1 - lam) ^ 2 / b

The Stam arithmetic kernel. For positive a, b and λ ∈ [0,1], 1/(a+b) ≤ λ²/a + (1-λ)²/b. This is the pure real-number content of the convex Fisher bound after substituting the Gaussian closed form J(𝒩(m,v)) = 1/v.

The difference λ²(a+b)b + (1-λ)²(a+b)a − ab equals (a − λ(a+b))², hence is ≥ 0; equality holds exactly at λ = a/(a+b).

Used by

§2 — Gaussian convex Fisher bound (V2-keyed, non-vacuous) #

theorem

InformationTheory.Shannon.FisherInfo.stam_convex_fisher_bound_gaussian

source

(m₁ m₂ : ℝ) {v₁ v₂ : NNReal} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) (lam : ℝ) (hlo : 0 ≤ lam) (hhi : lam ≤ 1) :

(fisherInfoOfMeasureV2 (ProbabilityTheory.gaussianReal (m₁ + m₂) (v₁ + v₂)) (ProbabilityTheory.gaussianPDFReal (m₁ + m₂) (v₁ + v₂))).toReal ≤ lam ^ 2 * (fisherInfoOfMeasureV2 (ProbabilityTheory.gaussianReal m₁ v₁) (ProbabilityTheory.gaussianPDFReal m₁ v₁)).toReal + (1 - lam) ^ 2 * (fisherInfoOfMeasureV2 (ProbabilityTheory.gaussianReal m₂ v₂) (ProbabilityTheory.gaussianPDFReal m₂ v₂)).toReal

The Gaussian Stam convex Fisher bound. For Gaussian laws 𝒩(m₁,v₁), 𝒩(m₂,v₂) with v₁, v₂ ≠ 0, the V2 Fisher information of the sum law 𝒩(m₁+m₂, v₁+v₂) satisfies J(X+Y) ≤ λ² J(X) + (1-λ)² J(Y) for every λ ∈ [0,1]. Each Fisher info evaluates to the closed form 1/v via fisherInfoOfMeasureV2_gaussianReal.

Used by