OAI/Probability/FreeIsing/Ising/ObservationResponseEnergy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.IsingObservationResponseEnergy.response line 20
  2. theorem OAI.Problem367.IsingObservationResponseEnergy.measurable_response line 23
  3. theorem OAI.Problem367.IsingObservationResponseEnergy.measurable_response_joint line 28
  4. theorem OAI.Problem367.IsingObservationResponseEnergy.observation_snapshot_identDistrib line 34
  5. theorem OAI.Problem367.IsingObservationResponseEnergy.lintegral_response_row_le line 40
  6. theorem OAI.Problem367.IsingObservationResponseEnergy.response_row_energy line 64
  7. def OAI.Problem367.IsingObservationResponseEnergy.copyObservation line 84
  8. theorem OAI.Problem367.IsingObservationResponseEnergy.measurePreserving_copyObservation line 87
  9. theorem OAI.Problem367.IsingObservationResponseEnergy.copy_response_row_energy line 93
  10. theorem OAI.Problem367.IsingObservationResponseEnergy.difference_response_row_energy line 108