OAI/NumberTheory/Jacobsthal/Siegel/NotEventuallyMaster.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.FinalComparison.not_eventually_master line 16
  2. theorem OAI.Erdos970.WeightedTorusJets.tendsto_log_natCeil_rpow_div_log line 48
  3. theorem OAI.Erdos970.WeightedTorusJets.tendsto_log_scale_natCeil_rpow_div_log line 67
  4. theorem OAI.Erdos970.WeightedTorusJets.tendsto_natCeil_rpow_atTop line 80
  5. theorem OAI.Erdos970.WeightedTorusJets.tendsto_scale_natCeil_rpow_atTop line 84
  6. theorem OAI.Erdos970.WeightedTorusJets.exists_gamma_second_term_bound line 89
  7. theorem OAI.Erdos970.WeightedTorusJets.scale_cube_eq_degree_four line 96
  8. theorem OAI.Erdos970.WeightedTorusJets.log_degree_four_eq_three_log_scale line 101
  9. theorem OAI.Erdos970.WeightedTorusJets.log_eq_three_quarters_log_scale line 106
  10. theorem OAI.Erdos970.WeightedTorusJets.weight_rpow_shift line 118
  11. theorem OAI.Erdos970.WeightedTorusJets.rectangle_weight_sum line 123
  12. theorem OAI.Erdos970.WeightedTorusJets.rectangle_weight_le line 129
  13. theorem OAI.Erdos970.WeightedTorusJets.transverse_coordinates_le line 138
  14. theorem OAI.Erdos970.WeightedTorusJets.pivot_ratio_le line 150
  15. theorem OAI.Erdos970.WeightedTorusJets.pivot_ratio_le_one_twelfth line 165
  16. theorem OAI.Erdos970.WeightedTorusJets.floor_square_bound line 174
  17. theorem OAI.Erdos970.WeightedTorusJets.transverse_scale_ge line 181
  18. theorem OAI.Erdos970.WeightedTorusJets.pivot_floor_square_rpow_bound line 194
  19. theorem OAI.Erdos970.WeightedTorusJets.twice_pivot_floor_square_le line 205
  20. theorem OAI.Erdos970.WeightedTorusJets.normalized_error_component_bounds line 232
  21. theorem OAI.Erdos970.WeightedTorusJets.normalized_error_component_bounds_weighted line 254
  22. theorem OAI.Erdos970.WeightedTorusJets.determinant_error_le line 274
  23. theorem OAI.Erdos970.WeightedTorusJets.tendsto_determinant_error line 288
  24. theorem OAI.Erdos970.WeightedTorusJets.tendsto_bounded_ratio_log_error line 315
  25. theorem OAI.Erdos970.WeightedTorusJets.tendsto_normalized_error_sum line 336
  26. theorem OAI.Erdos970.WeightedTorusJets.FinalComparison.uniform_master_bound line 367
  27. theorem OAI.Erdos970.WeightedTorusJets.exists_fixed_parameters_not_eventually_uniform_bound line 404