Monotonicity of conditional entropy under refinement of the σ-algebra

This file adds the monotonicity of conditional entropy to the conditional-entropy milestone (GitHub issue #13), continuing Oseledets.Entropy.CondPartition (which defines condEntropy μ 𝒜 s as the μ-average of the pointwise entropy against the regular conditional probability condExpKernel μ 𝒜 ω).

The single result is the conditional generalization of condEntropy_le ("conditioning does not increase entropy"): conditioning on a finer sub-σ-algebra reduces conditional entropy.

• condEntropy_mono_of_le: if 𝒜 ≤ ℬ ≤ mα then H(P | ℬ) ≤ H(P | 𝒜).

The proof runs the same Jensen argument as condEntropy_le, but with the conditional Jensen inequality (ConcaveOn.condExp_map_le) against the coarser σ-algebra 𝒜 in place of the unconditional one, combined with the tower property of conditional expectation (condExp_condExp_of_le). Term by term over the cells Pᵢ, writing f_i ω = (condExpKernel μ ℬ ω Pᵢ).toReal and g_i ω = (condExpKernel μ 𝒜 ω Pᵢ).toReal:

• the kernel-to-condExp links (condExpKernel_ae_eq_condExp) give f_i =ᵐ μ⟦Pᵢ | ℬ⟧ and g_i =ᵐ μ⟦Pᵢ | 𝒜⟧, and the tower property gives μ⟦f_i | 𝒜⟧ =ᵐ g_i;
• conditional Jensen for the concave negMulLog gives μ⟦negMulLog ∘ f_i | 𝒜⟧ ≤ᵐ negMulLog ∘ μ⟦f_i | 𝒜⟧ =ᵐ negMulLog ∘ g_i;
• integrating and using integral_condExp (the μ-average of a conditional expectation is the μ-average of the function) turns the left side back into ∫ negMulLog ∘ f_i ∂μ, giving ∫ negMulLog ∘ f_i ∂μ ≤ ∫ negMulLog ∘ g_i ∂μ.

Summing over the finite partition yields the claim.

Main results

• Oseledets.Entropy.condEntropy_mono_of_le: conditioning on a finer σ-algebra reduces conditional entropy.

References

• François Le Maître, Notes on the Kolmogorov–Sinai theorem (2017), §1.
• Peter Walters, An Introduction to Ergodic Theory, Springer GTM 79, Chapter 4.

theorem Oseledets.Entropy.condEntropy_mono_of_le {α : Type u_1} {ι : Type u_2} {𝒜 ℬ : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (h𝒜ℬ : 𝒜 ≤ ℬ) (hℬ : ℬ ≤ mα) (P : MeasurePartition μ ι) : condEntropy μ ℬ P.cells ≤ condEntropy μ 𝒜 P.cells

Monotonicity of conditional entropy under refinement. Conditioning on the finer sub-σ-algebra ℬ ⊇ 𝒜 produces the smaller conditional entropy: for any finite measurable partition P of the probability space and any sub-σ-algebras 𝒜 ≤ ℬ ≤ mα, H(P | ℬ) ≤ H(P | 𝒜).

This is the conditional generalization of condEntropy_le (which is the case 𝒜 = ⊥). The proof applies the conditional Jensen inequality (ConcaveOn.condExp_map_le) for the concave negMulLog against 𝒜, term by term over the cells Pᵢ. Writing f_i ω = (condExpKernel μ ℬ ω Pᵢ).toReal, the tower property condExp_condExp_of_le identifies the inner 𝒜-conditional expectation μ⟦f_i | 𝒜⟧ with the coarser kernel mass (condExpKernel μ 𝒜 ω Pᵢ).toReal; integrating the resulting pointwise Jensen bound and using integral_condExp gives the termwise inequality, which sums to the claim.