OAI/NumberTheory/Ostmann/ZeroDensity/DensityDetectorBlocks.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact dyadic decomposition of the original polynomial alternative

  1. theorem OAI.Ostmann.densityDetector_polynomial_extended line 12
  2. theorem OAI.Ostmann.densityDetector_polynomial_blocks line 33