OAI/InformationTheory/PhotonNumber/BeamForms.lean

GitHub source file

143 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BeamLadder.physical_ensemble_output line 25
  2. theorem OAI.BeamLadder.cross_slice_eq_partialTrace line 39
  3. theorem OAI.BeamLadder.physical_weighted_output line 45
  4. theorem OAI.BeamLadder.physical_product_weak line 66
  5. def OAI.BeamLadder.preLowerL line 95
  6. def OAI.BeamLadder.preLowerR line 96
  7. def OAI.BeamLadder.preRaiseL line 97
  8. def OAI.BeamLadder.preRaiseR line 98
  9. theorem OAI.BeamLadder.inverse_preLowerL line 100
  10. theorem OAI.BeamLadder.inverse_preLowerR line 112
  11. theorem OAI.BeamLadder.inverse_preRaiseL line 124
  12. theorem OAI.BeamLadder.inverse_preRaiseR line 140
  13. def OAI.BeamLadder.quadMinusL line 156
  14. def OAI.BeamLadder.quadMinusR line 160
  15. def OAI.BeamLadder.quadPlusL line 164
  16. def OAI.BeamLadder.quadPlusR line 168
  17. theorem OAI.BeamLadder.liftLeft_adjoint_inner line 173
  18. theorem OAI.BeamLadder.discarded_commutator_star line 181
  19. theorem OAI.BeamLadder.quadMinusR_zero line 188
  20. theorem OAI.BeamLadder.quadPlusR_zero line 197
  21. theorem OAI.BeamLadder.inverse_injective line 206
  22. theorem OAI.BeamLadder.cross_raise_lower line 215
  23. theorem OAI.BeamLadder.cross_lower_raise line 242
  24. def OAI.BeamLadder.crossMinus line 268
  25. def OAI.BeamLadder.crossPlus line 276
  26. theorem OAI.BeamLadder.cross_heat_zero line 284
  27. theorem OAI.BeamLadder.covariance_preLowerL line 297
  28. theorem OAI.BeamLadder.covariance_preLowerR line 305
  29. theorem OAI.BeamLadder.covariance_preRaiseL line 313
  30. theorem OAI.BeamLadder.covariance_preRaiseR line 321
  31. theorem OAI.BeamLadder.undo_rotation line 329
  32. theorem OAI.BeamLadder.beam_squares line 341
  33. theorem OAI.BeamLadder.undo_lowerL line 347
  34. theorem OAI.BeamLadder.undo_lowerR line 352
  35. theorem OAI.BeamLadder.undo_raiseL line 357
  36. theorem OAI.BeamLadder.undo_raiseR line 362
  37. theorem OAI.BeamLadder.undo_preLowerL line 367
  38. theorem OAI.BeamLadder.undo_preLowerR line 372
  39. theorem OAI.BeamLadder.undo_preRaiseL line 377
  40. theorem OAI.BeamLadder.undo_preRaiseR line 382
  41. theorem OAI.BeamLadder.expand_quadMinusL line 387
  42. theorem OAI.BeamLadder.expand_quadMinusR line 400
  43. theorem OAI.BeamLadder.expand_quadPlusL line 413
  44. theorem OAI.BeamLadder.expand_quadPlusR line 426
  45. theorem OAI.BeamLadder.generator_covariance line 439
  46. theorem OAI.BeamLadder.numberL_minus line 454
  47. theorem OAI.BeamLadder.numberL_plus line 470
  48. theorem OAI.BeamLadder.numberR_minus line 483
  49. theorem OAI.BeamLadder.numberR_plus line 499
  50. def OAI.BeamLadder.tensorPreimage2 line 518
  51. theorem OAI.BeamLadder.tensorPreimage2_apply line 526
  52. theorem OAI.BeamLadder.tensorPreimage2_inverse line 536
  53. theorem OAI.BeamLadder.square_smul_summable line 545
  54. theorem OAI.BeamLadder.tensorPreimage2_summable line 550
  55. theorem OAI.BeamLadder.dissipator_summable line 572
  56. theorem OAI.BeamLadder.quadMinusL_summable line 586
  57. theorem OAI.BeamLadder.quadPlusL_summable line 592
  58. theorem OAI.BeamLadder.quadMinusR_summable line 598
  59. theorem OAI.BeamLadder.quadPlusR_summable line 604
  60. def OAI.BeamLadder.generatorPairingL line 610
  61. def OAI.BeamLadder.generatorPairingR line 614
  62. theorem OAI.BeamLadder.generatorPairing_covariance line 619
  63. theorem OAI.BeamLadder.tensorPreimage2_numberL_minus line 656
  64. theorem OAI.BeamLadder.tensorPreimage2_numberL_plus line 668
  65. theorem OAI.BeamLadder.tensorPreimage2_numberR_minus line 680
  66. theorem OAI.BeamLadder.tensorPreimage2_numberR_plus line 692
  67. def OAI.BeamLadder.singleGeneratorPairing line 704
  68. theorem OAI.BeamLadder.generatorPairingL_product line 714
  69. theorem OAI.CrossEnsemble.shifted_both_operator_eq line 773
  70. theorem OAI.BeamLadder.lowerL_second_inverse_apply line 805
  71. theorem OAI.BeamLadder.raiseL_second_inverse_apply line 809
  72. theorem OAI.BeamLadder.single_lower_third_apply line 823
  73. theorem OAI.BeamLadder.single_raise_third_apply line 830
  74. theorem OAI.BeamLadder.single_number_third_apply line 842
  75. theorem OAI.BeamLadder.slice_dissipator line 857
  76. theorem OAI.BeamLadder.output_generator line 893
  77. theorem OAI.BeamLadder.generatorPairingR_product line 937
  78. theorem OAI.BeamLadder.physical_product_generator line 995
  79. def OAI.BeamLadder.tensorRatio line 1033
  80. def OAI.BeamLadder.retainedRatio line 1036
  81. theorem OAI.BeamLadder.tensorRatio_mem line 1038
  82. theorem OAI.BeamLadder.retainedRatio_mem line 1047
  83. theorem OAI.BeamLadder.ratioSquare_norm line 1053
  84. def OAI.BeamLadder.tensorRatioCLM line 1057
  85. def OAI.BeamLadder.retainedRatioCLM line 1061
  86. theorem OAI.BeamLadder.tensorRatioCLM_norm line 1065
  87. theorem OAI.BeamLadder.retainedRatioCLM_norm line 1071
  88. def OAI.BeamLadder.weightedColumn line 1077
  89. theorem OAI.BeamLadder.weightedColumn_apply line 1081
  90. theorem OAI.BeamLadder.weightedColumn_norm line 1084
  91. theorem OAI.BeamLadder.weightedColumn_summable line 1095
  92. theorem OAI.BeamLadder.tensorRatio_inverse line 1101
  93. theorem OAI.BeamLadder.retainedRatio_inverse line 1113
  94. theorem OAI.BeamLadder.weightedColumn_inverse line 1124
  95. def OAI.EnsemblePullback.compression line 1139
  96. theorem OAI.EnsemblePullback.compression_norm line 1142
  97. theorem OAI.EnsemblePullback.summable_norm_compression line 1150
  98. theorem OAI.EnsemblePullback.summable_compression line 1154
  99. def OAI.EnsemblePullback.pullback line 1159
  100. theorem OAI.EnsemblePullback.pullback_norm line 1162
  101. theorem OAI.EnsemblePullback.compression_entry line 1168
  102. theorem OAI.EnsemblePullback.hasSum_entry line 1172
  103. theorem OAI.EnsemblePullback.compression_positive line 1180
  104. theorem OAI.EnsemblePullback.pullback_positive line 1183
  105. theorem OAI.EnsemblePullback.pullback_add line 1189
  106. theorem OAI.EnsemblePullback.pullback_smul line 1195
  107. def OAI.EnsemblePullback.map line 1201
  108. theorem OAI.EnsemblePullback.applied_family_summable line 1218
  109. theorem OAI.EnsemblePullback.pairing_pullback line 1230
  110. def OAI.BeamLadder.weightedConditional line 1246
  111. def OAI.BeamLadder.weightedSlices line 1250
  112. theorem OAI.BeamLadder.weightedSlices_summable line 1254
  113. theorem OAI.BeamLadder.weighted_pairing_slicing line 1264
  114. theorem OAI.CrossEnsemble.rankOne_trace line 1282
  115. theorem OAI.CrossEnsemble.pairing_selfAdjoint_sandwich line 1292
  116. theorem OAI.Annihilation.inverseWeight_rankOne_range line 1306
  117. theorem OAI.Annihilation.inverseWeight_rankOne line 1318
  118. theorem OAI.Annihilation.weighted_trace_ext line 1327
  119. theorem OAI.BeamLadder.gain_inverse_apply line 1356
  120. theorem OAI.BeamLadder.inverse_two_one line 1363
  121. theorem OAI.BeamLadder.weighted_pairing_physical line 1366
  122. def OAI.WeightedGenerator.pushedDissipator line 1380
  123. def OAI.WeightedGenerator.pushedGenerator line 1386
  124. def OAI.WeightedGenerator.pushedPairing line 1389
  125. theorem OAI.WeightedGenerator.pushedPairing_hasSum line 1398
  126. theorem OAI.WeightedGenerator.pushedPairing_slicing line 1418
  127. theorem OAI.BeamLadder.weightedSlices_inverse line 1440
  128. theorem OAI.BeamLadder.weighted_pairing_bounded_physical line 1447
  129. def OAI.BeamLadder.weightedColumnRight line 1476
  130. theorem OAI.BeamLadder.weightedColumnRight_apply line 1480
  131. theorem OAI.BeamLadder.weightedColumnRight_norm line 1483
  132. theorem OAI.BeamLadder.weightedColumnRight_summable line 1494
  133. theorem OAI.BeamLadder.weightedColumnRight_inverse line 1500
  134. def OAI.BeamLadder.weightedConditionalRight line 1506
  135. def OAI.BeamLadder.weightedSlicesRight line 1510
  136. theorem OAI.BeamLadder.weightedSlicesRight_summable line 1514
  137. theorem OAI.BeamLadder.weighted_pairing_slicing_right line 1523
  138. theorem OAI.BeamLadder.weightedSlicesRight_inverse line 1536
  139. theorem OAI.BeamLadder.weighted_pairing_bounded_physical_right line 1543
  140. theorem OAI.BeamLadder.weighted_pushed_pairing_physical line 1578
  141. theorem OAI.BeamLadder.weighted_pushed_pairing_physical_right line 1592
  142. theorem OAI.BeamLadder.weighted_product_generator line 1606
  143. theorem OAI.CrossEnsemble.entry_transform line 1668