OAI/Probability/FreeIsing/Ising/ContinuousResponseEnergy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.IsingObservationFactor.measurable_real_of_progressive line 16
  2. theorem OAI.Problem367.IsingObservationFactor.measurable_response_real line 26
  3. theorem OAI.Problem367.IsingObservationFactor.measurable_covariance_real line 30
  4. theorem OAI.Problem367.IsingObservationFactor.continuousRootResponse_row_eq_ae line 34
  5. theorem OAI.Problem367.IsingObservationFactor.continuousRootResponse_row_energy line 50
  6. theorem OAI.Problem367.IsingObservationFactor.continuousRootResponse_hasSum_timeEnergy line 76
  7. theorem OAI.Problem367.IsingObservationFactor.continuousRootCovariance_sq_le_response_sq line 89
  8. theorem OAI.Problem367.IsingObservationFactor.continuousRootCovariance_row_energy line 101
  9. theorem OAI.Problem367.IsingObservationFactor.continuousRootCovariance_hasSum_timeEnergy line 137