OAI/NumberTheory/Ostmann/ZeroDensity/DensityActualBlock.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform estimates for the actual detector's dyadic blocks

  1. theorem OAI.Ostmann.density_actual_block_bound line 12