EntropyUpper.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Entropy bounds from a small collection of orbit names

This is the finite-partition estimate used in an entropy upper bound: if all but a small mass lies on a short list of names, the entropy is bounded by the logarithm of that list, plus the cost of the exceptional mass. No dynamical covering or leafwise estimate is assumed here.

theorem OAI.DukePrimeDegree.finiteShannon_le_good_card line 23

Source documentation

A finite distribution concentrated on a list of names has small entropy. The binary coding cost is at most log 2.

theorem finiteShannon_le_good_card {α : Type*} [Fintype α] [DecidableEq α]
    (p : α → ℝ) (hp : ∀ a, 0 ≤ p a) (hp1 : ∑ a, p a = 1)
    (G : Finset α) (hG : G.Nonempty) :
    finiteShannon p ≤ Real.log 2 + Real.log G.card +
      (∑ a, if a ∈ G then 0 else p a) * Real.log (Fintype.card α) := by
…

theorem OAI.DukePrimeDegree.observationEntropy_le_good_card line 72

Source documentation

If a collection of observation values misses at most ε of the measure, its cardinality bounds the observation entropy.

theorem observationEntropy_le_good_card {Y α : Type*}
    [MeasurableSpace Y] [Fintype α] [DecidableEq α]
    (μ : Measure Y) [IsProbabilityMeasure μ] (P : Y → α)
    (hP : ∀ a, MeasurableSet {y | P y = a})
    (G : Finset α) (hG : G.Nonempty) {ε : ℝ}
    (hbad : (∑ a, if a ∈ G then 0 else μ.real {y | P y = a}) ≤ ε) :
    observationEntropy μ P ≤ Real.log 2 + Real.log G.card +
      ε * Real.log (Fintype.card α) := by
…

theorem OAI.DukePrimeDegree.observationEntropyRate_le_of_good_names line 90

Source documentation

The exponential growth of a list of orbit names, together with its exceptional mass, bounds the entropy rate of the observation.

theorem observationEntropyRate_le_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})
    (G : ∀ N : ℕ, Finset (Fin N → α)) {a ε : ℝ}
    (hne : ∀ᶠ N : ℕ in atTop, (G N).Nonempty)
    (hbad : ∀ᶠ N : ℕ in atTop,
      (∑ w, if w ∈ G N then 0 else μ.real {y | orbitName T P N y = w}) ≤ ε)
    (hcard : ∀ᶠ N : ℕ in atTop, Real.log (G N).card ≤ a * N) :
    observationEntropyRate μ T P ≤ a + ε * Real.log (Fintype.card α) := by
…