EntropyCover.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Subexponential name covers and zero entropy

The criterion concerns the finite-observation definition of metric entropy. Its hypotheses ask for high-mass collections of orbit names, not for an entropy inequality.

theorem OAI.DukePrimeDegree.observationEntropyRate_le_zero_of_good_names line 21

Source documentation

Subexponentially many names covering arbitrarily high mass give zero entropy rate for an observation.

theorem observationEntropyRate_le_zero_of_good_names {Y α : Type*}
    [MeasurableSpace Y] [Fintype α] [DecidableEq α]
    (μ : Measure Y) [IsProbabilityMeasure μ] {T : Y → Y}
    (hT : MeasurePreserving T μ μ) (P : Y → α)
    (hP : ∀ a, MeasurableSet {y | P y = a})
    (hcover : ∀ ε : ℝ, 0 < ε →
      ∃ G : ∀ N : ℕ, Finset (Fin N → α),
        (∀ᶠ N : ℕ in atTop, (G N).Nonempty) ∧
        (∀ᶠ N : ℕ in atTop,
          (∑ w, if w ∈ G N then 0 else μ.real {y | orbitName T P N y = w}) ≤ ε) ∧
        (∀ᶠ N : ℕ in atTop, Real.log (G N).card ≤ ε * N)) :
    observationEntropyRate μ T P ≤ 0 := by
…

theorem OAI.DukePrimeDegree.measureEntropy_eq_zero_of_good_names line 50

Source documentation

If every finite observation admits subexponential high-mass name covers, the metric entropy is zero.

theorem measureEntropy_eq_zero_of_good_names {Y : Type*} [MeasurableSpace Y]
    (μ : Measure Y) [IsProbabilityMeasure μ] {T : Y → Y}
    (hT : MeasurePreserving T μ μ)
    (hcover : ∀ (k : ℕ) (P : Y → Fin k)
      (_hP : ∀ a, MeasurableSet {y | P y = a}) (ε : ℝ), 0 < ε →
      ∃ G : ∀ N : ℕ, Finset (Fin N → Fin k),
        (∀ᶠ N : ℕ in atTop, (G N).Nonempty) ∧
        (∀ᶠ N : ℕ in atTop,
          (∑ w, if w ∈ G N then 0 else μ.real {y | orbitName T P N y = w}) ≤ ε) ∧
        (∀ᶠ N : ℕ in atTop, Real.log (G N).card ≤ ε * N)) :
    measureEntropy μ T = 0 := by
…