OAI/NumberTheory/Ostmann/ZeroDensity/DensityDyadicBlockCost.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The sharp length cost of one dyadic detector block

  1. theorem OAI.Ostmann.density_dyadic_power_cost line 9
  2. theorem OAI.Ostmann.density_dyadic_log_cost line 28
  3. theorem OAI.Ostmann.density_dyadic_total_cost line 58