OAI/InformationTheory/PhotonNumber/BeamTrace.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Annihilation.weight_down line 22
  2. def OAI.BeamLadder.W line 32
  3. theorem OAI.BeamLadder.W_one_le line 34
  4. def OAI.BeamLadder.upL line 38
  5. def OAI.BeamLadder.upR line 39
  6. theorem OAI.BeamLadder.upL_inj line 41
  7. theorem OAI.BeamLadder.upR_inj line 45
  8. theorem OAI.BeamLadder.W_upL line 49
  9. theorem OAI.BeamLadder.W_upR line 52
  10. theorem OAI.BeamLadder.up_update line 56
  11. theorem OAI.BeamLadder.coordinate_le line 62
  12. theorem OAI.BeamLadder.lowerL_bound line 67
  13. theorem OAI.BeamLadder.lowerR_bound line 76
  14. def OAI.BeamLadder.lowerL line 85
  15. def OAI.BeamLadder.lowerR line 88
  16. theorem OAI.BeamLadder.lowerL_apply line 91
  17. theorem OAI.BeamLadder.lowerR_apply line 93
  18. theorem OAI.BeamLadder.lowerL_single line 96
  19. theorem OAI.BeamLadder.lowerR_single line 117
  20. theorem OAI.BeamLadder.coefficient_W line 138
  21. theorem OAI.BeamLadder.inverse_W_coefficient line 153
  22. theorem OAI.BeamLadder.retained_covariance line 163
  23. theorem OAI.EntropyPhotonNumber.beam_discarded_lower line 190
  24. theorem OAI.BeamLadder.inverse_W_coefficient_right line 204
  25. theorem OAI.BeamLadder.discarded_covariance line 214
  26. def OAI.BeamLadder.radial line 245
  27. theorem OAI.BeamLadder.radial_apply line 250
  28. theorem OAI.BeamLadder.radial_single line 255
  29. theorem OAI.BeamLadder.radial_covariance line 266
  30. theorem OAI.BeamLadder.adjoint_covariance line 286
  31. theorem OAI.BeamLadder.retained_adjoint_covariance line 306
  32. theorem OAI.BeamLadder.discarded_adjoint_covariance line 313
  33. def OAI.BeamLadder.increase line 325
  34. theorem OAI.BeamLadder.W_nat line 327
  35. theorem OAI.BeamLadder.increase_bound line 332
  36. def OAI.BeamLadder.raiseL line 344
  37. def OAI.BeamLadder.raiseR line 347
  38. theorem OAI.BeamLadder.retained_creation_covariance line 350
  39. theorem OAI.BeamLadder.discarded_creation_covariance line 361
  40. theorem OAI.BeamLadder.raiseL_up line 372
  41. theorem OAI.BeamLadder.raiseR_up line 382
  42. theorem OAI.BeamLadder.raiseL_zero line 392
  43. theorem OAI.BeamLadder.raiseR_zero line 402
  44. theorem OAI.BeamLadder.inverse_bound line 418
  45. def OAI.BeamLadder.inverse line 422
  46. theorem OAI.BeamLadder.inverse_apply line 425
  47. theorem OAI.BeamLadder.inverse_selfAdjoint line 430
  48. theorem OAI.BeamLadder.inverse_covariance line 439
  49. theorem OAI.BeamLadder.slice_raiseR_up line 444
  50. theorem OAI.BeamLadder.slice_raiseR_zero line 455
  51. theorem OAI.BeamLadder.discarded_commutator_operator line 461
  52. theorem OAI.BeamLadder.discarded_commutator line 491
  53. def OAI.BeamLadder.conjugate line 504
  54. theorem OAI.BeamLadder.conjugate_inner line 509
  55. theorem OAI.BeamLadder.covariance_lower_apply line 515
  56. theorem OAI.BeamLadder.covariance_raise_apply line 522
  57. theorem OAI.BeamLadder.covariance_inverse_apply line 529
  58. theorem OAI.BeamLadder.covariance_discarded_lower_apply line 533
  59. theorem OAI.BeamLadder.covariance_discarded_raise_apply line 540
  60. theorem OAI.BeamLadder.two_port_algebra line 547
  61. def OAI.BeamLadder.weakL line 554
  62. def OAI.BeamLadder.weakR line 559
  63. theorem OAI.BeamLadder.physical_weak_covariance line 564
  64. def OAI.BeamLadder.tensorPreimage line 591
  65. theorem OAI.BeamLadder.tensorPreimage_apply line 596
  66. theorem OAI.BeamLadder.tensorPreimage_inverse line 605
  67. theorem OAI.BeamLadder.tensorPreimage_lowerL line 614
  68. theorem OAI.BeamLadder.tensorPreimage_lowerR line 628
  69. theorem OAI.BeamLadder.tensorPreimage_raiseL line 642
  70. theorem OAI.BeamLadder.tensorPreimage_raiseR line 656
  71. theorem OAI.BeamLadder.square_add_summable line 670
  72. theorem OAI.BeamLadder.tensorPreimage_summable line 679
  73. def OAI.KrausBounded.wave line 707
  74. theorem OAI.KrausBounded.wave_apply line 712
  75. theorem OAI.KrausBounded.wave_square line 715
  76. def OAI.KrausBounded.linearMap line 721
  77. theorem OAI.KrausBounded.wave_bound line 727
  78. def OAI.KrausBounded.lift line 734
  79. theorem OAI.KrausBounded.sum_bound line 739
  80. def OAI.KrausBounded.analysis line 750
  81. def OAI.KrausBounded.acted line 754
  82. def OAI.KrausBounded.dual line 759
  83. theorem OAI.KrausBounded.dual_entry line 762
  84. theorem OAI.KrausBounded.analysis_norm line 770
  85. theorem OAI.KrausBounded.acted_norm line 777
  86. theorem OAI.KrausBounded.dual_norm line 783
  87. theorem OAI.KrausBounded.dual_add line 796
  88. theorem OAI.KrausBounded.dual_smul line 805
  89. theorem OAI.KrausBounded.dual_adjoint line 813
  90. theorem OAI.KrausBounded.dual_selfAdjoint line 824
  91. theorem OAI.TensorLp.rightFamily_norm line 835
  92. theorem OAI.TensorLp.leftFamily_norm line 838
  93. def OAI.TensorLp.conditionalLeft line 842
  94. def OAI.TensorLp.conditionalRight line 846
  95. theorem OAI.TensorLp.conditionalLeft_entry line 850
  96. theorem OAI.TensorLp.conditionalRight_entry line 855
  97. theorem OAI.TensorLp.tensorFamily_summable line 860
  98. theorem OAI.TensorLp.pairing_conditionalLeft line 865
  99. theorem OAI.TensorLp.pairing_conditionalRight line 876
  100. def OAI.BeamLadder.singleWeak line 899
  101. theorem OAI.BeamLadder.weakL_summable line 905
  102. theorem OAI.BeamLadder.weakR_summable line 914
  103. theorem OAI.BeamLadder.weakL_product line 923
  104. theorem OAI.BeamLadder.weakR_product line 942
  105. theorem OAI.BeamLadder.product_weak_covariance line 961
  106. theorem OAI.EntropyPhotonNumber.entry_ext line 994
  107. theorem OAI.TensorLp.slice_family_summable line 1012
  108. theorem OAI.TensorLp.pairing_liftLeft line 1018
  109. theorem OAI.CrossEnsemble.coordinate_hasSum line 1035
  110. theorem OAI.CrossEnsemble.shifted_right_operator_eq line 1041
  111. theorem OAI.CrossEnsemble.shifted_left_operator_eq line 1065
  112. theorem OAI.BeamLadder.lowerL_inverse_apply line 1094
  113. theorem OAI.BeamLadder.raiseL_inverse_apply line 1102
  114. theorem OAI.BeamLadder.single_lower_inverse_apply line 1111
  115. theorem OAI.BeamLadder.single_raise_inverse_apply line 1117
  116. theorem OAI.BeamLadder.output_weak line 1126
  117. theorem OAI.TensorLp.hasSum_slice_family line 1164
  118. def OAI.TensorLp.partialTrace line 1178
  119. theorem OAI.TensorLp.partialTrace_positive line 1181
  120. theorem OAI.TensorLp.partialTrace_trace line 1185
  121. theorem OAI.TensorLp.partialTrace_entry line 1190
  122. theorem OAI.TraceEnsemble.hasSum_tensor_norm line 1212
  123. theorem OAI.TraceEnsemble.tensor_entry line 1218
  124. theorem OAI.TraceEnsemble.unitary_entry line 1238
  125. theorem OAI.EntropyPhotonNumber.beam_ensemble_entry line 1257