OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingFourWindows.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Four candidate windows for the two annular radii

EKL Lemma 4.6 needs both possible scale regimes at each of two annular radii. The four windows have total density loss at most 72 * ε for two initial points. Null-time exceptions for covariance can be avoided at all four windows simultaneously.

  1. theorem OAI.DukePrimeDegree.exists_common_four_window_time line 20
  2. theorem OAI.DukePrimeDegree.exists_common_four_window_time_ae line 79
  3. theorem OAI.DukePrimeDegree.exists_common_four_window_time_with_covariance line 105