OAI/NumberTheory/Ostmann/Quadratic/QuadraticGrowthBridge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recovering the full matrix bound from uniform dyadic estimates

  1. theorem OAI.Ostmann.quadratic_growth_of_dyadic line 11