OAI/Probability/FreeIsing/Critical/Reduction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.log_sq_le_four_mul line 11
  2. theorem OAI.Problem367.log_three_halves_le_four_mul line 21
  3. theorem OAI.Problem367.sqrt_mul_sqrt_le_of_le_mul line 32
  4. theorem OAI.Problem367.endpoint_sums_critical_reduction line 49
  5. theorem OAI.Problem367.small_time_scale_reduction line 126
  6. theorem OAI.Problem367.critical_differential_bound_of_endpoint_sums line 155