OAI/NumberTheory/Ostmann/Quadratic/QuadraticDilationPowerCost.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The enlarged balanced row interval costs only a small power

  1. theorem OAI.Ostmann.quadratic_dilation_power_cost line 9