Subadditivity and invariance of conditional entropy

This file is the next layer of the conditional-entropy milestone (GitHub issue #13). It continues Oseledets.Entropy.CondPartition (which defines condEntropy μ 𝒜 s, the μ-average of the pointwise entropy against the regular conditional probability condExpKernel μ 𝒜 ω) and Oseledets.Entropy.CondExpEquivariant (the two-sided conditional-expectation equivariance (★)).

Two structural facts about conditional entropy are established:

• Subadditivity under joins (condEntropy_join_le): for partitions P and Q, H(P ∨ Q | 𝒜) ≤ H(P | 𝒜) + H(Q | 𝒜). This is proved by running the absolute argument (entropy_join_le) pointwise inside the integral against the Markov-kernel measure condExpKernel μ 𝒜 ω, which for μ-a.e. ω is a probability measure for which P and Q are still genuine measurable partitions; the resulting pointwise bound integrates termwise.

• Invariance under a measure-preserving factor (condEntropy_pullback and its iterate): for a measure-preserving T : α → α satisfying the two-sided invariance hypotheses (T is 𝒜/𝒜-measurable and every 𝒜-set is μ-a.e. a T-preimage of an 𝒜-set), H(T⁻¹P | 𝒜) = H(P | 𝒜), and the iterated version H(T⁻ⁿP | 𝒜) = H(P | 𝒜). The proof bridges the conditional kernel to the conditional expectation (condExpKernel_ae_eq_condExp), invokes the equivariance (★) (condExp_indicator_preimage_comp), and finishes with the measure-preserving change of variables integral_comp_self.

The two-sided hypotheses are necessary: a prior analysis exhibited an explicit non-invertible Markov factor for which the one-sided hypothesis comap T 𝒜 ≤ 𝒜 makes condEntropy_pullback false.

Main results

• Oseledets.Entropy.condEntropy_sum_eq_one: a.e. normalization of the conditional cell probabilities of a partition.
• Oseledets.Entropy.condExpKernel_sum_inter_toReal: the conditional marginal identity ∑ⱼ (κ(ω, Pᵢ ∩ Qⱼ)).toReal = (κ(ω, Pᵢ)).toReal (a.e.).
• Oseledets.Entropy.condEntropy_join_le: subadditivity of conditional entropy under joins.
• Oseledets.Entropy.condEntropy_pullback: invariance of conditional entropy under a two-sided measure-preserving factor.
• Oseledets.Entropy.condEntropy_pullback_iterate: the iterated invariance H(T⁻ⁿP | 𝒜) = H(P | 𝒜).

References

• François Le Maître, Notes on the Kolmogorov–Sinai theorem (2017), §1.

theorem Oseledets.Entropy.condEntropy_sum_eq_one {α : Type u_1} {ι : Type u_2} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (h𝒜 : 𝒜 ≤ mα) (P : MeasurePartition μ ι) : ∀ᵐ (ω : α) ∂μ, ∑ i : ι, (((ProbabilityTheory.condExpKernel μ 𝒜) ω) (P.cells i)).toReal = 1

For a finite measurable partition P of the probability space and μ-almost every ω, the conditional cell probabilities under condExpKernel μ 𝒜 ω sum to 1. This is a re-export of condExpKernel_sum_toReal_measure_eq_one.

theorem Oseledets.Entropy.condExpKernel_sum_inter_toReal {α : Type u_1} {ι : Type u_2} {κ : Type u_3} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (h𝒜 : 𝒜 ≤ mα) (P : MeasurePartition μ ι) (Q : MeasurePartition μ κ) : ∀ᵐ (ω : α) ∂μ, ∀ (i : ι), ∑ j : κ, (((ProbabilityTheory.condExpKernel μ 𝒜) ω) (P.cells i ∩ Q.cells j)).toReal = (((ProbabilityTheory.condExpKernel μ 𝒜) ω) (P.cells i)).toReal

Conditional marginal identity. For partitions P (indexed by ι) and Q (indexed by κ) of the probability space, the conditional kernel measures of the join cells Pᵢ ∩ Qⱼ sum, over the column index j, to the conditional kernel measure of Pᵢ, for μ-almost every ω.

This is the conditional (kernel-level) analogue of MeasurePartition.measure_eq_sum_inter. It follows from finite additivity of the probability measure condExpKernel μ 𝒜 ω over the family (Pᵢ ∩ Qⱼ)ⱼ, whose union is Pᵢ (since the cells of Q cover the space) and whose members are condExpKernel μ 𝒜 ω-a.e. disjoint; the a.e.-disjointness is transferred from μ through the disintegration condExpKernel μ 𝒜 ∘ₘ μ.trim h𝒜 = μ.

theorem Oseledets.Entropy.condExpKernel_pairwise_aedisjoint {α : Type u_1} {ι : Type u_2} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (h𝒜 : 𝒜 ≤ mα) (P : MeasurePartition μ ι) : ∀ᵐ (ω : α) ∂μ, Pairwise (Function.onFun (MeasureTheory.AEDisjoint ((ProbabilityTheory.condExpKernel μ 𝒜) ω)) P.cells)

For a finite measurable partition P of the probability space, the cells are condExpKernel μ 𝒜 ω-a.e. pairwise disjoint for μ-almost every ω. This is the partition hypothesis of MeasurePartition transferred from μ to the conditional kernel through the disintegration condExpKernel μ 𝒜 ∘ₘ μ.trim h𝒜 = μ.

theorem Oseledets.Entropy.condEntropy_integrand_eq_entropy {α : Type u_1} {ι : Type u_2} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (s : ι → Set α) (ω : α) : ∑ i : ι, (((ProbabilityTheory.condExpKernel μ 𝒜) ω) (s i)).toReal.negMulLog = entropy ((ProbabilityTheory.condExpKernel μ 𝒜) ω) s

The pointwise condEntropy integrand of a family s equals the Shannon entropy of s computed against the conditional-kernel probability measure condExpKernel μ 𝒜 ω.

theorem Oseledets.Entropy.condEntropy_join_le {α : Type u_1} {ι : Type u_2} {κ : Type u_3} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (h𝒜 : 𝒜 ≤ mα) (P : MeasurePartition μ ι) (Q : MeasurePartition μ κ) : condEntropy μ 𝒜 (joinCells P.cells Q.cells) ≤ condEntropy μ 𝒜 P.cells + condEntropy μ 𝒜 Q.cells

Subadditivity of conditional entropy under joins. For two finite measurable partitions P and Q of a probability space, the conditional entropy of the join is at most the sum of the conditional entropies: H(P ∨ Q | 𝒜) ≤ H(P | 𝒜) + H(Q | 𝒜).

The bound is the absolute subadditivity entropy_join_le run pointwise inside the integral: for μ-almost every ω the conditional kernel condExpKernel μ 𝒜 ω is a probability measure for which both P and Q are still genuine measurable partitions (their cells are kernel-a.e. disjoint by condExpKernel_pairwise_aedisjoint and still cover the space), so the discrete Gibbs argument bounds the pointwise integrand entropy (κ ω) (P ∨ Q) by entropy (κ ω) P + entropy (κ ω) Q. Integrating this a.e. inequality over μ (all three integrands are integrable by the log card bound) gives the claim.

theorem Oseledets.Entropy.condExpKernel_preimage_toReal_ae_eq {α : Type u_1} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] {T : α → α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (h𝒜 : 𝒜 ≤ mα) (hT : MeasureTheory.MeasurePreserving T μ μ) (hTA : Measurable T) (hpull : ∀ (A : Set α), MeasurableSet A → ∃ (A' : Set α), MeasurableSet A' ∧ A =ᵐ[μ] T ⁻¹' A') {B : Set α} (hB : MeasurableSet B) : (fun (ω : α) => (((ProbabilityTheory.condExpKernel μ 𝒜) ω) (T ⁻¹' B)).toReal) =ᵐ[μ] fun (ω : α) => (((ProbabilityTheory.condExpKernel μ 𝒜) (T ω)) B).toReal

Kernel equivariance. Under the two-sided invariance hypotheses, for a measurable set B the conditional kernel probability of the T-preimage T⁻¹B is μ-a.e. the conditional kernel probability of B evaluated at T ω: (κ(ω, T⁻¹B)).toReal =ᵐ[μ] (κ(Tω, B)).toReal.

The proof bridges the kernel to the conditional expectation via condExpKernel_ae_eq_condExp, applies the conditional-expectation equivariance (★) (condExp_indicator_preimage_comp), and transports the kernel-side identity for B through the measure-preserving change of variables with Measure.QuasiMeasurePreserving.ae_eq_comp.

theorem Oseledets.Entropy.hpull_iterate {α : Type u_1} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] {T : α → α} {μ : MeasureTheory.Measure α} (hT : MeasureTheory.MeasurePreserving T μ μ) (hpull : ∀ (A : Set α), MeasurableSet A → ∃ (A' : Set α), MeasurableSet A' ∧ A =ᵐ[μ] T ⁻¹' A') (n : ℕ) (A : Set α) : MeasurableSet A → ∃ (A' : Set α), MeasurableSet A' ∧ A =ᵐ[μ] T^[n] ⁻¹' A'

Iterating the two-sided pull-back hypothesis. If every 𝒜-set is μ-a.e. a T-preimage of an 𝒜-set, then every 𝒜-set is μ-a.e. a T^[n]-preimage of an 𝒜-set, for every n. The inductive step composes the n-fold preimage of the chosen 𝒜-witness with one more application of the hypothesis, transported through the measure-preserving T.

theorem Oseledets.Entropy.condEntropy_pullback {α : Type u_1} {ι : Type u_2} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] {T : α → α} [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (h𝒜 : 𝒜 ≤ mα) (hT : MeasureTheory.MeasurePreserving T μ μ) (hTA : Measurable T) (hpull : ∀ (A : Set α), MeasurableSet A → ∃ (A' : Set α), MeasurableSet A' ∧ A =ᵐ[μ] T ⁻¹' A') (P : MeasurePartition μ ι) : (condEntropy μ 𝒜 fun (i : ι) => T ⁻¹' P.cells i) = condEntropy μ 𝒜 P.cells

Invariance of conditional entropy under a two-sided measure-preserving factor. For a measure-preserving T : α → α that is 𝒜/𝒜-measurable and satisfies the two-sided pull-back hypothesis (every 𝒜-set is μ-a.e. a T-preimage of an 𝒜-set), the conditional entropy of the pulled-back partition T⁻¹P equals that of P: H(T⁻¹P | 𝒜) = H(P | 𝒜).

The condEntropy integrand at T⁻¹P is, by the kernel equivariance condExpKernel_preimage_toReal_ae_eq applied to each (measurable) cell, μ-a.e. equal to the integrand at P precomposed with T; the measure-preserving change of variables integral_comp_self then leaves the integral unchanged.

theorem Oseledets.Entropy.condEntropy_pullback_iterate {α : Type u_1} {ι : Type u_2} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] {T : α → α} [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (h𝒜 : 𝒜 ≤ mα) (hT : MeasureTheory.MeasurePreserving T μ μ) (hTA : Measurable T) (hpull : ∀ (A : Set α), MeasurableSet A → ∃ (A' : Set α), MeasurableSet A' ∧ A =ᵐ[μ] T ⁻¹' A') (n : ℕ) (P : MeasurePartition μ ι) : (condEntropy μ 𝒜 fun (i : ι) => T^[n] ⁻¹' P.cells i) = condEntropy μ 𝒜 P.cells

Iterated invariance of conditional entropy. For a measure-preserving T satisfying the two-sided invariance hypotheses, the conditional entropy of the n-fold pulled-back partition T^[n]⁻¹P equals that of P: H(T⁻ⁿP | 𝒜) = H(P | 𝒜).

The hypotheses are iteration-stable: T^[n] is again measure-preserving (MeasurePreserving.iterate) and 𝒜/𝒜-measurable (Measurable.iterate), and hpull_iterate lifts the pull-back hypothesis to T^[n]. The claim is then condEntropy_pullback applied to T^[n].