The Breiman telescoping for the information function and the in-measure SMB upper bound

This file closes the analytic side of sub-problem A of the unconditional Krieger theorem (issue #15): it discharges the hbreiman hypothesis of the pointwise Shannon–McMillan–Breiman theorem (Oseledets.Krieger.SMBLeaves.ae_tendsto_div_infoFun) at the level of the concrete information function infoFun of InfoFunction.lean, and uses it to prove the in-measure SMB upper bound UpperSMBInMeasure (NameCountSharp.lean) as an unconditional theorem for ergodic transformations.

The Breiman telescoping identity (and a sharp off-by-one)

The pointwise SMB machinery in SMBLeaves is parameterized by an abstract sequence infoFun_n together with the Breiman telescoping hypothesis hbreiman : iₙ(x) = ∑_{j<n} g_{n−j}(Tʲx) (with g_k = condInfoFun 𝒞ₖ P and 𝒞ₖ = condLevelSigma). The convention used there indexes the summands by n − j, i.e. it conditions on the σ-algebras 𝒞₁, …, 𝒞ₙ.

For the concrete information function infoFun (the -log μ(atom) of InfoFunction.lean) the true telescoping conditions on 𝒞₀, …, 𝒞ₙ₋₁ instead: infoFun_n(x) = ∑_{j<n} g_{n−1−j}(Tʲx) (infoFun_succ_ae peels the first symbol: the first symbol of an n-name, given the remaining n−1 future symbols, conditions on the (n−1)-step past 𝒞ₙ₋₁; iterating gives the n−1−j index, with 𝒞₀ = ⊥ the trivial σ-algebra contributing the raw partition information -log μ(P-cell)). In particular at n = 1 the true identity is infoFun₁(x) = -log μ(P-cell of x) = g₀(x), not g₁(x).

So hbreiman with the SMBLeaves index n − j is false for infoFun. We therefore do not feed infoFun to ae_tendsto_div_infoFun directly. Instead we feed it the SMBLeaves-convention sum Aₙ(x) = ∑_{j<n} g_{n−j}(Tʲx) (for which hbreiman holds by reflexivity), obtaining (1/n)·Aₙ → h a.e., and bridge to infoFun via the one-term edge identity infoFun_{n+1}(x) = Aₙ(x) + g₀(Tⁿx) together with the orbital decay (1/n)·g₀(Tⁿx) → 0 (ae_tendsto_orbit_div_atTop_zero, valid since g₀ ∈ L¹). This yields the pointwise SMB (1/n)·infoFunₙ → h for infoFun, hence the in-measure bound.

Main results

• Oseledets.Krieger.infoFun_succ_ae — the one-step front-peel of the Breiman telescoping: infoFun_{n+1}(x) = g_n(x) + infoFun_n(Tx) a.e.
• Oseledets.Krieger.ae_tendsto_div_infoFun_self — the pointwise SMB for infoFun: (1/n)·infoFunₙ(x) → h(P,T) a.e. for ergodic T.
• Oseledets.Krieger.upperSMBInMeasure_of_ergodic — UpperSMBInMeasure hT P for ergodic T: discharges the in-measure SMB upper bound that exists_cover_names_card_le (C2) consumes.

References

• L. Breiman, The individual ergodic theorem of information theory, Ann. Math. Statist. 28 (1957), 809–811.
• M. Einsiedler, E. Lindenstrauss, T. Ward, Entropy in Ergodic Theory and Topological Dynamics, Ch. 2 (SMB).

The kernel/measure bridge condInfoFun(𝒞ₖ) = condInfoWeight Bₖ

The conditional information function condInfoFun (gen B) P y (defined via the regular conditional probability condExpKernel μ (gen B) y (Pᵢ)) agrees μ-a.e. with the conditional information weight condInfoWeight B P i₀ b (defined via the elementary conditional probability μ(B_b ∩ P_{i₀})/μ(B_b)), where i₀ is the unique P-cell and b the unique B-cell of y. This is the per-step instance of the partition/σ-algebra bridge (condCandidate_ae_eq_condExp, condCandidate_ae_eq_on_cell).

theorem Oseledets.Krieger.toReal_condExpKernel_generated_ae_eq {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : Entropy.MeasurePartition μ ι) {β : Type u_3} [Fintype β] (B : Entropy.MeasurePartition μ β) (i : ι) (b : β) : (fun (y : α) => (((ProbabilityTheory.condExpKernel μ (Entropy.generatedSigmaAlgebra μ B)) y) (P.cells i)).toReal) =ᵐ[μ.restrict (B.cells b)] fun (x : α) => (μ (B.cells b ∩ P.cells i)).toReal / (μ (B.cells b)).toReal

For a finite partition B, the gen(B)-conditional probability of a P-cell is a.e. the elementary conditional probability: for μ-a.e. y lying in the B-cell b, (condExpKernel μ (gen B) y Pᵢ).toReal = μ(B_b ∩ Pᵢ)/μ(B_b).

theorem Oseledets.Krieger.condInfoFun_eq_condInfoWeight_ae {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : Entropy.MeasurePartition μ ι) (k : ℕ) : ∀ᵐ (y : α) ∂μ, ∀ (i₀ : ι), y ∈ P.cells i₀ → (∀ (i' : ι), i' ≠ i₀ → y ∉ P.cells i') → ∀ (b : Fin k → ι), y ∈ (Entropy.MeasurePartition.pullback hT (Entropy.ksJoin hT P k)).cells b → condInfoFun P y = condInfoWeight (Entropy.MeasurePartition.pullback hT (Entropy.ksJoin hT P k)) P i₀ b

The bridge, membership form. For μ-a.e. y: whenever y lies in the unique P-cell i₀ and in the Bₖ-cell b (Bₖ = (ksJoin hT P k).pullback hT), the conditional info function of P given the k-step past 𝒞ₖ = condLevelSigma hT P k evaluates to the conditional info weight condInfoWeight Bₖ P i₀ b. The conditioning σ-algebra 𝒞ₖ is exactly generatedSigmaAlgebra μ Bₖ, so the conditional probability of Pᵢ₀ given 𝒞ₖ is a.e. the elementary conditional probability μ(B_b ∩ Pᵢ₀)/μ(B_b) (toReal_condExpKernel_generated_ae_eq), and only the i₀-indicator of condInfoFun survives at a point in a unique P-cell (condInfoFun_eq_neg_log_of_mem_unique).

theorem Oseledets.Krieger.ae_forall_orbit {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) {p : α → Prop} (hp : ∀ᵐ (x : α) ∂μ, p x) : ∀ᵐ (x : α) ∂μ, ∀ (j : ℕ), p (T^[j] x)

A predicate that holds μ-a.e. holds μ-a.e. along the whole forward orbit.

theorem Oseledets.Krieger.infoFun_succ_ae {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : Entropy.MeasurePartition μ ι) (n : ℕ) : ∀ᵐ (x : α) ∂μ, infoFun hT P (n + 1) x = condInfoFun P x + infoFun hT P n (T x)

One-step front-peel of the Breiman telescoping for infoFun. For each n, μ-a.e. x, the rank-(n+1) information function splits as the conditional information of the first symbol given the n-step past plus the rank-n information of the shifted point: infoFun_{n+1}(x) = condInfoFun(𝒞ₙ)(x) + infoFun_n(Tx).

The proof peels the first symbol of the rank-(n+1) itinerary using the cell cons-factorization (ksJoinCells_cons) and the measure-algebra one-step identity infoWeight_succ_eq (its positivity hypothesis holds a.e., off the null set of points in a null (n+1)-cell, measure_nullAtom_eq_zero); the conditional weight is identified with condInfoFun(𝒞ₙ) by the bridge condInfoFun_eq_condInfoWeight_ae, and the shifted rank-n weight with infoFun_n(Tx) by the a.e. uniqueness of the n-name of Tx (ae_mem_unique_cell for the n-fold join, transferred along T).

noncomputable def Oseledets.Krieger.breimanSum {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : Entropy.MeasurePartition μ ι) (n : ℕ) (x : α) : ℝ

The SMBLeaves-convention Breiman partial sum Aₙ(x) = ∑_{j<n} g_{n−j}(Tʲx) (g_k = condInfoFun 𝒞ₖ P), the exact object fed to ae_tendsto_div_infoFun.

Equations

• Oseledets.Krieger.breimanSum hT P n x = ∑ j ∈ Finset.range n, Oseledets.Krieger.condInfoFun P (T^[j] x)

theorem Oseledets.Krieger.breimanSum_succ {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : Entropy.MeasurePartition μ ι) (n : ℕ) (x : α) : breimanSum hT P (n + 1) x = condInfoFun P x + breimanSum hT P n (T x)

The one-step recursion of the partial sum: A_{n+1}(x) = g_{n+1}(x) + A_n(Tx). Peeling the j = 0 summand (= g_{n+1}(x)) and reindexing the rest j ↦ j+1 along the orbit.

theorem Oseledets.Krieger.infoFun_eq_breimanSum_add_edge {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : Entropy.MeasurePartition μ ι) : ∀ᵐ (x : α) ∂μ, ∀ (j n : ℕ), infoFun hT P (n + 1) (T^[j] x) = breimanSum hT P n (T^[j] x) + condInfoFun P (T^[n + j] x)

The Breiman telescoping for infoFun (edge form). For μ-a.e. x, for all j, n, infoFun_{n+1}(Tʲx) = Aₙ(Tʲx) + g₀(T^{n+j}x), where Aₙ is the SMBLeaves-convention partial sum and g₀ = condInfoFun 𝒞₀ P is the raw partition information (𝒞₀ trivial). This is the true Breiman identity infoFun_{n+1}(y) = ∑_{j≤n} g_{n−j}(Tʲy), one summand longer than Aₙ.

Proved by induction on n, with j universally quantified so that the induction hypothesis applies at the shifted point Tʲ⁺¹x = Tʲ(Tx): the one-step front-peel infoFun_succ_ae holds a.e. along the orbit, and the partial-sum recursion breimanSum_succ folds the peeled symbol.

theorem Oseledets.Krieger.ae_tendsto_div_infoFun_self {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} [Nonempty ι] (herg : Ergodic T μ) (P : Entropy.MeasurePartition μ ι) : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => infoFun ⋯ P n x / ↑n) Filter.atTop (nhds (Entropy.ksEntropyPartition ⋯ P))

Pointwise Shannon–McMillan–Breiman for the concrete information function. For an ergodic measure-preserving T and a finite partition P, the rank-n information averages (1/n)·infoFunₙ(x) converge μ-a.e. to the Kolmogorov–Sinai entropy h(P,T).

Combines the unconditional pointwise SMB for the SMBLeaves-convention partial sum Aₙ (ae_tendsto_div_infoFun with hbreiman holding by reflexivity for Aₙ = breimanSum) with the edge telescoping infoFun_{n+1}(x) = Aₙ(x) + g₀(Tⁿx) (infoFun_eq_breimanSum_add_edge), the orbital decay (1/n)·g₀(Tⁿx) → 0 (g₀ ∈ L¹, ae_tendsto_orbit_div_atTop_zero), and an index shift n ↦ n+1.

theorem Oseledets.Krieger.upperSMBInMeasure_of_ergodic {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} [Nonempty ι] (herg : Ergodic T μ) (P : Entropy.MeasurePartition μ ι) : UpperSMBInMeasure ⋯ P

The in-measure SMB upper bound, unconditional for ergodic T. This discharges the hypothesis UpperSMBInMeasure that exists_cover_names_card_le (C2) and the symbolic code carry: for every ε > 0, the measure of the deviation set {x | h + ε < (1/N)·infoFunₙ(x)} tends to 0.

Immediate from the pointwise a.e. SMB ae_tendsto_div_infoFun_self and the implication a.e.-convergence ⟹ in-measure vanishing of the deviation set (tendsto_measure_of_ae_tendsto_indicator_of_isFiniteMeasure).