OAI/Probability/FreeIsing/Critical/Comparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.exists_last_level_crossing line 11
  2. theorem OAI.Problem367.eq_zero_of_positive_interval_lower_bound line 45
  3. theorem OAI.Problem367.lower_bound_of_log_log_le line 72
  4. theorem OAI.Problem367.eq_zero_of_log_log_comparison line 93
  5. theorem OAI.Problem367.eq_zero_of_ae_deriv_le_mul_self line 111
  6. theorem OAI.Problem367.eq_zero_of_ae_osgood line 155