OAI/Probability/ClassicalON/GradientComplex.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalON.SpinSystem.normObservable line 14
  2. def OAI.ClassicalON.SpinSystem.reObservable line 17
  3. def OAI.ClassicalON.SpinSystem.imObservable line 20
  4. theorem OAI.ClassicalON.SpinSystem.averageLinear_nonneg line 23
  5. theorem OAI.ClassicalON.SpinSystem.averageLinear_mono line 27
  6. theorem OAI.ClassicalON.SpinSystem.averageLinear_mul_self_nonneg line 31
  7. theorem OAI.ClassicalON.SpinSystem.averageLinear_cauchySchwarz line 35
  8. theorem OAI.ClassicalON.SpinSystem.averageLinear_mul_le_sqrt line 53
  9. theorem OAI.ClassicalON.SpinSystem.norm_averageComplex_le line 60
  10. theorem OAI.ClassicalON.SpinSystem.complexEnergy_re line 75
  11. theorem OAI.ClassicalON.SpinSystem.complexEnergy_im line 82
  12. theorem OAI.ClassicalON.SpinSystem.complexEnergy_conj line 89
  13. theorem OAI.ClassicalON.SpinSystem.complex_gradient_current_bound line 94
  14. theorem OAI.ClassicalON.SpinSystem.averageComplex_re line 128
  15. theorem OAI.ClassicalON.SpinSystem.averageComplex_conj line 141
  16. theorem OAI.ClassicalON.SpinSystem.abs_localCoefficient_le line 155
  17. theorem OAI.ClassicalON.norm_square_le_one line 172
  18. theorem OAI.ClassicalON.mixedAB_norm_le line 177
  19. theorem OAI.ClassicalON.mixedAAB_norm_le line 190
  20. theorem OAI.ClassicalON.mixedABB_norm_le line 197
  21. theorem OAI.ClassicalON.mixedAABB_norm_le line 204