OAI/NumberTheory/DukePrimeDegree/Geometry/LeafScaleComposition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Comparing leaves at two selected diagonal times

Normalized scaling composes exactly when the leaf gives positive mass to every neighborhood of the origin. This transfers the small-ball bound at the second recurrence time to the annulus at the first time, the measure comparison in EKL Lemma 4.5.

  1. theorem OAI.DukePrimeDegree.normalized_scaling_comp line 21
  2. theorem OAI.DukePrimeDegree.normalized_scaling_ball_pos line 44
  3. theorem OAI.DukePrimeDegree.rootPair_leaf_covariance_between_times line 54
  4. theorem OAI.DukePrimeDegree.rootPair_small_ball_gives_annulus line 80