OAI/NumberTheory/TotientAsymptotic/FixedModelTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The five-percent Ford interval lies inside the ten-percent model interval once the uniform center ratio is sufficiently close to one.

  1. theorem OAI.TotientAsymptotic.fixed_model_band_failure_transfer line 12