OAI/NumberTheory/Ostmann/Construction/ScheduledSelectedGaps.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Every actual removal has its prescribed diagonal gap

  1. theorem OAI.Ostmann.movingCompensationTargets_drop_gap line 10
  2. theorem OAI.Ostmann.movingCompensationGaps_at line 25
  3. theorem OAI.Ostmann.movingCompensationTargets_drop_balance line 33
  4. theorem OAI.Ostmann.forallâ‚‚_headD_drop line 48
  5. theorem OAI.Ostmann.selected_scheduled_drop_diagonal_gap line 58