OAI/NumberTheory/SiegelZeros/Structure/NotEventuallyMaster.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.FinalComparison.not_eventually_master line 15
  2. theorem OAI.SiegelZeros.WeightedTorusJets.tendsto_log_natCeil_rpow_div_log line 47
  3. theorem OAI.SiegelZeros.WeightedTorusJets.tendsto_log_scale_natCeil_rpow_div_log line 66
  4. theorem OAI.SiegelZeros.WeightedTorusJets.tendsto_natCeil_rpow_atTop line 79
  5. theorem OAI.SiegelZeros.WeightedTorusJets.tendsto_scale_natCeil_rpow_atTop line 83
  6. theorem OAI.SiegelZeros.WeightedTorusJets.exists_gamma_second_term_bound line 88
  7. theorem OAI.SiegelZeros.WeightedTorusJets.scale_cube_eq_degree_four line 95
  8. theorem OAI.SiegelZeros.WeightedTorusJets.log_degree_four_eq_three_log_scale line 100
  9. theorem OAI.SiegelZeros.WeightedTorusJets.log_eq_three_quarters_log_scale line 105
  10. theorem OAI.SiegelZeros.WeightedTorusJets.weight_rpow_shift line 117
  11. theorem OAI.SiegelZeros.WeightedTorusJets.rectangle_weight_sum line 122
  12. theorem OAI.SiegelZeros.WeightedTorusJets.rectangle_weight_le line 128
  13. theorem OAI.SiegelZeros.WeightedTorusJets.transverse_coordinates_le line 137
  14. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_ratio_le line 149
  15. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_ratio_le_one_twelfth line 164
  16. theorem OAI.SiegelZeros.WeightedTorusJets.floor_square_bound line 173
  17. theorem OAI.SiegelZeros.WeightedTorusJets.transverse_scale_ge line 180
  18. theorem OAI.SiegelZeros.WeightedTorusJets.pivot_floor_square_rpow_bound line 193
  19. theorem OAI.SiegelZeros.WeightedTorusJets.twice_pivot_floor_square_le line 204
  20. theorem OAI.SiegelZeros.WeightedTorusJets.normalized_error_component_bounds line 231
  21. theorem OAI.SiegelZeros.WeightedTorusJets.normalized_error_component_bounds_weighted line 253
  22. theorem OAI.SiegelZeros.WeightedTorusJets.determinant_error_le line 273
  23. theorem OAI.SiegelZeros.WeightedTorusJets.tendsto_determinant_error line 287
  24. theorem OAI.SiegelZeros.WeightedTorusJets.tendsto_bounded_ratio_log_error line 314
  25. theorem OAI.SiegelZeros.WeightedTorusJets.tendsto_normalized_error_sum line 335
  26. theorem OAI.SiegelZeros.WeightedTorusJets.FinalComparison.uniform_master_bound line 366
  27. theorem OAI.SiegelZeros.WeightedTorusJets.exists_fixed_parameters_not_eventually_uniform_bound line 403