The additive-over-cells conditional entropy is the σ-algebra conditional entropy #
This module proves the W2 bridge lemma of issue #13 §5b: for a finite measurable partition
B of a standard-Borel probability space, the additive-over-cells conditional entropy
H(Q | B) = ∑ᵢ μ(Bᵢ) · H(Q | Bᵢ) (the condEntropyGivenPartition of CondChainRule, the
𝒜 = ⊥ form) coincides with the σ-algebra conditional entropy H(Q | σ(B)) (the condEntropy
of CondPartition, conditioning on the σ-algebra σ(B) = generatedSigmaAlgebra μ B generated by
the cells of B):
condEntropyGivenPartition μ B.cells t = condEntropy μ (generatedSigmaAlgebra μ B) t.
This identifies the elementary, finite-sum definition of conditional entropy used in the
Abramov–Rokhlin chain rule with the kernel/disintegration definition H(· | σ(B)), and is a
prerequisite for the W3 sub-piece.
Proof outline #
The crux is the atom-agreement kernel identity: for μ-a.e. ω lying in the cell Bᵢ,
the regular conditional probability of tⱼ given σ(B) is the cell-conditional value
μ(Bᵢ ∩ tⱼ) / μ(Bᵢ). Concretely we prove that the piecewise-constant candidate
gⱼ(ω) = ∑ᵢ (μ(Bᵢ ∩ tⱼ)/μ(Bᵢ)) · 𝟙_{Bᵢ}(ω) (condCandidate) is a version of the conditional
expectation μ⟦tⱼ | σ(B)⟧, via ae_eq_condExp_of_forall_setIntegral_eq. Its set-integral
hypothesis — ∫ x in s, gⱼ x ∂μ = μ(s ∩ tⱼ).toReal for every σ(B)-measurable s — rests on the
atom property of σ(B) (generatedSigmaAlgebra_atom): every σ(B)-measurable set is, modulo
μ-null sets, a union of cells (proved by induction on the generateFrom structure, the
countable-union step closing for arbitrary, not just disjoint, unions). On each cell s is then
all-or-nothing, so the indicator term (μ(Bᵢ ∩ tⱼ)/μ(Bᵢ)) · μ(s ∩ Bᵢ) equals μ(s ∩ Bᵢ ∩ tⱼ)
(condCandidate_cell_scaling), and summing over the covering cells gives μ(s ∩ tⱼ) via the
marginal identity MeasurePartition.measure_eq_sum_inter.
Bridging the kernel to condExp (condExpKernel_ae_eq_condExp) and splitting the defining
integral of condEntropy over the a.e.-disjoint covering cells (integral_iUnion_ae) — on each of
which the integrand is the constant condEntropyOnCell μ Bᵢ t — then yields the claim.
Main results #
Oseledets.Entropy.condEntropyGivenPartition_eq_condEntropy_generated: the bridge lemmaH(Q | B) = H(Q | σ(B)).
A cell B.cells i of a finite partition is measurable for the generated σ-algebra
σ(B) = generateFrom (range B.cells).
The generated σ-algebra σ(B) is below the ambient σ-algebra mα (every cell is
mα-measurable).
Atom property of the generated σ-algebra. Every σ(B)-measurable set is, modulo μ-null
sets, a union of cells: on each cell Bᵢ it is all-or-nothing. Either Bᵢ meets the set in a
null set, or Bᵢ is contained in the set up to a null set.
Proved by induction on the generateFrom structure: a cell is all-or-nothing on every cell
(distinct cells are μ-a.e. disjoint; a cell against itself); complementation swaps the two
alternatives; and a countable union is null on Bᵢ if every piece is, else contains Bᵢ up to a
null set as soon as one piece does.
The piecewise-constant candidate for the conditional expectation μ⟦t j | σ(B)⟧: the function
taking the cell-conditional value μ(Bᵢ ∩ t j) / μ(Bᵢ) on each cell Bᵢ. Written as a finite sum
of indicators of the cells, it is σ(B)-strongly measurable.
Equations
Instances For
The candidate is σ(B)-strongly measurable: a finite sum of indicators of cells (which are
σ(B)-measurable) scaled by constants.
Per-cell scaling identity. For a σ(B)-measurable set s and a measurable tⱼ, the
cell-conditional value μ(Bᵢ ∩ tⱼ)/μ(Bᵢ) scaled by μ(s ∩ Bᵢ) equals μ(s ∩ Bᵢ ∩ tⱼ). This is
where the atom property enters: on the cell Bᵢ, s is all-or-nothing (mod null), so the
proportion μ(Bᵢ ∩ tⱼ)/μ(Bᵢ) of the cell that lies in tⱼ is exactly the proportion of s ∩ Bᵢ
that lies in tⱼ.
Set-integral of the candidate. For every σ(B)-measurable set s,
∫ x in s, condCandidate B tⱼ x ∂μ = μ(s ∩ tⱼ).toReal.
The integral distributes over the finite indicator sum; the i-th term is
(μ(Bᵢ ∩ tⱼ)/μ(Bᵢ)) · μ(s ∩ Bᵢ).toReal, which equals μ(s ∩ Bᵢ ∩ tⱼ).toReal by the per-cell
scaling identity; summing these over the a.e.-disjoint covering cells recovers μ(s ∩ tⱼ).toReal
via the marginal identity MeasurePartition.measure_eq_sum_inter.
The candidate is a version of the conditional expectation. For a finite measure and a
measurable tⱼ, the piecewise-constant condCandidate B tⱼ equals the conditional expectation
μ⟦tⱼ | σ(B)⟧ almost everywhere. Verified via ae_eq_condExp_of_forall_setIntegral_eq: the
candidate is σ(B)-strongly measurable (stronglyMeasurable_condCandidate) and matches the
set-integrals of the indicator 𝟙_{tⱼ} on every σ(B)-measurable set
(setIntegral_condCandidate).
The candidate is constant on each cell, a.e. For μ-a.e. ω ∈ Bᵢ, the value of
condCandidate B tⱼ ω is the cell-conditional value μ(Bᵢ ∩ tⱼ)/μ(Bᵢ): only the i-th indicator
of the defining sum is nonzero, since the set of points of Bᵢ that also lie in another cell is
μ-null (the cells are a.e. disjoint).
W2 bridge lemma. The additive-over-cells conditional entropy H(Q | B) of a finite family
t given a finite measurable partition B equals the σ-algebra conditional entropy H(Q | σ(B))
obtained by conditioning on the σ-algebra σ(B) = generatedSigmaAlgebra μ B generated by the cells
of B:
condEntropyGivenPartition μ B.cells t = condEntropy μ (generatedSigmaAlgebra μ B) t.
This identifies the elementary finite-sum definition of conditional entropy used in the
Abramov–Rokhlin chain rule (CondChainRule) with the kernel/disintegration definition
(CondPartition). The crux is the atom-agreement kernel identity: for μ-a.e. ω ∈ Bᵢ, the
regular conditional probability condExpKernel μ (σ(B)) ω (tⱼ) equals the cell-conditional value
μ(Bᵢ ∩ tⱼ)/μ(Bᵢ), established by identifying the piecewise-constant candidate with the
conditional expectation (condCandidate_ae_eq_condExp) and bridging the kernel to condExp
(condExpKernel_ae_eq_condExp). The defining integral of condEntropy then splits over the
a.e.-disjoint covering cells (integral_iUnion_ae), and on each cell the integrand is the constant
condEntropyOnCell μ Bᵢ t, summing to condEntropyGivenPartition.