OAI/NumberTheory/PiExponent/Approximation/Parameters.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PiExponent.exists_rational_parameters line 7
2. theorem OAI.PiExponent.exists_eta_preserving_exponent_gap line 71
3. structure OAI.PiExponent.Parameters line 93
4. theorem OAI.PiExponent.exists_parameters line 112
5. theorem OAI.PiExponent.Parameters.A_pos line 124
6. theorem OAI.PiExponent.Parameters.B_pos line 126
7. theorem OAI.PiExponent.Parameters.C_pos line 128
8. theorem OAI.PiExponent.Parameters.A_lt_one line 130
9. theorem OAI.PiExponent.Parameters.theta_lt_one line 132
10. theorem OAI.PiExponent.Parameters.CB_lt_one line 134
11. theorem OAI.PiExponent.Parameters.one_lt_C_theta_div_B line 138
12. theorem OAI.PiExponent.Parameters.one_lt_B_div_A line 142