OAI/NumberTheory/DukePrimeDegree/Entropy/ReturnPartitionEntropy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite Shannon entropy of the first-return partition

The geometric reference distribution turns the mass-weighted return-time bound into summable information. This is the return-partition estimate in Einsiedler--Lindenstrauss, Proposition 7.44, paragraph 7.48.

  1. theorem OAI.DukePrimeDegree.summable_information_of_first_moment line 21

    Source documentation

    A finite first moment controls the information of a subprobability sequence; no normalization of the return section is necessary.

    theorem summable_information_of_first_moment (p : ℕ → ℝ)
    (hp : ∀ n, 0 ≤ p n) (hp1 : ∀ n, p n ≤ 1)
    (hmean : Summable (fun n : ℕ => (n+1:ℝ)*p n)) :
    Summable (fun n => Real.negMulLog (p n)) := by
…
  2. theorem OAI.DukePrimeDegree.firstReturnPartition_information_summable line 42