OAI/NumberTheory/SiegelZeros/Structure/MasterContradiction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.SiegelZerosAwei.W46.masterRHS line 17
2. theorem OAI.SiegelZeros.SiegelZerosAwei.W46.master_identity line 24
3. theorem OAI.SiegelZeros.SiegelZerosAwei.W46.master_from_real_bounds line 35
4. theorem OAI.SiegelZeros.SiegelZerosAwei.W46.master_from_log_bounds line 51
5. theorem OAI.SiegelZeros.SiegelZerosAwei.W46.log_three_quarters_power line 72
6. theorem OAI.SiegelZeros.SiegelZerosAwei.W46.master_from_power_scale line 77
7. theorem OAI.SiegelZeros.SiegelZerosAwei.W50.one_le_allowances_of_eventual_master line 100
8. theorem OAI.SiegelZeros.SiegelZerosAwei.W50.false_of_eventual_master_allowances line 115
9. theorem OAI.SiegelZeros.SiegelZerosAwei.W50.second_term_eventually_le line 126
10. theorem OAI.SiegelZeros.SiegelZerosAwei.W50.false_of_master_ratio_limit line 140
11. theorem OAI.SiegelZeros.SiegelZerosAwei.W50.false_of_exact_master line 163