OAI/MathematicalPhysics/Fock/Beam.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FischerBeam.weight line 19
  2. def OAI.FischerBeam.pairing line 23
  3. theorem OAI.FischerBeam.pairing_monomial line 27
  4. theorem OAI.FischerBeam.weight_zero line 38
  5. theorem OAI.FischerBeam.pairing_one line 41
  6. theorem OAI.FischerBeam.weight_add_single line 47
  7. theorem OAI.FischerBeam.pairing_X_left line 61
  8. theorem OAI.FischerBeam.pairing_comm line 71
  9. abbrev OAI.FischerBeam.Poly line 83
  10. def OAI.FischerBeam.creatorA line 85
  11. def OAI.FischerBeam.creatorB line 87
  12. def OAI.FischerBeam.derivA line 89
  13. def OAI.FischerBeam.derivB line 91
  14. theorem OAI.FischerBeam.derivA_creatorA line 93
  15. theorem OAI.FischerBeam.derivA_creatorB line 101
  16. theorem OAI.FischerBeam.derivB_creatorA line 104
  17. theorem OAI.FischerBeam.derivB_creatorB line 107
  18. theorem OAI.FischerBeam.pairing_creatorA line 116
  19. theorem OAI.FischerBeam.pairing_creatorB line 120
  20. def OAI.FischerBeam.rotated line 125
  21. theorem OAI.FischerBeam.derivA_rotated line 127
  22. theorem OAI.FischerBeam.derivB_rotated line 133
  23. theorem OAI.FischerBeam.constantCoeff_rotated line 139
  24. theorem OAI.FischerBeam.pairing_rotated line 146
  25. def OAI.FischerBeam.degree line 187
  26. theorem OAI.FischerBeam.degree_zero line 189
  27. theorem OAI.FischerBeam.degree_one line 190
  28. theorem OAI.FischerBeam.degree_eq_iff line 192
  29. theorem OAI.FischerBeam.degree_add line 199
  30. theorem OAI.FischerBeam.weight_degree line 203
  31. theorem OAI.FischerBeam.linear_power line 207
  32. theorem OAI.FischerBeam.rotated_expansion line 223
  33. theorem OAI.FischerBeam.coeff_rotated line 240
  34. theorem OAI.FischerBeam.degree_coordinates line 271
  35. theorem OAI.FischerBeam.sector_reconstruction line 276
  36. theorem OAI.FischerBeam.rotated_sector line 300
  37. theorem OAI.FischerBeam.pairing_rotated_coefficients line 308
  38. def OAI.FischerBeam.sectorMatrix line 319
  39. theorem OAI.FischerBeam.sqrt_weight_degree_pos line 324
  40. theorem OAI.FischerBeam.sectorMatrix_columns line 330
  41. theorem OAI.FischerBeam.sectorMatrix_rows line 381
  42. def OAI.FischerBeam.multiSectorMatrix line 393
  43. theorem OAI.FischerBeam.multiSectorMatrix_columns line 397
  44. theorem OAI.FischerBeam.multiSectorMatrix_rows line 413
  45. def OAI.BlockUnitary.rotated line 444
  46. theorem OAI.BlockUnitary.inner_rotated_same line 448
  47. theorem OAI.BlockUnitary.inner_rotated_ne line 457
  48. theorem OAI.BlockUnitary.rotated_orthonormal line 469
  49. theorem OAI.BlockUnitary.inner_basis_rotated_same line 484
  50. theorem OAI.BlockUnitary.inner_basis_rotated_ne line 490
  51. theorem OAI.BlockUnitary.inverse_expansion line 499
  52. theorem OAI.BlockUnitary.rotated_dense line 521
  53. def OAI.BlockUnitary.basis line 535
  54. theorem OAI.BlockUnitary.basis_apply line 542
  55. def OAI.BlockUnitary.unitary line 550
  56. theorem OAI.BlockUnitary.unitary_apply_basis line 556
  57. def OAI.BlockUnitary.reindex line 571
  58. theorem OAI.BlockUnitary.reindex_apply line 580
  59. theorem OAI.BlockUnitary.unitary_symm_apply_basis line 583
  60. theorem OAI.EntropyPhotonNumber.oneModeBeamCoefficient_eq line 600
  61. abbrev OAI.EntropyPhotonNumber.PairedIndex line 610
  62. abbrev OAI.EntropyPhotonNumber.JointFock line 611
  63. abbrev OAI.EntropyPhotonNumber.NumberSector line 612
  64. def OAI.EntropyPhotonNumber.sectorEquiv line 615
  65. def OAI.EntropyPhotonNumber.jointNumberBasis line 636
  66. def OAI.EntropyPhotonNumber.jointSectorBasis line 639
  67. theorem OAI.EntropyPhotonNumber.jointNumberBasis_apply line 642
  68. theorem OAI.EntropyPhotonNumber.jointSectorBasis_apply line 646
  69. theorem OAI.EntropyPhotonNumber.beam_sectorCoefficient line 650
  70. theorem OAI.EntropyPhotonNumber.sqrt_beam_rotation line 657
  71. def OAI.EntropyPhotonNumber.beamUnitary line 663
  72. theorem OAI.EntropyPhotonNumber.beam_symm_sector line 679
  73. theorem OAI.EntropyPhotonNumber.beam_symm_number line 691
  74. theorem OAI.FischerBeam.pderiv_zero_rotated line 709
  75. theorem OAI.FischerBeam.pderiv_one_rotated line 716
  76. theorem OAI.FischerBeam.degree_add_zero line 722
  77. theorem OAI.FischerBeam.degree_add_one line 725
  78. theorem OAI.FischerBeam.coeff_lower_zero line 729
  79. theorem OAI.FischerBeam.coeff_lower_one line 739
  80. def OAI.FischerBeam.oscillatorCoefficient line 749
  81. theorem OAI.FischerBeam.sqrt_weight_succ_left line 753
  82. theorem OAI.FischerBeam.sqrt_weight_succ_right line 759
  83. theorem OAI.FischerBeam.sqrt_lower_left line 766
  84. theorem OAI.FischerBeam.sqrt_lower_right line 780
  85. theorem OAI.FischerBeam.oscillator_lower_zero line 794
  86. theorem OAI.FischerBeam.oscillator_lower_one line 810
  87. theorem OAI.EntropyPhotonNumber.oneMode_retained_lower line 833
  88. theorem OAI.EntropyPhotonNumber.oneMode_discarded_lower line 841
  89. theorem OAI.EntropyPhotonNumber.beam_product_lower line 848
  90. theorem OAI.EntropyPhotonNumber.beam_retained_lower line 881
  91. theorem OAI.EntropyPhotonNumber.beamCoefficient_sector_zero line 894
  92. theorem OAI.EntropyPhotonNumber.beamUnitary_apply_sector line 907
  93. theorem OAI.EntropyPhotonNumber.beam_coordinate_sector line 915
  94. theorem OAI.EntropyPhotonNumber.beam_coordinate line 927