OAI/NumberTheory/DukePrimeDegree/Dynamics/ReturnTowerMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

First return times have finite mass-weighted mean

  1. theorem OAI.DukePrimeDegree.firstReturnLevel_mass_sum_le line 15
  2. theorem OAI.DukePrimeDegree.summable_firstReturnLevel_mass line 49

    Source documentation

    This finite first moment is the return-time estimate used to keep the refined countable partition's Shannon entropy finite.

    theorem summable_firstReturnLevel_mass
    {Y : Type*} [MeasurableSpace Y] (μ : Measure Y) [IsProbabilityMeasure μ]
    {T : Y → Y} (hT : MeasurePreserving T μ μ) (hE : MeasurableEmbedding T)
    {S : Set Y} (hS : MeasurableSet S) :
    Summable (fun n : ℕ => (n+1:ℝ)*μ.real (firstReturnLevel T S n)) := by
…

    Mentions: OAI.DukePrimeDegree.firstReturnLevel