OAI/Probability/FreeIsing/Energy/Attenuation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.responseAttenuation line 9
  2. lemma OAI.Problem367.attenuation_denominator_pos line 12
  3. lemma OAI.Problem367.responseAttenuation_pos line 18
  4. lemma OAI.Problem367.responseAttenuation_le_one line 23
  5. lemma OAI.Problem367.responseAttenuation_zero line 29
  6. lemma OAI.Problem367.responseAttenuation_neg line 33
  7. lemma OAI.Problem367.hasDerivAt_tanh_response line 37
  8. lemma OAI.Problem367.hasDerivAt_log_responseAttenuation line 47
  9. lemma OAI.Problem367.abs_deriv_log_responseAttenuation_le line 62
  10. lemma OAI.Problem367.abs_deriv_log_responseAttenuation_le_two line 74
  11. lemma OAI.Problem367.deriv_log_responseAttenuation_zero line 80
  12. lemma OAI.Problem367.lipschitzWith_log_responseAttenuation line 86
  13. lemma OAI.Problem367.lipschitzWith_tanh_response line 94
  14. lemma OAI.Problem367.abs_tanh_le_abs_response line 105
  15. lemma OAI.Problem367.log_responseAttenuation_small_field line 109
  16. lemma OAI.Problem367.log_responseAttenuation_nonpos line 122
  17. lemma OAI.Problem367.responseAttenuation_le_one_sub line 127
  18. lemma OAI.Problem367.responseAttenuation_le_exp line 134
  19. lemma OAI.Problem367.log_responseAttenuation_small_field_sq line 143