Lévy-upward continuity of conditional Shannon entropy

This file adds the upward continuity of conditional Shannon 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 condEntropy_tendsto_iSup says: for an increasing sequence of conditioning sub-σ-algebras 𝒜seq 0 ≤ 𝒜seq 1 ≤ ⋯ ≤ mα and a fixed finite measurable partition P, the conditional entropies H(P | 𝒜seq n) converge to the conditional entropy H(P | ⨆ n, 𝒜seq n) with respect to the limiting (generated) σ-algebra. This is the specialization of Mathlib's almost-sure Lévy upward theorem for conditional expectations (MeasureTheory.tendsto_ae_condExp) to the nonlinear entropy functional; it is a load-bearing analytic sub-ingredient of issue #13's §5b.

The proof has three steps, run per cell Pᵢ of the partition:

• Lévy upward (a.e.). Bundling 𝒜seq into a MeasureTheory.Filtration ℕ mα, Mathlib's tendsto_ae_condExp applied to the indicator g_i = (Pᵢ).indicator (fun _ => 1) gives μ⟦Pᵢ | 𝒜seq n⟧ → μ⟦Pᵢ | ⨆ n, 𝒜seq n⟧ μ-a.e. The kernel-to-condExp bridge condExpKernel_ae_eq_condExp rewrites both sides as the kernel masses (condExpKernel μ · ω Pᵢ).toReal, so a.e. ω has (condExpKernel μ (𝒜seq n) ω Pᵢ).toReal → (condExpKernel μ (⨆ n, 𝒜seq n) ω Pᵢ).toReal.
• Continuity of negMulLog. Composing with the continuous Real.negMulLog and summing over the finite index ι gives a.e. convergence of the full condEntropy integrand.
• Dominated convergence. Each integrand is a.e. in [0, log (card ι)] (nonnegativity plus the pointwise Jensen bound entropy_le_log_card), so the constant log (card ι) is an integrable dominator on the probability space and tendsto_integral_of_dominated_convergence transfers the pointwise convergence to convergence of the integrals, i.e. of condEntropy.

Main results

• Oseledets.Entropy.condEntropy_tendsto_iSup: conditional Shannon entropy is upward-continuous along an increasing sequence of conditioning σ-algebras (Lévy-upward continuity).

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_tendsto_iSup {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] [Nonempty ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (𝒜seq : ℕ → MeasurableSpace α) (hmono : Monotone 𝒜seq) (hle : ∀ (n : ℕ), 𝒜seq n ≤ mα) (P : MeasurePartition μ ι) : Filter.Tendsto (fun (n : ℕ) => condEntropy μ (𝒜seq n) P.cells) Filter.atTop (nhds (condEntropy μ (⨆ (n : ℕ), 𝒜seq n) P.cells))

Lévy-upward continuity of conditional Shannon entropy. For an increasing sequence of conditioning sub-σ-algebras 𝒜seq 0 ≤ 𝒜seq 1 ≤ ⋯ ≤ mα and a fixed finite measurable partition P of the probability space, the conditional Shannon entropies H(P | 𝒜seq n) converge to the conditional entropy H(P | ⨆ n, 𝒜seq n) with respect to the generated limiting σ-algebra.

This is the specialization of Mathlib's almost-sure Lévy upward theorem (MeasureTheory.tendsto_ae_condExp) to the nonlinear conditional-entropy functional. Per cell Pᵢ, the indicator's conditional expectations μ⟦Pᵢ | 𝒜seq n⟧ converge a.e. to μ⟦Pᵢ | ⨆ n⟧; via condExpKernel_ae_eq_condExp these are the kernel masses entering condEntropy, so composing with the continuous negMulLog and summing over the finite index gives a.e. convergence of the integrand. As the integrand lies a.e. in [0, log (card ι)], the constant log (card ι) dominates it and tendsto_integral_of_dominated_convergence yields convergence of the integrals.