OAI/Probability/FreeIsing/Energy/ShiftedFieldVariance.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem367.strictMono_tanh_response line 11
  2. lemma OAI.Problem367.tanh_abs_response line 17
  3. lemma OAI.Problem367.tanh_one_pos_response line 21
  4. lemma OAI.Problem367.sq_le_cosh_sq_mul_tanh_sq line 25
  5. lemma OAI.Problem367.tanh_one_sq_le_of_one_le_abs line 42
  6. lemma OAI.Problem367.integrable_tanh_shift_sq line 54
  7. lemma OAI.Problem367.variance_le_cosh_sq_mul_tanh_shift_integral line 63
  8. lemma OAI.Problem367.variance_le_beta_sq_of_abs_le line 89
  9. lemma OAI.Problem367.variance_le_tanh_shift_integral_of_far line 97
  10. lemma OAI.Problem367.variance_le_uniform_tanh_shift_integral line 125
  11. lemma OAI.Problem367.exists_pos_uniform_shifted_tanh_variance line 137
  12. lemma OAI.Problem367.continuous_responseAttenuation line 153
  13. lemma OAI.Problem367.integral_responseAttenuation_shift_sq_le line 160
  14. lemma OAI.Problem367.exists_pos_uniform_shifted_attenuation_loss line 189