OAI/NumberTheory/Ostmann/Construction/SelectedCellMassRate.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The chosen small cells meet the original prior's exponential budget

  1. theorem OAI.Ostmann.eventual_cell_harmonic_floor line 12
  2. theorem OAI.Ostmann.selected_cell_after_finite_deletion line 32