OAI/NumberTheory/TotientAsymptotic/CoordinateGridConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed bad coordinate has exponentially small mass after the exact unit-box affine correction.

  1. theorem OAI.TotientAsymptotic.coordinate_grid_concentration line 12