OAI/NumberTheory/DukePrimeDegree/Dynamics/MaximalOccupation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform control of visits to decreasing exceptional sets

The finite Hopf inequality bounds the probability of ever having an excessive occupation average. Applied to decreasing null-intersection sets, it gives almost-sure uniform control over every time interval.

  1. lemma OAI.DukePrimeDegree.visitCount_mono line 19
  2. def OAI.DukePrimeDegree.excessiveOccupation line 27
  3. lemma OAI.DukePrimeDegree.excessiveOccupation_mono line 30
  4. lemma OAI.DukePrimeDegree.measurableSet_excessiveOccupation line 41
  5. theorem OAI.DukePrimeDegree.excessiveOccupation_measure_bound line 49
  6. theorem OAI.DukePrimeDegree.ae_uniform_small_occupation_of_decreasing line 91