OAI/NumberTheory/DukePrimeDegree/Entropy/RefinedReturnEntropy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exponential refinements of the first-return partition

A return level may be subdivided into exponentially many transverse cells. The logarithmic cell count is paid for by the return-time first moment.

  1. lemma OAI.DukePrimeDegree.finiteShannon_le_mass_log_card line 17
  2. theorem OAI.DukePrimeDegree.refined_return_information_summable line 53

    Source documentation

    The exact entropy budget used by exponentially refined return cells.

    theorem refined_return_information_summable
    (K : ℕ → ℕ) (p : ∀ n, Fin (K n) → ℝ) (mass : ℕ → ℝ)
    (hp : ∀ n i, 0 ≤ p n i) (hm : ∀ n, ∑ i, p n i=mass n)
    (hm1 : ∀ n, mass n ≤ 1)
    (hmean : Summable (fun n : ℕ => (n+1:ℝ)*mass n))
    (C : ℝ) (hcard : ∀ n, Real.log (K n) ≤ C*(n+1)) :
    Summable (fun z : Σ n : ℕ, Fin (K n) => Real.negMulLog (p z.1 z.2)) := by
…