OAI/Probability/FreeIsing/Ising/CopyEnergyIntegrability.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.IsingCopyEnergy.responseRow line 15
  2. theorem OAI.Problem367.IsingCopyEnergy.measurable_responseRow line 18
  3. theorem OAI.Problem367.IsingCopyEnergy.observation_extended_energy_le line 27
  4. theorem OAI.Problem367.IsingCopyEnergy.observation_row_energy_integrable line 71
  5. abbrev OAI.Problem367.IsingCopyEnergy.Joint line 92
  6. def OAI.Problem367.IsingCopyEnergy.projection line 94
  7. theorem OAI.Problem367.IsingCopyEnergy.projection_measurePreserving line 97
  8. def OAI.Problem367.IsingCopyEnergy.timeProjection line 108
  9. theorem OAI.Problem367.IsingCopyEnergy.timeProjection_measurePreserving line 111
  10. theorem OAI.Problem367.IsingCopyEnergy.copy_row_energy_integrable line 119
  11. def OAI.Problem367.IsingCopyEnergy.density line 137
  12. theorem OAI.Problem367.IsingCopyEnergy.density_integrable line 145
  13. theorem OAI.Problem367.IsingCopyEnergy.ae_integral_density_eq line 177