OAI/InformationTheory/PhotonNumber/Continuity.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EntropyPhotonNumber.mixedVector line 25
  2. theorem OAI.EntropyPhotonNumber.mixedVector_norm line 29
  3. def OAI.EntropyPhotonNumber.beamOutput line 34
  4. theorem OAI.EntropyPhotonNumber.mixedVector_entry line 41
  5. theorem OAI.EntropyPhotonNumber.beamOutput_spec line 63
  6. theorem OAI.BlockUnitary.finite_transform_norm_sq line 74
  7. theorem OAI.BlockUnitary.unitary_coordinate line 104
  8. theorem OAI.BlockUnitary.unitary_sector_mass line 117
  9. theorem OAI.BlockUnitary.unitary_weighted_mass line 127
  10. def OAI.TensorLp.vectorMoment line 147
  11. def OAI.TensorLp.matrixMoment line 150
  12. theorem OAI.TensorLp.vectorMoment_one line 153
  13. theorem OAI.TensorLp.matrixMoment_ensemble line 158
  14. theorem OAI.TensorLp.partialTrace_moment line 173
  15. theorem OAI.TensorLp.tensor_add_moment line 183
  16. theorem OAI.TensorLp.ensemble_tensor_add_moment line 199
  17. theorem OAI.EntropyPhotonNumber.beam_sector_weighted_mass line 220
  18. theorem OAI.EntropyPhotonNumber.beam_vector_moment line 228
  19. theorem OAI.EntropyPhotonNumber.beam_total_moment line 244
  20. def OAI.EntropyPhotonNumber.energyMoment line 251
  21. theorem OAI.EntropyPhotonNumber.energyMoment_eq line 254
  22. theorem OAI.EntropyPhotonNumber.finiteEnergy_iff line 259
  23. theorem OAI.EntropyPhotonNumber.beamOutput_energy_le line 271
  24. theorem OAI.EntropyPhotonNumber.beamOutput_finiteEnergy line 293
  25. theorem OAI.TensorLp.sum_slice_moment line 304
  26. def OAI.EntropyPhotonNumber.firstKraus line 314
  27. theorem OAI.EntropyPhotonNumber.firstKraus_apply line 319
  28. theorem OAI.EntropyPhotonNumber.firstKraus_norm line 323
  29. theorem OAI.EntropyPhotonNumber.firstKraus_energy line 330
  30. def OAI.EntropyPhotonNumber.secondKraus line 360
  31. theorem OAI.EntropyPhotonNumber.secondKraus_apply line 365
  32. theorem OAI.EntropyPhotonNumber.secondKraus_norm line 369
  33. theorem OAI.EntropyPhotonNumber.secondKraus_energy line 376
  34. def OAI.EntropyPhotonNumber.composeKraus line 406
  35. theorem OAI.EntropyPhotonNumber.composeKraus_norm line 409
  36. theorem OAI.EntropyPhotonNumber.composeKraus_energy line 425
  37. theorem OAI.EntropyPhotonNumber.state_ext line 448
  38. theorem OAI.EntropyPhotonNumber.output_unique line 451
  39. theorem OAI.EntropyPhotonNumber.output_eq line 457
  40. theorem OAI.TraceEnsemble.operator_reindex line 468
  41. theorem OAI.TraceEnsemble.kraus_hasSum line 472
  42. theorem OAI.EntropyPhotonNumber.beam_ensemble line 490
  43. theorem OAI.EntropyPhotonNumber.firstKraus_ensemble line 506
  44. theorem OAI.EntropyPhotonNumber.secondKraus_ensemble line 518
  45. theorem OAI.EntropyPhotonNumber.composeKraus_ensemble line 529
  46. def OAI.EnsembleL2.vector line 543
  47. theorem OAI.EnsembleL2.vector_apply line 547
  48. theorem OAI.EnsembleL2.norm_sum line 550
  49. theorem OAI.EnsembleL2.inner_sum line 555
  50. theorem OAI.EnsembleL2.image_summable line 559
  51. theorem OAI.EnsembleL2.projection_bound line 565
  52. theorem OAI.EnsembleL2.projection_sums line 581
  53. theorem OAI.EnsembleL2.fubini_inner line 600
  54. theorem OAI.EnsembleL2.fubini_inner_second line 607
  55. theorem OAI.EnsembleL2.self_inner_hasSum line 616
  56. theorem OAI.TensorLp.conditional_left_overlap line 630
  57. theorem OAI.TensorLp.conditional_right_overlap line 646
  58. theorem OAI.TensorLp.tensorFamily_norm line 662
  59. theorem OAI.TensorLp.tensorFamily_orthogonal line 668
  60. theorem OAI.TensorLp.arithmetic_projection line 681
  61. theorem OAI.KrausBounded.dual_point_square line 716
  62. def OAI.EnsembleL2.mean line 736
  63. def OAI.EnsembleL2.center line 737
  64. theorem OAI.EnsembleL2.mean_hasSum line 740
  65. theorem OAI.EnsembleL2.center_mean line 745
  66. theorem OAI.TensorLp.conditionalLeft_mean line 758
  67. theorem OAI.TensorLp.conditionalRight_mean line 767
  68. theorem OAI.TensorLp.centered_arithmetic_projection line 777
  69. theorem OAI.KrausBounded.dual_id line 801
  70. theorem OAI.KrausBounded.family_hasSum line 818
  71. theorem OAI.KrausBounded.dual_output_mean line 831
  72. theorem OAI.KrausBounded.dual_center line 840
  73. theorem OAI.KrausBounded.dual_variance line 849
  74. theorem OAI.TensorLp.channel_arithmetic_projection line 866
  75. def OAI.KrausBounded.composite line 886
  76. theorem OAI.KrausBounded.composite_norm line 889
  77. theorem OAI.KrausBounded.dual_composite line 895
  78. theorem OAI.KrausBounded.dual_reindex line 906
  79. def OAI.EntropyPhotonNumber.jointKraus line 920
  80. theorem OAI.EntropyPhotonNumber.jointKraus_norm line 924
  81. def OAI.EntropyPhotonNumber.rawJointKraus line 930
  82. theorem OAI.EntropyPhotonNumber.rawJointKraus_norm line 933
  83. def OAI.EntropyPhotonNumber.rawDual line 938
  84. theorem OAI.EntropyPhotonNumber.physical_arithmetic_projection line 942
  85. def OAI.EntropyPhotonNumber.fixedPortEquiv line 957
  86. theorem OAI.EntropyPhotonNumber.rawDual_first_slice line 964
  87. theorem OAI.EntropyPhotonNumber.rawDual_second_slice line 987