PeriodicEntropyZero.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Almost-everywhere periodicity gives zero finite-observation entropy

A common positive period makes every long orbit name a deterministic extension of one fixed finite name. Thus block entropy stays bounded and its entropy rate is zero. Combining this with full-A ergodicity isolates the aperiodic branch without asserting ergodicity of the chosen map.

def OAI.DukePrimeDegree.periodicNameExtension line 22
lemma OAI.DukePrimeDegree.ae_orbitName_periodic_extension line 26

theorem OAI.DukePrimeDegree.orbitEntropy_le_period_name line 36

Source documentation

The bound is independent of the length of the observed orbit.

theorem orbitEntropy_le_period_name {Y α : Type*}
    [MeasurableSpace Y] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype α]
    (μ : Measure Y) [IsProbabilityMeasure μ] (T : Y → Y) (hT : Measurable T)
    (n : ℕ) (hn : 0 < n) (hperiod : ∀ᵐ x ∂μ, T^[n] x = x)
    (P : Y → α) (hP : Measurable P) (N : ℕ) :
    observationEntropy μ (orbitName T P N) ≤ observationEntropy μ (orbitName T P n) := by
…

theorem OAI.DukePrimeDegree.observationEntropyRate_zero_of_ae_periodic line 53
theorem OAI.DukePrimeDegree.measureEntropy_zero_of_ae_periodic line 71

theorem OAI.DukePrimeDegree.diagonal_entropy_zero_or_aperiodic line 87

Source documentation

Full diagonal ergodicity gives a zero-entropy/aperiodic dichotomy for every fixed real-time diagonal map.

theorem diagonal_entropy_zero_or_aperiodic (d : ℕ)
    (ell : Fin (d + 1) → ℝ) (hell : ∑ i, ell i = 0) (t : ℝ)
    (μ : Measure (X (d + 1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d + 1)) μ] :
    measureEntropy μ (fun x => rightAction x (diagonalOneParameter ell hell t)) = 0 ∨
    (∀ᵐ x ∂μ, ∀ n : ℕ, 0 < n →
      (fun y => rightAction y (diagonalOneParameter ell hell t))^[n] x ≠ x) := by
…

theorem OAI.DukePrimeDegree.diagonal_aperiodic_of_positive_entropy line 105