OAI/Probability/ClassicalON/AmplitudeLaw.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ClassicalON.Amplitude line 11
  2. def OAI.ClassicalON.amplitudeReference line 13
  3. instance OAI.ClassicalON.amplitudeReference_isProbability line 15
  4. def OAI.ClassicalON.transverseAmplitude line 21
  5. theorem OAI.ClassicalON.continuous_transverseAmplitude line 23
  6. theorem OAI.ClassicalON.transverseAmplitude_nonneg line 26
  7. theorem OAI.ClassicalON.transverseAmplitude_antitone line 28
  8. theorem OAI.ClassicalON.transverseAmplitude_inf line 36
  9. theorem OAI.ClassicalON.transverseAmplitude_sup line 42
  10. def OAI.ClassicalON.isingAmplitudePartition line 50
  11. def OAI.ClassicalON.planarAmplitudePartition line 53
  12. def OAI.ClassicalON.amplitudeDensity line 56
  13. theorem OAI.ClassicalON.isingAmplitudePartition_pos line 59
  14. theorem OAI.ClassicalON.planarAmplitudePartition_pos line 63
  15. theorem OAI.ClassicalON.continuous_isingAmplitudePartition line 67
  16. theorem OAI.ClassicalON.continuous_planarAmplitudePartition line 73
  17. theorem OAI.ClassicalON.amplitudeDensity_pos line 79
  18. theorem OAI.ClassicalON.continuous_amplitudeDensity line 83
  19. theorem OAI.ClassicalON.isingAmplitudePartition_logSupermodular line 87
  20. theorem OAI.ClassicalON.planarAmplitudePartition_logSupermodular line 94
  21. theorem OAI.ClassicalON.amplitudeDensity_logSupermodular line 111
  22. theorem OAI.ClassicalON.amplitude_associated line 122
  23. theorem OAI.ClassicalON.amplitude_associated_any line 127