The Bernoulli entropy identity (N4a)

For the i.i.d. (Bernoulli) measure bern ν on the one-sided full shift Shift α₀ over a finite alphabet, the Kolmogorov–Sinai entropy of the coordinate partition equals the single-symbol Shannon entropy Hnu ν = ∑ i, negMulLog (ν {i}).toReal.

The argument is the classical computation that the entropy of an i.i.d. process is additive over coordinates:

• N4a.1 (cell mass). The depth-n join cell of the coordinate partition at an index f : Fin n → α₀ is the length-n cylinder {x | ∀ k : Fin n, x k = f k}, whose bern ν-mass is the product ∏ k, (ν {f k}).toReal of single-symbol masses (Measure.infinitePi_pi).
• N4a.2 (per-n entropy). Hence ksEntropySeq n = ∑ f, negMulLog (∏ k, p (f k)) with p a := (ν {a}).toReal. The per-coordinate factorization negMulLog (∏ k, p (f k)) = ∑ k, (∏ j, p (f j)) * (-log (p (f k))) followed by the sum/product swap Finset.sum_prod_piFinset (and ∑ a, p a = 1) collapses this to n * Hnu ν.
• N4a.3 (Fekete limit). Since ksEntropySeq n = n * Hnu ν, the averaged sequence ksEntropySeq n / n is eventually the constant Hnu ν; by uniqueness of the Fekete limit (tendsto_ksEntropySeq), the partition entropy is Hnu ν.

The system entropy identity (ksEntropy).toReal = Hnu ν then follows from the generator reduction already proved on main (ksEntropy_eq_ksEntropyPartition_of_generating via coordPartition_isGenerating), taking the ergodicity of the shift as a hypothesis (it is a sibling node).

Main results

• Oseledets.Multifractal.ksEntropyPartition_coordPartition_bern_eq
• Oseledets.Multifractal.ksEntropy_bern_eq

N4a.0 — a real-analytic per-f factorization

theorem Oseledets.Multifractal.negMulLog_prod_eq_sum {n : ℕ} (p : Fin n → ℝ) : (∏ k : Fin n, p k).negMulLog = ∑ k : Fin n, (∏ j : Fin n, p j) * -Real.log (p k)

Per-coordinate factorization of negMulLog of a product. For any finite family p : Fin n → ℝ of nonnegative reals, negMulLog (∏ k, p k) = ∑ k, (∏ j, p j) * (-log (p k)). When every p k is nonzero this is the distributivity of log over the product; when some p k = 0 both sides vanish (the product is 0, and on the right each summand carries the vanishing product factor; the convention Real.log 0 = 0 keeps the k-summand 0 * 0 = 0).

N4a.1 — the depth-n join cell mass

theorem Oseledets.Multifractal.ksJoinCells_coordPartition_eq {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) (n : ℕ) (f : Fin n → α₀) : Entropy.ksJoinCells (coordPartition (bern ν)).cells shiftMap n f = {x : Shift α₀ | ∀ (k : Fin n), x ↑k = f k}

The depth-n join cell of the coordinate partition at f : Fin n → α₀ is the cylinder {x | ∀ k : Fin n, x ↑k = f k}: the cell at coordinate k pulled back along shiftMap^[k] is {x | x ↑k = f k} (because (shiftMap^[k] x) 0 = x k).

theorem Oseledets.Multifractal.cylinder_eq_pi {α₀ : Type u_1} (n : ℕ) (f : Fin n → α₀) : {x : Shift α₀ | ∀ (k : Fin n), x ↑k = f k} = (↑(Finset.range n)).pi fun (i : ℕ) => if hi : i < n then {f ⟨i, hi⟩} else Set.univ

The cylinder {x | ∀ k : Fin n, x ↑k = f k} is the measurable box Set.pi ↑(Finset.range n) t with t i = {f ⟨i, hi⟩} for i < n (and Set.univ otherwise).

theorem Oseledets.Multifractal.bern_ksJoinCells_eq {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] (n : ℕ) (f : Fin n → α₀) : (bern ν) (Entropy.ksJoinCells (coordPartition (bern ν)).cells shiftMap n f) = ∏ k : Fin n, ν {f k}

N4a.1 (cell mass). The bern ν-mass of the depth-n join cell at f : Fin n → α₀ is the product ∏ k, ν {f k} of single-symbol masses (Measure.infinitePi_pi on the cylinder box).

N4a.2 — the per-n entropy is n * Hnu ν

theorem Oseledets.Multifractal.sum_measureReal_singleton_eq_one {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : ∑ a : α₀, (ν {a}).toReal = 1

The single-symbol masses sum to 1: ∑ a, (ν {a}).toReal = 1.

theorem Oseledets.Multifractal.ksEntropySeq_coordPartition_bern_eq {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] (n : ℕ) : Entropy.ksEntropySeq ⋯ (coordPartition (bern ν)) n = ↑n * Hnu ν

N4a.2 (per-n entropy). The iterated-join entropy of the coordinate partition at depth n is n * Hnu ν.

N4a — the headline partition identity

theorem Oseledets.Multifractal.ksEntropyPartition_coordPartition_bern_eq {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : Entropy.ksEntropyPartition ⋯ (coordPartition (bern ν)) = Hnu ν

N4a (partition entropy). The Kolmogorov–Sinai entropy of the coordinate partition for the Bernoulli measure bern ν equals the single-symbol Shannon entropy Hnu ν.

N4a — the system entropy identity

theorem Oseledets.Multifractal.ksEntropy_bern_eq {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : (Entropy.ksEntropy ⋯).toReal = Hnu ν

N4a (system entropy). For the Bernoulli shift, the Kolmogorov–Sinai entropy of the system equals the single-symbol Shannon entropy Hnu ν.

The coordinate partition is a generator (coordPartition_isGenerating), so the Kolmogorov–Sinai generator theorem (ksEntropy_eq_ksEntropyPartition_of_generating, on the Fin-reindexed partition) identifies ksEntropy with the coordinate-partition entropy, which the partition identity ties to Hnu ν. No ergodicity is needed: the generator reduction is unconditional (it consumes only the generating property and the standard-Borel structure).