InformationTheory.Shannon.SufficientStatistic

source

Imports 7

Sufficient statistics and mutual information (Cover-Thomas) #

If T is sufficient for θ (i.e., the chain X → T(X) → θ is Markov), then I(θ; X) = I(θ; T(X)).

Main definitions #

IsSufficientStatistic — sufficient statistic in markov-chain form: the chain Xs → f∘Xs → θ is a Markov chain, i.e., Xs ⊥ θ ∣ f(Xs).
IsSufficientStatisticFactorized — Neyman-Fisher factorization form: the conditional distribution of Xs given (f(Xs), θ) does not depend on θ.

Main statements #

mutualInfo_eq_of_sufficient — sufficiency implies I(θ; X) = I(θ; T(X)).
isSufficient_iff_factorized — equivalence of the two forms of sufficiency.

Implementation notes #

IsSufficientStatistic is defined in markov-chain form (matching the conclusion of mutualInfo_le_of_markov) rather than the Neyman-Fisher factorization form. This makes the main theorem close directly via mutualInfo_le_of_postprocess (the ≥ direction) and mutualInfo_le_of_markov + mutualInfo_comm (the ≤ direction) by le_antisymm.

Equivalence with the Neyman-Fisher form is proved via Mathlib's conditional independence API.

References #

T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

def

InformationTheory.Shannon.IsSufficientStatistic

source

{Ω : Type u_1} [MeasurableSpace Ω] {Θ : Type u_2} [MeasurableSpace Θ] {X : Type u_3} [MeasurableSpace X] {T' : Type u_4} [MeasurableSpace T'] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [StandardBorelSpace X] [Nonempty X] [StandardBorelSpace Θ] [Nonempty Θ] (θ : Ω → Θ) (Xs : Ω → X) (f : X → T') :

Prop

Sufficient statistic in markov-chain form: the chain Xs → f∘Xs → θ is a Markov chain, i.e., the statistic T(X) = f(X) separates Xs and θ (conditional independence Xs ⊥ θ ∣ T(X)).

Equivalence with the Neyman-Fisher factorization form is proved in isSufficient_iff_factorized. @audit:ok

Equations

InformationTheory.Shannon.IsSufficientStatistic μ θ Xs f = InformationTheory.Shannon.IsMarkovChain μ Xs (fun (ω : Ω) => f (Xs ω)) θ

Instances For

Used by

theorem

InformationTheory.Shannon.mutualInfo_eq_of_sufficient

source

{Ω : Type u_1} [MeasurableSpace Ω] {Θ : Type u_2} [MeasurableSpace Θ] {X : Type u_3} [MeasurableSpace X] {T' : Type u_4} [MeasurableSpace T'] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace X] [Nonempty X] [StandardBorelSpace Θ] [Nonempty Θ] (θ : Ω → Θ) (Xs : Ω → X) {f : X → T'} (hθ : Measurable θ) (hXs : Measurable Xs) (hf : Measurable f) (hsuff : IsSufficientStatistic μ θ Xs f) :

mutualInfo μ θ Xs = mutualInfo μ θ fun (ω : Ω) => f (Xs ω)

If T is sufficient for θ, then I(θ; X) = I(θ; T(X)).

IsSufficientStatistic is a structural precondition (the Markov chain property), not the conclusion itself. The proof is le_antisymm with the two directions from DPI. @audit:ok

Used by

Equivalence with the Neyman-Fisher factorization form #

def

InformationTheory.Shannon.IsSufficientStatisticFactorized

source

Prop

Sufficient statistic in Neyman-Fisher factorization form: the conditional distribution of Xs given (f(Xs), θ) does not depend on θ.

Concretely: condDistrib Xs (T(X), θ) =ᵃᵉ (condDistrib Xs T(X)).prodMkRight Θ. This is the measure-theoretic encoding of p(x ∣ θ) = g(T(x), θ) h(x). @audit:ok

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

theorem

InformationTheory.Shannon.isSufficient_iff_factorized

source

{Ω : Type u_1} [MeasurableSpace Ω] {Θ : Type u_2} [MeasurableSpace Θ] {X : Type u_3} [MeasurableSpace X] {T' : Type u_4} [MeasurableSpace T'] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace Ω] [StandardBorelSpace X] [Nonempty X] [StandardBorelSpace Θ] [Nonempty Θ] (θ : Ω → Θ) (Xs : Ω → X) {f : X → T'} (hθ : Measurable θ) (hXs : Measurable Xs) (hf : Measurable f) :

IsSufficientStatistic μ θ Xs f ↔ IsSufficientStatisticFactorized μ θ Xs f

Neyman-Fisher factorization theorem: the markov-chain form and the factorization form of sufficiency are equivalent (both express X ⊥ θ ∣ T(X)).

Proof via Mathlib's conditional independence API:

(A) IsSufficientStatistic (γ-form joint factorization) ↔ Xs ⟂ᵢ[f∘Xs] θ via condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib + compProd_eq_comp_prod.
(B) Xs ⟂ᵢ[f∘Xs] θ ↔ θ ⟂ᵢ[f∘Xs] Xs via CondIndepFun.symm.
(C) θ ⟂ᵢ[f∘Xs] Xs ↔ factorization form via condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight. @audit:ok

Used by