OAI/Geometry/HeilbronnTriangle/AlterationAsymptotics.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem355.tendsto_log_sq_div_pow_nine line 13
  2. theorem OAI.Problem355.log_two_mul_le_of_polynomial_bound line 19
  3. theorem OAI.Problem355.tendsto_box_log_sq_div_pow_nine line 35
  4. theorem OAI.Problem355.sample_half_le_nat_floor line 59
  5. theorem OAI.Problem355.floor_sample_properties line 64
  6. theorem OAI.Problem355.tendsto_real_sample_atTop line 73
  7. theorem OAI.Problem355.sample_floor_le_polynomial line 86
  8. theorem OAI.Problem355.pair_error_le_inverse_pow line 99
  9. theorem OAI.Problem355.sample_floor_square_bound line 111
  10. theorem OAI.Problem355.triple_error_le_log_majorant line 128
  11. theorem OAI.Problem355.tendsto_alteration_error_majorant line 145
  12. theorem OAI.Problem355.alteration_error_eventually_lt_one line 158