The two-sided Bernoulli entropy identity (the hbase for the W3 flow descent)

This file lifts the one-sided Bernoulli entropy identity (Oseledets/Multifractal/BernoulliEntropy.lean) to the two-sided (invertible) full shift BiShift α₀ := ℤ → α₀ equipped with the two-sided i.i.d. measure bernZ ν (Oseledets/Multifractal/BernoulliTwoSided.lean). The result is the base entropy datum that the W3 flow-entropy descent consumes.

The combinatorial core is identical to the one-sided case: the depth-n forward join of the time-0 coordinate partition coordPartitionZ reads the coordinates 0, 1, …, n-1 (because biShiftMap^[k] x reads coordinate k), so its bernZ ν-mass factorizes as a product of single-symbol masses (bernZ_pi_eq_prod); the real-analytic identity negMulLog_prod_eq_sum and the sum/product swap Finset.sum_prod_piFinset (both reused verbatim from the one-sided file) collapse the per-n join entropy to n · Hnu ν, and Fekete's limit uniqueness gives the partition entropy Hnu ν.

The one and only structural difference is that the index type is ℤ rather than ℕ: the coordinate-support of the join cell is {0, 1, …, n-1} ⊆ ℤ, packaged as (Finset.range n).map intOfNatEmb.

There is deliberately no generator-theorem step here: coordPartitionZ is not one-sided generating for an invertible shift (it sees only the forward future), so the system-entropy reduction from the one-sided file does not port. Only the partition-relative identity is established (that is all the W3 descent needs).

Main results

• Oseledets.Multifractal.coordPartitionZFin
• Oseledets.Multifractal.ksEntropyPartition_coordPartitionZ_bernZ_eq
• Oseledets.Multifractal.ksEntropyPartition_coordPartitionZFin_bernZ_eq — the headline hbase

The shift-iterate reads a forward coordinate

theorem Oseledets.Multifractal.biShiftMap_iterate_apply {α₀ : Type u_1} (k : ℕ) (x : BiShift α₀) (n : ℤ) : biShiftMap^[k] x n = x (n + ↑k)

The k-th iterate of the two-sided shift advances every (integer) index by k: biShiftMap^[k] x n = x (n + k).

The integer-coordinate support {0, 1, …, n-1}

def Oseledets.Multifractal.intOfNatEmb : ℕ ↪ ℤ

The order-embedding ℕ ↪ ℤ of nonnegative integers, used to package the coordinate support {0, 1, …, n-1} ⊆ ℤ of a depth-n forward join cell as (Finset.range n).map intOfNatEmb.

Equations

• Oseledets.Multifractal.intOfNatEmb = { toFun := fun (k : ℕ) => ↑k, inj' := Oseledets.Multifractal.intOfNatEmb._proof_1 }

@[simp]

theorem Oseledets.Multifractal.intOfNatEmb_apply (k : ℕ) : intOfNatEmb k = ↑k

The depth-n forward join cell is the integer-coordinate cylinder

theorem Oseledets.Multifractal.ksJoinCells_coordPartitionZ_eq {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) (n : ℕ) (f : Fin n → α₀) : Entropy.ksJoinCells (coordPartitionZ (bernZ ν)).cells biShiftMap n f = {x : BiShift α₀ | ∀ (k : Fin n), x ↑↑k = f k}

The depth-n forward join cell of coordPartitionZ at f : Fin n → α₀ is the cylinder {x | ∀ k : Fin n, x ↑k = f k} on the (integer) coordinates 0, …, n-1: the cell at coordinate k pulled back along biShiftMap^[k] is {x | x ↑k = f k} (because (biShiftMap^[k] x) 0 = x k).

theorem Oseledets.Multifractal.coordCylinderZ_eq_pi {α₀ : Type u_1} (n : ℕ) (f : Fin n → α₀) : {x : BiShift α₀ | ∀ (k : Fin n), x ↑↑k = f k} = (↑(Finset.map intOfNatEmb (Finset.range n))).pi fun (i : ℤ) => if hi : i.toNat < n ∧ 0 ≤ i then {f ⟨i.toNat, ⋯⟩} else Set.univ

The cylinder {x | ∀ k : Fin n, x ↑k = f k} is the measurable box Set.pi ↑((Finset.range n).map intOfNatEmb) t with t i = {f ⟨i.toNat, _⟩} on the support and Set.univ elsewhere.

N4a.1 — the depth-n forward join cell mass

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

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

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

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

N4a.2 (per-n entropy). The iterated-join entropy of the coordinate partition at depth n is n * Hnu ν. The combinatorial core is reused verbatim from the one-sided file via negMulLog_prod_eq_sum, Finset.sum_prod_piFinset, and sum_measureReal_singleton_eq_one.

N4a — the headline partition identity

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

N4a (partition entropy, two-sided). The Kolmogorov–Sinai entropy of the time-0 coordinate partition coordPartitionZ for the two-sided Bernoulli measure bernZ ν equals the single-symbol Shannon entropy Hnu ν. Ported verbatim from the one-sided ksEntropyPartition_coordPartition_bern_eq: the averaged join-entropy sequence is eventually constant Hnu ν, so the Fekete limit is Hnu ν.

The Fin-reindexed coordinate partition and its entropy

def Oseledets.Multifractal.coordPartitionZFin {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure (BiShift α₀)) : Entropy.MeasurePartition ν (Fin (Fintype.card α₀))

The two-sided coordinate partition reindexed onto Fin (card α₀) via (Fintype.equivFin α₀).symm, mirroring coordPartitionFin for the one-sided shift. This is the canonical Fin-indexed presentation consumed by the W3 descent.

Equations

• One or more equations did not get rendered due to their size.

theorem Oseledets.Multifractal.ksEntropyPartition_coordPartitionZFin_eq {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : Entropy.ksEntropyPartition ⋯ (coordPartitionZFin (bernZ ν)) = Entropy.ksEntropyPartition ⋯ (coordPartitionZ (bernZ ν))

Reindexing invariance of the two-sided partition-relative entropy. The reindexed coordinate partition has the same Kolmogorov–Sinai entropy as the original. Ported from ksEntropyPartition_coordPartitionFin_eq: the iterated-join entropy sequences agree (the cells coincide up to the index reindexing Equiv.piCongrRight), and the Fekete limit is determined by that sequence.

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

The headline hbase. The Kolmogorov–Sinai entropy of the Fin-reindexed time-0 coordinate partition coordPartitionZFin for the two-sided Bernoulli measure bernZ ν equals the single-symbol Shannon entropy Hnu ν. This is the base entropy datum consumed by the W3 flow-entropy descent.