OAI/NumberTheory/Ostmann/Construction/InitialProtectedTarget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual two cutoff centers fit the protected target

  1. def OAI.Ostmann.movingInitialGapTotal line 11
  2. theorem OAI.Ostmann.movingInitialGapTotal_linear line 16
  3. theorem OAI.Ostmann.initial_log_center_bounds line 24
  4. theorem OAI.Ostmann.eventual_initial_protected_target line 34