OAI/NumberTheory/PiExponent/Approximation/Exponent.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.eventualLowerBound_iff_integer line 7
2. theorem OAI.PiExponent.finite_rat_den_le_abs_sub_lt_one line 28
3. theorem OAI.PiExponent.two_mem_approximationExponents line 57
4. theorem OAI.PiExponent.finite_goodRationalApproximations_of_eventualLowerBound line 77
5. theorem OAI.PiExponent.irrationalityExponent_eq_two_of_eventualLowerBound line 92
6. theorem OAI.PiExponent.pi_irrationalityExponent_eq_two_of_eventualLowerBound line 104
7. theorem OAI.PiExponent.eventualLowerBound_of_not_unbounded_approximations line 108