Shannon entropy of a countable measurable partition

This file builds the countable-partition Shannon entropy layer needed for the unconditional Krieger finite generator theorem (issue #15). Krieger's proof (Downarowicz, Entropy in Dynamical Systems, Theorem 4.2.3) first produces a countable generator with finite static (Shannon) entropy, and only then codes it into Fin k. The repository's existing entropy stack (Oseledets.Entropy.*) is indexed by a Fintype; this file extends the Shannon entropy H(α) = ∑ᵢ negMulLog (μ(αᵢ)) to a countable family of cells via an unconditional tsum, and proves the finiteness criterion that the Krieger limit-code construction consumes.

Representation

Following Oseledets.Entropy.entropy, the entropy is defined on loose data — a Countable-indexed family of cells s : ι → Set α — so that it applies both to a countable measurable partition and to intermediate families. The companion bundle is the existing Oseledets.Entropy.MeasurePartition (finite) for the agreement lemma.

Because tsum over ℝ returns the junk value 0 for a non-summable family, the honest formalization of "the entropy is finite" is the Summable predicate on the termwise sequence i ↦ negMulLog (μ(sᵢ)).toReal: when it holds, Hμ is the genuine infinite sum (and is finite, being a real number); the finiteness criterion is therefore stated as a Summable conclusion.

Main definitions

• Oseledets.Krieger.cHμ: the countable Shannon entropy ∑' i, negMulLog (μ (s i)).toReal of a Countable-indexed family of cells s : ι → Set α.

Main results

• Oseledets.Krieger.cHμ_nonneg: countable entropy is nonnegative for a probability measure.
• Oseledets.Krieger.cHμ_eq_entropy: for a Fintype-indexed family the countable entropy agrees with the finite Oseledets.Entropy.entropy, so the countable theory genuinely extends the finite one.
• Oseledets.Krieger.summable_negMulLog_of_le: the comparison core. If 0 ≤ p i ≤ c i ≤ e⁻¹ for all i and i ↦ negMulLog (c i) is summable, then i ↦ negMulLog (p i) is summable. This is the directly-consumable finiteness input: a partition cell used with probability ≤ cᵢ, where ∑ negMulLog cᵢ < ∞, contributes a summable entropy tail.
• Oseledets.Krieger.summable_negMulLog_of_summable_index_mul: Downarowicz Fact 1.1.4. If a countable nonnegative sub-probability family p : ℕ → ℝ satisfies ∑ i, i · pᵢ < ∞, then its entropy i ↦ negMulLog (pᵢ) is summable, hence H(p) < ∞.
• Oseledets.Krieger.cHμ_summable_of_summable_index_mul: the same criterion phrased on a partition μ-measure family: if ∑ i, i · μ(sᵢ).toReal < ∞, the countable entropy cHμ μ s is a genuine finite sum.

References

• Tomasz Downarowicz, Entropy in Dynamical Systems, Cambridge (2011), §1.1 (Fact 1.1.4) and §4.2 (the Krieger generator theorem).
• Peter Walters, An Introduction to Ergodic Theory, Springer (1982), Ch. 4.
• François Le Maître, Notes on the Kolmogorov–Sinai theorem (2017), §1.

noncomputable def Oseledets.Krieger.cHμ {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : ι → Set α) : ℝ

The countable Shannon entropy ∑' i, negMulLog (μ (s i)).toReal of a Countable-indexed family of cells s : ι → Set α with respect to a measure μ. For a genuine partition this is - ∑ᵢ μ(sᵢ) log μ(sᵢ), the average information of learning which cell a random point lies in. The tsum is unconditional; it returns 0 if the termwise sequence is not summable (see cHμ_summable_of_summable_index_mul for the finiteness criterion that makes it a genuine sum).

Equations

• Oseledets.Krieger.cHμ μ s = ∑' (i : ι), (μ (s i)).toReal.negMulLog

@[simp]

theorem Oseledets.Krieger.cHμ_def {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : ι → Set α) : cHμ μ s = ∑' (i : ι), (μ (s i)).toReal.negMulLog

theorem Oseledets.Krieger.negMulLog_measure_toReal_nonneg {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (A : Set α) : 0 ≤ (μ A).toReal.negMulLog

Each entropy term negMulLog (μ (s i)).toReal is nonnegative for a probability measure, since each cell has measure in [0, 1] and negMulLog is nonnegative there.

theorem Oseledets.Krieger.cHμ_nonneg {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (s : ι → Set α) : 0 ≤ cHμ μ s

Countable Shannon entropy is nonnegative for a probability measure: every term is nonnegative, so the unconditional tsum is nonnegative (whether or not it converges, since tsum of a non-summable nonnegative family is the junk value 0 ≥ 0).

@[simp]

theorem Oseledets.Krieger.cHμ_eq_entropy {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] (μ : MeasureTheory.Measure α) (s : ι → Set α) : cHμ μ s = Entropy.entropy μ s

Finite agreement. For a Fintype-indexed family of cells the countable Shannon entropy cHμ agrees with the repository's finite Oseledets.Entropy.entropy: the unconditional tsum over a finite index type collapses to the finite sum. This shows the countable theory genuinely extends the finite one.

Monotonicity of negMulLog on the lower branch

The function negMulLog x = -x log x is increasing on [0, e⁻¹] (its maximum is at e⁻¹). This is the lower-branch monotonicity used in Downarowicz's finiteness criterion (Fact 1.1.4): a cell used with very small probability p contributes negMulLog p, dominated by negMulLog c for any p ≤ c ≤ e⁻¹.

theorem Oseledets.Krieger.negMulLog_monotoneOn_Icc : MonotoneOn Real.negMulLog (Set.Icc 0 (Real.exp (-1)))

negMulLog is monotone increasing on [0, e⁻¹]: it is -(x log x), and x ↦ x log x is strictly antitone there (Real.mul_log_strictAntiOn).

theorem Oseledets.Krieger.negMulLog_le_of_le {p c : ℝ} (hp : 0 ≤ p) (hpc : p ≤ c) (hc : c ≤ Real.exp (-1)) : p.negMulLog ≤ c.negMulLog

The monotone comparison for a single pair 0 ≤ p ≤ c ≤ e⁻¹: negMulLog p ≤ negMulLog c.

The comparison finiteness criterion

theorem Oseledets.Krieger.summable_negMulLog_of_le {ι : Type u_2} {p c : ι → ℝ} (hp : ∀ (i : ι), 0 ≤ p i) (hpc : ∀ (i : ι), p i ≤ c i) (hc : ∀ (i : ι), c i ≤ Real.exp (-1)) (hsum : Summable fun (i : ι) => (c i).negMulLog) : Summable fun (i : ι) => (p i).negMulLog

Comparison core for finite countable entropy. If 0 ≤ p i ≤ c i ≤ e⁻¹ for all i and the dominating entropy sequence i ↦ negMulLog (c i) is summable, then i ↦ negMulLog (p i) is summable. This is the directly-consumable input for Krieger's limit-code construction: a partition cell used with probability ≤ cᵢ, with ∑ negMulLog cᵢ < ∞, has a summable (hence finite) entropy contribution.

Downarowicz's Fact 1.1.4: the ∑ i·pᵢ < ∞ finiteness criterion

The criterion the Krieger limit-code construction (Downarowicz Thm 4.2.3) ultimately consumes: a countable nonnegative sub-probability family whose index-weighted total ∑ i·pᵢ is finite has finite Shannon entropy. The proof is Downarowicz's two-branch split of each term against the threshold 2⁻ⁱ: above the threshold negMulLog pᵢ = pᵢ·(−log pᵢ) ≤ pᵢ·(i·log 2) since −log is decreasing; below it negMulLog pᵢ ≤ negMulLog 2⁻ⁱ = 2⁻ⁱ·(i·log 2) since negMulLog is increasing on [0, e⁻¹] ⊇ [0, 2⁻ⁱ] for i ≥ 2. Both dominating sequences are summable.

theorem Oseledets.Krieger.half_pow_le_exp_neg_one {i : ℕ} (hi : 2 ≤ i) : (1 / 2) ^ i ≤ Real.exp (-1)

(1/2)^i ≤ e⁻¹ for i ≥ 2: indeed (1/2)^i ≤ (1/2)^2 = 1/4, and 1/4 ≤ e⁻¹ since e < 3 < 4. This places 2⁻ⁱ in the lower monotone branch [0, e⁻¹] of negMulLog.

theorem Oseledets.Krieger.negMulLog_half_pow (i : ℕ) : ((1 / 2) ^ i).negMulLog = (1 / 2) ^ i * (↑i * Real.log 2)

negMulLog ((1/2)^i) = (1/2)^i · (i · log 2).

theorem Oseledets.Krieger.negMulLog_le_index_bound {i : ℕ} (hi : 2 ≤ i) {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : p.negMulLog ≤ ↑i * Real.log 2 * p + ↑i * Real.log 2 * (1 / 2) ^ i

The two-branch termwise domination (Downarowicz Fact 1.1.4, per term). For i ≥ 2 and a sub-probability value 0 ≤ p ≤ 1, negMulLog p ≤ (i·log 2)·p + (i·log 2)·(1/2)^i. Above the threshold 2⁻ⁱ the first summand dominates (since −log is decreasing); below it the second dominates (since negMulLog is increasing on [0, 2⁻ⁱ]).

theorem Oseledets.Krieger.summable_negMulLog_of_summable_index_mul {p : ℕ → ℝ} (hp0 : ∀ (i : ℕ), 0 ≤ p i) (hp1 : ∀ (i : ℕ), p i ≤ 1) (hsum : Summable fun (i : ℕ) => ↑i * p i) : Summable fun (i : ℕ) => (p i).negMulLog

Downarowicz Fact 1.1.4. If a countable nonnegative sub-probability family p : ℕ → ℝ (0 ≤ pᵢ ≤ 1) has finite index-weighted total ∑ i, i·pᵢ < ∞, then its Shannon entropy sequence i ↦ negMulLog (pᵢ) is summable, hence H(p) = ∑ᵢ negMulLog pᵢ < ∞.

This is the static finiteness input to Krieger's finite generator theorem: the inductively built countable generator places cell i with measure controlled so that ∑ i·μ(cellᵢ) < ∞, whence its static entropy is finite. The proof dominates each entropy term (Downarowicz's two-branch split, negMulLog_le_index_bound) by (i·log 2)·pᵢ + (i·log 2)·2⁻ⁱ; the first is summable from ∑ i·pᵢ < ∞, the second is the convergent series ∑ i·2⁻ⁱ.

The partition-level finiteness criterion

theorem Oseledets.Krieger.cHμ_summable_of_summable_index_mul {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] {s : ℕ → Set α} (hsum : Summable fun (i : ℕ) => ↑i * (μ (s i)).toReal) : Summable fun (i : ℕ) => (μ (s i)).toReal.negMulLog

Finite static entropy of a countable partition (Krieger's static input). If a ℕ-indexed family of cells s of a probability space has finite index-weighted total mass ∑ i, i·μ(sᵢ) < ∞, then the entropy terms i ↦ negMulLog (μ(sᵢ)).toReal are summable, so the countable Shannon entropy cHμ μ s is a genuine (finite) sum rather than the tsum junk value.

This is Downarowicz Fact 1.1.4 specialized to a μ-measure family: it is the criterion the Krieger limit-code construction (Downarowicz Thm 4.2.3) verifies for the inductively built countable generator, certifying that the generator has finite static entropy before it is coded into Fin k.