OAI/Probability/FreeIsing/Ising/ContinuousCopyCoefficients.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.IsingContinuousCopyCoefficients.response line 16
  2. def OAI.Problem367.IsingContinuousCopyCoefficients.covariance line 20
  3. lemma OAI.Problem367.IsingContinuousCopyCoefficients.projection_measurable line 24
  4. lemma OAI.Problem367.IsingContinuousCopyCoefficients.projection_preserving line 29
  5. lemma OAI.Problem367.IsingContinuousCopyCoefficients.field_progressive line 38
  6. lemma OAI.Problem367.IsingContinuousCopyCoefficients.response_progressive line 51
  7. lemma OAI.Problem367.IsingContinuousCopyCoefficients.continuous_tanh line 58
  8. lemma OAI.Problem367.IsingContinuousCopyCoefficients.covariance_progressive line 61
  9. lemma OAI.Problem367.IsingContinuousCopyCoefficients.response_abs_le_one line 69
  10. lemma OAI.Problem367.IsingContinuousCopyCoefficients.covariance_abs_le_one line 73
  11. lemma OAI.Problem367.IsingContinuousCopyCoefficients.covariance_sq_le_response_sq line 77
  12. lemma OAI.Problem367.IsingContinuousCopyCoefficients.response_continuous_ae line 88
  13. lemma OAI.Problem367.IsingContinuousCopyCoefficients.covariance_continuous_ae line 96
  14. lemma OAI.Problem367.IsingContinuousCopyCoefficients.response_eq_raw_ae line 104
  15. lemma OAI.Problem367.IsingContinuousCopyCoefficients.covariance_eq_raw_ae line 113
  16. lemma OAI.Problem367.IsingContinuousCopyCoefficients.real_measurable line 122
  17. lemma OAI.Problem367.IsingContinuousCopyCoefficients.sq_time_integrable line 128
  18. theorem OAI.Problem367.IsingContinuousCopyCoefficients.response_row_energy line 142
  19. theorem OAI.Problem367.IsingContinuousCopyCoefficients.response_energy_summable line 168
  20. theorem OAI.Problem367.IsingContinuousCopyCoefficients.covariance_energy_summable line 185