Sufficient statistics and the factorization theorem

DefinitionSufficient sub-σ-algebra#✓fully proved

A sub-σ-algebra m is sufficient for the family of measures P on (Ω, m₀) if m ≤ m₀, every P θ is finite, and for every m₀-measurable set s one m-measurable function is a version of the conditional probability P_θ[1_s | m] under every P θ. Bundling m ≤ m₀ and finiteness into the predicate means an IsSufficient hypothesis itself represents a sufficient sub-σ-algebra for statistical laws: the conditional expectations it mentions are genuine, not Mathlib's totalized fallback on unrelated σ-algebras or infinite measures.

def IsSufficient (m : MeasurableSpace Ω) {m₀ : MeasurableSpace Ω}
    (P : Θ → Measure[m₀] Ω) : Prop :=
  m ≤ m₀ ∧ (∀ θ, IsFiniteMeasure (P θ)) ∧
    ∀ s, MeasurableSet[m₀] s → ∃ f : Ω → ℝ, StronglyMeasurable[m] f ∧
      ∀ θ, f =ᵐ[P θ] (P θ)[s.indicator (fun _ => (1 : ℝ)) | m]

Used by 6

Used byThe Rao–Blackwell theorem · The Rao–Blackwell theorem for a sufficient statistic · Common conditional expectation under a sufficient σ-algebra · Halmos–Savage factorization, necessity · Factorization criterion, sufficiency direction, for a statistic, under an extra σ-finiteness hypothesis · Factorization implies sufficiency

TheoremCommon conditional expectation under a sufficient σ-algebra#✓fully proved

If m is sufficient for a family of probability measures, every m₀-measurable real function W that is integrable under all the measures has one m-measurable version of the conditional expectation P_θ[W | m] for every θ. (Measurability of W itself, not only under each P θ, is what lets one approximating sequence serve every parameter.)

theorem IsSufficient.exists_common_condExp {m m₀ : MeasurableSpace Ω}
    {P : Θ → Measure[m₀] Ω} [∀ θ, IsProbabilityMeasure (P θ)] (hP : IsSufficient m P)
    {W : Ω → ℝ} (hWm : Measurable[m₀] W) (hW : ∀ θ, Integrable W (P θ)) :
    ∃ η : Ω → ℝ, StronglyMeasurable[m] η ∧ ∀ θ, η =ᵐ[P θ] (P θ)[W | m]

Uses 1 · Used by 2

Statement usesSufficient sub-σ-algebra

Used byThe Rao–Blackwell theorem · The Rao–Blackwell theorem for a sufficient statistic

TheoremFactorization implies sufficiency#✓fully proved

Factorization implies sufficiency (Halmos–Savage, the sufficiency half). If every P θ has a density g θ with respect to one measure ν that is σ-finite on m, and each g θ is m-measurable, then m is sufficient for P.

theorem isSufficient_of_withDensity {m m₀ : MeasurableSpace Ω} (hm : m ≤ m₀)
    (ν : Measure[m₀] Ω) [SigmaFinite (ν.trim hm)] {P : Θ → Measure[m₀] Ω}
    [∀ θ, IsFiniteMeasure (P θ)] (g : Θ → Ω → ℝ≥0∞) (hg : ∀ θ, Measurable[m] (g θ))
    (hP : ∀ θ, P θ = ν.withDensity (g θ)) : IsSufficient m P

Uses 1 · Used by 1

Statement usesSufficient sub-σ-algebra

Used byFactorization criterion, sufficiency direction, for a statistic, under an extra σ-finiteness hypothesis

TheoremFactorization criterion, sufficiency direction, for a statistic, under an extra σ-finiteness hypothesis#✓fully proved

Factorization criterion, sufficiency direction, for a statistic, under an extra σ-finiteness hypothesis. If dP_θ/dμ = g_θ(T) · h with g_θ and h measurable and h · μ σ-finite on the σ-algebra generated by T, then T is sufficient for P.

The σ-finiteness hypothesis on (μ.withDensity h).trim (comap T) is an extra, nonstandard assumption, named in the theorem: it is strictly stronger than μ being σ-finite, since restriction to a sub-σ-algebra need not preserve σ-finiteness, and it can fail even when μ is σ-finite and h is a density. This theorem is therefore the factorization criterion under that extra hypothesis, not the classical criterion as stated. Removing the hypothesis would require a different proof.

theorem isSufficient_comap_of_factorization_of_sigmaFinite_trim {τ : Type*} [MeasurableSpace τ]
    {m₀ : MeasurableSpace Ω} {T : Ω → τ} (hT : Measurable T) (μ : Measure[m₀] Ω)
    {P : Θ → Measure[m₀] Ω} [∀ θ, IsFiniteMeasure (P θ)] (g : Θ → τ → ℝ≥0∞)
    (hg : ∀ θ, Measurable (g θ)) (h : Ω → ℝ≥0∞) (hh : Measurable h)
    [SigmaFinite ((μ.withDensity h).trim hT.comap_le)]
    (hP : ∀ θ, P θ = μ.withDensity (fun ω => g θ (T ω) * h ω)) :
    IsSufficient (MeasurableSpace.comap T ‹MeasurableSpace τ›) P

