OAI/Probability/FreeIsing/Estimates/EndpointTimeScale.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.inv_sqrt_sq_time line 9
  2. theorem OAI.Problem367.mul_sqrt_eq_three_halves line 13
  3. theorem OAI.Problem367.inv_sqrt_mul_sqrt_time line 23
  4. theorem OAI.Problem367.inv_sqrt_le_time_three_quarters line 29
  5. theorem OAI.Problem367.quadratic_endpoint_time_scale line 40
  6. theorem OAI.Problem367.linear_endpoint_time_scale line 52
  7. theorem OAI.Problem367.sqrt_endpoint_time_scale line 69
  8. def OAI.Problem367.endpointTimeConstant line 82
  9. theorem OAI.Problem367.endpointTimeConstant_ge_one line 86
  10. theorem OAI.Problem367.endpoint_time_scales line 89