FourthIterateEntropy.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Positive entropy survives the fourth iterate

The regular weights used in the finite coefficient-balance test are four times the original regular weights. Grouping four consecutive symbols transfers positive metric entropy to that time-four map. Only this fixed iterate is needed here.

def OAI.DukePrimeDegree.fourWordEquiv line 21
lemma OAI.DukePrimeDegree.orbitName_four_blocks line 31
lemma OAI.DukePrimeDegree.observationEntropyRate_recode line 42

theorem OAI.DukePrimeDegree.observationEntropyRate_four_blocks line 57

Source documentation

Four-symbol blocks have four times the original entropy rate.

theorem observationEntropyRate_four_blocks {Y α : Type*}
    [MeasurableSpace Y] [Fintype α]
    (μ : Measure Y) [IsProbabilityMeasure μ] {T : Y → Y}
    (hT : MeasurePreserving T μ μ) (P : Y → α)
    (hP : ∀ a, MeasurableSet {y | P y = a}) :
    observationEntropyRate μ (T^[4]) (orbitName T P 4) =
      4 * observationEntropyRate μ T P := by
…

theorem OAI.DukePrimeDegree.measureEntropy_eq_zero_of_fourth_iterate line 91

Source documentation

Vanishing entropy of the time-four map forces vanishing entropy of the original map. This uses the actual supremum over finite observations.

theorem measureEntropy_eq_zero_of_fourth_iterate {Y : Type*} [MeasurableSpace Y]
    (μ : Measure Y) [IsProbabilityMeasure μ] {T : Y → Y}
    (hT : MeasurePreserving T μ μ) (hzero : measureEntropy μ (T^[4]) = 0) :
    measureEntropy μ T = 0 := by
…

theorem OAI.DukePrimeDegree.measureEntropy_fourth_iterate_pos line 118