Rao–Blackwell theorem

TheoremIntegrability of a convex loss of a conditional expectation#✓fully proved

For a convex loss L, L ∘ μ[W | m] is integrable whenever W and L ∘ W are.

theorem integrable_comp_condExp {m m₀ : MeasurableSpace Ω} (hm : m ≤ m₀)
    (μ : Measure[m₀] Ω) [IsProbabilityMeasure μ] {L : ℝ → ℝ} (hL : ConvexOn ℝ Set.univ L)
    {W : Ω → ℝ} (hW : Integrable W μ) (hLW : Integrable (fun ω => L (W ω)) μ) :
    Integrable (fun ω => L (μ[W | m] ω)) μ

Used by 1

Used byRao–Blackwell inequality for one law

TheoremRao–Blackwell inequality for one law#✓fully proved

For a convex loss L and an integrable W with integrable loss, ∫ L(μ[W | m]) dμ ≤ ∫ L(W) dμ.

theorem integral_comp_condExp_le {m m₀ : MeasurableSpace Ω} (hm : m ≤ m₀)
    (μ : Measure[m₀] Ω) [IsProbabilityMeasure μ] {L : ℝ → ℝ} (hL : ConvexOn ℝ Set.univ L)
    {W : Ω → ℝ} (hW : Integrable W μ) (hLW : Integrable (fun ω => L (W ω)) μ) :
    ∫ ω, L (μ[W | m] ω) ∂μ ≤ ∫ ω, L (W ω) ∂μ

Uses 1 · Used by 1

Proof usesIntegrability of a convex loss of a conditional expectation

Used byThe Rao–Blackwell theorem

TheoremSquared-error decomposition#✓fully proved

For W with a finite second moment and any target c, E (W - c)² = E (μ[W | m] - c)² + E (W - μ[W | m])². This is the Pythagorean identity MeasureTheory.integral_sq_sub_eq_integral_sq_sub_condExp_add with the constant predictor fun _ => c, with the two summands commuted; it is not a second Pythagorean proof.

theorem integral_sq_sub_eq_add {m m₀ : MeasurableSpace Ω} (hm : m ≤ m₀)
    (μ : Measure[m₀] Ω) [IsProbabilityMeasure μ] {W : Ω → ℝ} (hW : MemLp W 2 μ) (c : ℝ) :
    ∫ ω, (W ω - c) ^ 2 ∂μ =
      ∫ ω, (μ[W | m] ω - c) ^ 2 ∂μ + ∫ ω, (W ω - μ[W | m] ω) ^ 2 ∂μ

Uses 1 · Used by 2

Proof usesPythagorean identity for the conditional mean

Used byEquality case under squared error · The Rao–Blackwell theorem for a sufficient statistic

TheoremEquality case under squared error#✓fully proved

Conditioning leaves the squared-error risk at c unchanged if and only if W already equals μ[W | m] almost everywhere.

theorem integral_sq_sub_condExp_eq_iff {m m₀ : MeasurableSpace Ω} (hm : m ≤ m₀)
    (μ : Measure[m₀] Ω) [IsProbabilityMeasure μ] {W : Ω → ℝ} (hW : MemLp W 2 μ) (c : ℝ) :
    ∫ ω, (μ[W | m] ω - c) ^ 2 ∂μ = ∫ ω, (W ω - c) ^ 2 ∂μ ↔ W =ᵐ[μ] μ[W | m]

Uses 1

Proof usesSquared-error decomposition

TheoremThe Rao–Blackwell theorem#✓fully proved

Let m be sufficient for the family of probability measures P, and let W be a measurable estimator that is integrable under every P θ. There is one parameter-free m-measurable estimator η, a version of P_θ[W | m] for every θ, with the same mean as W under every θ and no larger risk under every loss ℓ θ that is convex in the estimate (for which ℓ θ ∘ W is integrable).

theorem IsSufficient.raoBlackwell {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]) ∧
      (∀ θ, ∫ ω, η ω ∂P θ = ∫ ω, W ω ∂P θ) ∧
      ∀ ℓ : Θ → ℝ → ℝ, ∀ θ, ConvexOn ℝ Set.univ (ℓ θ) →
        Integrable (fun ω => ℓ θ (W ω)) (P θ) →
        ∫ ω, ℓ θ (η ω) ∂P θ ≤ ∫ ω, ℓ θ (W ω) ∂P θ

Sources

• Rao (1945); Blackwell (1947); Casella–Berger, Section 7.3.

Uses 3

Statement usesSufficient sub-σ-algebra

Proof usesCommon conditional expectation under a sufficient σ-algebra · Rao–Blackwell inequality for one law

TheoremThe Rao–Blackwell theorem for a sufficient statistic#✓fully proved

If the statistic T is sufficient for P and W is a measurable estimator with finite second moment under every P θ, there is a measurable φ such that φ ∘ T is a version of every E_θ[W | T], has the same mean as W, and for every target τ θ satisfies E_θ (W - τ θ)² = E_θ (φ(T) - τ θ)² + E_θ (W - φ(T))².

theorem raoBlackwell_comap {τ : Type*} [MeasurableSpace τ] {m₀ : MeasurableSpace Ω}
    {T : Ω → τ} (hT : Measurable T) {P : Θ → Measure[m₀] Ω} [∀ θ, IsProbabilityMeasure (P θ)]
    (hP : IsSufficient (MeasurableSpace.comap T ‹MeasurableSpace τ›) P) {W : Ω → ℝ}
    (hWm : Measurable[m₀] W) (hW : ∀ θ, MemLp W 2 (P θ)) (tgt : Θ → ℝ) :
    ∃ φ : τ → ℝ, Measurable φ ∧
      (∀ θ, (fun ω => φ (T ω)) =ᵐ[P θ] (P θ)[W | MeasurableSpace.comap T ‹_›]) ∧
      (∀ θ, ∫ ω, φ (T ω) ∂P θ = ∫ ω, W ω ∂P θ) ∧
      ∀ θ, ∫ ω, (W ω - tgt θ) ^ 2 ∂P θ =
        ∫ ω, (φ (T ω) - tgt θ) ^ 2 ∂P θ + ∫ ω, (W ω - φ (T ω)) ^ 2 ∂P θ

Uses 3

Statement usesSufficient sub-σ-algebra

Proof usesCommon conditional expectation under a sufficient σ-algebra · Squared-error decomposition

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.