OAI/MathematicalPhysics/Fock/Operators.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WeightedShift.H line 15
  2. theorem OAI.WeightedShift.hasSum_square line 17
  3. theorem OAI.WeightedShift.pull_mem line 20
  4. def OAI.WeightedShift.pull line 31
  5. theorem OAI.WeightedShift.pull_apply line 34
  6. theorem OAI.WeightedShift.pull_bound line 38
  7. def OAI.WeightedShift.pullCLM line 53
  8. theorem OAI.WeightedShift.pullCLM_apply line 68
  9. theorem OAI.WeightedShift.pullCLM_single line 74
  10. theorem OAI.WeightedShift.pullCLM_single_outside line 86
  11. theorem OAI.WeightedShift.adjoint_apply_image line 93
  12. theorem OAI.WeightedShift.adjoint_apply_outside line 102
  13. def OAI.Annihilation.up line 116
  14. theorem OAI.Annihilation.up_same line 117
  15. theorem OAI.Annihilation.up_other line 118
  16. theorem OAI.Annihilation.up_injective line 119
  17. theorem OAI.Annihilation.weight_up line 122
  18. theorem OAI.Annihilation.coordinate_le_weight line 130
  19. theorem OAI.Annihilation.sqrt_step_le_weight line 136
  20. def OAI.Annihilation.coefficient line 144
  21. theorem OAI.Annihilation.coefficient_bound line 147
  22. def OAI.Annihilation.sandwich line 163
  23. theorem OAI.Annihilation.sandwich_apply line 166
  24. theorem OAI.Annihilation.sandwich_norm_le line 169
  25. theorem OAI.Annihilation.sqrt_step_le_base line 181
  26. def OAI.Annihilation.creationCoefficient line 187
  27. theorem OAI.Annihilation.creationCoefficient_bound line 190
  28. def OAI.Annihilation.creationSandwich line 207
  29. theorem OAI.Annihilation.creationSandwich_norm_le line 211
  30. theorem OAI.Annihilation.creationSandwich_up line 218
  31. theorem OAI.Annihilation.creationSandwich_zero line 223
  32. def OAI.Annihilation.down line 232
  33. theorem OAI.Annihilation.up_down line 233
  34. theorem OAI.Annihilation.down_up line 238
  35. theorem OAI.Annihilation.index_cases line 244
  36. theorem OAI.Annihilation.coefficient_inverse_bound line 249
  37. def OAI.Annihilation.inverseWeight line 253
  38. theorem OAI.Annihilation.inverseWeight_apply line 256
  39. theorem OAI.Annihilation.inverseWeight_injective line 259
  40. theorem OAI.Annihilation.inverseWeight_add line 267
  41. theorem OAI.Annihilation.sandwich_factor line 272
  42. theorem OAI.Annihilation.creationSandwich_factor line 280
  43. def OAI.Annihilation.lowering line 299
  44. def OAI.Annihilation.raising line 300
  45. theorem OAI.Annihilation.lowering_apply line 302
  46. theorem OAI.Annihilation.raising_up line 308
  47. theorem OAI.Annihilation.raising_zero line 314
  48. theorem OAI.Annihilation.lowering_sq line 317
  49. theorem OAI.Annihilation.raising_sq line 322
  50. theorem OAI.Annihilation.lowering_norm_sum line 327
  51. theorem OAI.Annihilation.raising_norm_sum line 339
  52. theorem OAI.Annihilation.canonical_norm_identity line 349
  53. theorem OAI.Annihilation.inverseWeight_selfAdjoint line 359
  54. theorem OAI.Annihilation.lowering_adjoint_inverse line 369
  55. theorem OAI.Annihilation.ladder_adjoint_pairing line 393
  56. def OAI.CrossEnsemble.operator line 406
  57. theorem OAI.CrossEnsemble.norm_product_summable line 409
  58. theorem OAI.CrossEnsemble.hasSum_operator line 415
  59. theorem OAI.CrossEnsemble.entry_hasSum line 422
  60. theorem OAI.CrossEnsemble.square_coordinates_summable line 430
  61. theorem OAI.CrossEnsemble.trace_norm_summable line 445
  62. def OAI.CrossEnsemble.pairing line 454
  63. theorem OAI.CrossEnsemble.applied_summable line 457
  64. theorem OAI.CrossEnsemble.pairing_summable line 466
  65. theorem OAI.CrossEnsemble.trace_hasSum line 472
  66. theorem OAI.CrossEnsemble.operator_comp_left line 487
  67. theorem OAI.CrossEnsemble.pairing_trace line 503
  68. theorem OAI.CrossEnsemble.pairing_eq_of_operator_eq line 510
  69. theorem OAI.CrossEnsemble.operator_adjoint line 524
  70. theorem OAI.CrossEnsemble.operator_sandwich line 542
  71. def OAI.Annihilation.modeBound line 557
  72. theorem OAI.Annihilation.modeBound_apply line 568
  73. theorem OAI.Annihilation.modeBound_selfAdjoint line 572
  74. theorem OAI.Annihilation.modeBound_inverse_commute line 581
  75. theorem OAI.Annihilation.sandwich_right_inverse line 587
  76. theorem OAI.Annihilation.creationSandwich_right_inverse line 594
  77. def OAI.Annihilation.gain line 606
  78. def OAI.Annihilation.unweightedGain line 609
  79. theorem OAI.Annihilation.gain_factor line 612
  80. theorem OAI.Annihilation.quadratic_coordinate line 618
  81. theorem OAI.Annihilation.mode_quadratic line 628
  82. def OAI.WeightedGenerator.dissipator line 655
  83. def OAI.WeightedGenerator.generator line 660
  84. def OAI.WeightedGenerator.pairing line 663
  85. theorem OAI.WeightedGenerator.pairing_hasSum line 671