OAI/NumberTheory/SiegelZeros/Estimates/FloorExponents.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.W44.floor_quotient_eq line 13
2. theorem OAI.SiegelZeros.W44.quotient_lower line 16
3. theorem OAI.SiegelZeros.W44.quotient_eq_zero_of_lt line 20
4. def OAI.SiegelZeros.W44.exponent line 23
5. theorem OAI.SiegelZeros.W44.exponent_lower line 26
6. theorem OAI.SiegelZeros.W44.exponent_weight_interchange line 32
7. theorem OAI.SiegelZeros.W44.weighted_exponent_lower line 39
8. theorem OAI.SiegelZeros.W44.logarithmic_exponent_lower line 57
9. theorem OAI.SiegelZeros.W44.logarithmic_exponent_lower_subset line 67