Sources

• Halmos and Savage (1949); Lehmann–Romano, Chapter 2.

Uses 2

Statement usesSufficient sub-σ-algebra

Proof usesFactorization implies sufficiency

DefinitionSufficient statistic for a discrete family#✓fully proved

A statistic T : X → τ is sufficient for the discrete family P : Θ → PMF X if the conditional probability P θ x / P_θ(T = T x) of x given T = T x is the same under any two parameters θ, θ' for which {T = T x} has positive probability. Here P_θ(T = t) = (P θ).map T t.

def IsSufficientPMF (P : Θ → PMF X) (T : X → τ) : Prop :=
  ∀ θ θ' x, (P θ).map T (T x) ≠ 0 → (P θ').map T (T x) ≠ 0 →
    P θ x / (P θ).map T (T x) = P θ' x / (P θ').map T (T x)

Used by 3

Used byFactorization, necessity · The Fisher–Neyman factorization theorem · Factorization, sufficiency

TheoremFactorization, necessity#✓fully proved

If T is sufficient for P, then P θ x = g θ (T x) * h x with g θ t = P_θ(T = t) and a parameter-free h with values in [0, 1].

theorem IsSufficientPMF.factorization {P : Θ → PMF X} {T : X → τ}
    (hT : IsSufficientPMF P T) :
    ∃ h : X → ℝ≥0, (∀ x, h x ≤ 1) ∧
      ∀ θ x, P θ x = (P θ).map T (T x) * (h x : ℝ≥0∞)

Uses 1 · Used by 1

Statement usesSufficient statistic for a discrete family

Used byThe Fisher–Neyman factorization theorem

TheoremFactorization, sufficiency#✓fully proved

If P θ x = g θ (T x) * h x for nonnegative real g, h with h free of θ, then T is sufficient for P.

theorem isSufficientPMF_of_factorization {P : Θ → PMF X} {T : X → τ} (g : Θ → τ → ℝ≥0)
    (h : X → ℝ≥0) (hP : ∀ θ x, P θ x = ((g θ (T x) * h x : ℝ≥0) : ℝ≥0∞)) :
    IsSufficientPMF P T

Uses 1 · Used by 1

Statement usesSufficient statistic for a discrete family

Used byThe Fisher–Neyman factorization theorem

TheoremThe Fisher–Neyman factorization theorem#✓fully proved

The Fisher–Neyman factorization theorem (discrete case). A statistic T is sufficient for the family of mass functions P if and only if there are nonnegative functions g and h, with h free of the parameter, such that P θ x = g θ (T x) * h x for every θ, x.

theorem isSufficientPMF_iff_exists_factorization (P : Θ → PMF X) (T : X → τ) :
    IsSufficientPMF P T ↔ ∃ (g : Θ → τ → ℝ≥0) (h : X → ℝ≥0),
      ∀ θ x, P θ x = ((g θ (T x) * h x : ℝ≥0) : ℝ≥0∞)

Sources

• Neyman (1935); Casella–Berger, Theorem 6.2.6.

Uses 3

Statement usesSufficient statistic for a discrete family

Proof usesFactorization, necessity · Factorization, sufficiency

TheoremHalmos–Savage factorization, necessity#●ready to prove

If the family of probability measures P is dominated by a σ-finite measure μ and the statistic T is sufficient for P, then the densities factor as dP_θ/dμ = g_θ(T) · h with measurable g_θ and h, h free of θ.

public theorem_wanted exists_factorization_of_isSufficient_comap {Ω Θ τ : Type*}
    [MeasurableSpace τ] {m₀ : MeasurableSpace Ω} {T : Ω → τ} (hT : Measurable T)
    (μ : Measure[m₀] Ω) [SigmaFinite μ] (P : Θ → Measure[m₀] Ω)
    [∀ θ, IsProbabilityMeasure (P θ)] (hdom : ∀ θ, P θ ≪ μ)
    (hP : IsSufficient (MeasurableSpace.comap T ‹MeasurableSpace τ›) P) :
    ∃ (g : Θ → τ → ℝ≥0∞) (h : Ω → ℝ≥0∞), (∀ θ, Measurable (g θ)) ∧ Measurable h ∧
      ∀ θ, P θ = μ.withDensity (fun ω => g θ (T ω) * h ω)

Sources

• P. R. Halmos and L. J. Savage, Application of the Radon–Nikodym theorem to the theory of sufficient statistics, Ann. Math. Statist. 20 (1949), 225–241.

Uses 1

Statement usesSufficient sub-σ-algebra

8 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.