OAI/NumberTheory/TotientAsymptotic/ConcentrationInput.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Discharging Ford's fixed-deviation coordinate input by elementary simplex caps.

  1. theorem OAI.TotientAsymptotic.fordCoordinateConcentrationInput line 12

    Source documentation

    The only distinction between the exact triangular simplex and Ford's terminal inequality costs the fixed determinant factor 1/a₁.

    theorem fordCoordinateConcentrationInput : FordCoordinateConcentrationInput := by
…

    Mentions: OAI.TotientAsymptotic.FordCoordinateConcentrationInput