OAI/NumberTheory/Ostmann/Construction/SelectedInitialWindowRate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The selected product center fits the original one-unit gap reserve

  1. theorem OAI.Ostmann.selected_initial_window_rate line 9
  2. theorem OAI.Ostmann.selected_initial_normalizer_rate line 37