OAI/NumberTheory/JointDickman/Amplification/MinorArcStrongApproximation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Dirichlet approximation retaining the error on the ambient scale

  1. theorem OAI.JointDickman.minorArc_strong_rational_approximation line 8