OAI/Probability/ClassicalON/AmplitudePartition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalON.amplitudeCoupling line 17
  2. def OAI.ClassicalON.amplitudePartition line 19
  3. def OAI.ClassicalON.amplitudeSlope line 22
  4. theorem OAI.ClassicalON.continuous_amplitudeHamiltonian line 26
  5. theorem OAI.ClassicalON.amplitudePartition_pos line 32
  6. theorem OAI.ClassicalON.continuous_amplitudePartition line 36
  7. theorem OAI.ClassicalON.amplitudeHamiltonian_direction_derivative line 41
  8. theorem OAI.ClassicalON.log_amplitudePartition_direction_derivative line 53
  9. theorem OAI.ClassicalON.amplitudeCoupling_mono line 76
  10. theorem OAI.ClassicalON.amplitudeSlope_nonneg line 84
  11. theorem OAI.ClassicalON.amplitudeSlope_mono line 93