OAI/NumberTheory/Ostmann/Supply/ConstantModeBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The constant mode bounds the size of a sieved interval subset

  1. theorem OAI.Ostmann.lowMode_tensor_energy_one_le line 9
  2. theorem OAI.Ostmann.constant_mode_card_bound line 23