OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingTimeSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One time for two points and two shearing scales

The finite bad-window estimate selects the common time in EKL (2006), Lemma 4.6. For each point and each scale the loss is at most nine times the original density error. The four losses total at most thirty-six.

  1. theorem OAI.DukePrimeDegree.exists_common_two_scale_time line 19