OAI/Probability/FreeIsing/Ising/ContinuousRootResponse.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem367.IsingObservationFactor.continuous_tanh line 15
  2. def OAI.Problem367.IsingObservationFactor.siteRootResponse line 18
  3. lemma OAI.Problem367.IsingObservationFactor.continuous_siteRootResponse line 25
  4. lemma OAI.Problem367.IsingObservationFactor.siteRootResponse_mem_Icc line 36
  5. def OAI.Problem367.IsingObservationFactor.continuousRootResponse line 54
  6. lemma OAI.Problem367.IsingObservationFactor.continuousRootResponse_progressive line 58
  7. lemma OAI.Problem367.IsingObservationFactor.continuousRootResponse_abs_le_one line 65
  8. theorem OAI.Problem367.IsingObservationFactor.continuousRootResponse_continuous_ae line 70
  9. theorem OAI.Problem367.IsingObservationFactor.continuousRootResponse_eq_response_ae line 79
  10. def OAI.Problem367.IsingObservationFactor.continuousRootCovariance line 95
  11. lemma OAI.Problem367.IsingObservationFactor.continuousRootCovariance_progressive line 100
  12. lemma OAI.Problem367.IsingObservationFactor.continuousRootCovariance_abs_le_one line 108
  13. theorem OAI.Problem367.IsingObservationFactor.continuousRootCovariance_continuous_ae line 118
  14. theorem OAI.Problem367.IsingObservationFactor.continuousRootCovariance_eq_covariance_ae line 127