OAI/NumberTheory/TotientAsymptotic/SimplexConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform two-sided concentration of bounded linear forms on a simplex.

  1. lemma OAI.TotientAsymptotic.volume_simplex_fixed_deviation line 11