OAI/InformationTheory/PhotonNumber/Gibbs.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TraceEnsemble.positiveRoot line 18
  2. def OAI.TraceEnsemble.operator line 20
  3. theorem OAI.TraceEnsemble.summable_rankOne line 23
  4. theorem OAI.TraceEnsemble.hasSum_rankOne line 28
  5. theorem OAI.TraceEnsemble.positive line 32
  6. theorem OAI.TraceEnsemble.hasSum_entry line 38
  7. theorem OAI.TraceEnsemble.hasSum_quadratic line 45
  8. theorem OAI.TraceEnsemble.basis_hasSum_norm_sq line 53
  9. theorem OAI.TraceEnsemble.trace line 63
  10. theorem OAI.TraceEnsemble.operator_ext line 82
  11. theorem OAI.TraceEnsemble.summable_entry_norm line 98
  12. theorem OAI.TraceEnsemble.sqrt_quadratic line 108
  13. theorem OAI.TraceEnsemble.sqrt_ensemble line 119
  14. theorem OAI.TraceEnsemble.summable_expectation_norm line 142
  15. def OAI.EntropyPhotonNumber.channelNumberBasis line 155
  16. theorem OAI.EntropyPhotonNumber.channelNumberBasis_apply line 158
  17. def OAI.EntropyPhotonNumber.rootColumn line 162
  18. theorem OAI.EntropyPhotonNumber.rootColumn_norm line 165
  19. theorem OAI.EntropyPhotonNumber.rootColumn_operator line 171
  20. def OAI.EntropyPhotonNumber.numberMoment line 180
  21. def OAI.EntropyPhotonNumber.FiniteMoment line 183
  22. theorem OAI.WeightedShift.weighted_entries_summable line 192
  23. def OAI.WeightedShift.weightedFamily line 210
  24. theorem OAI.WeightedShift.weightedFamily_apply line 219
  25. theorem OAI.WeightedShift.weightedFamily_summable line 224
  26. theorem OAI.EntropyPhotonNumber.root_weighted_entries line 238
  27. def OAI.EntropyPhotonNumber.weightedRoot line 246
  28. theorem OAI.EntropyPhotonNumber.weightedRoot_apply line 250
  29. theorem OAI.EntropyPhotonNumber.weightedRoot_summable line 253
  30. theorem OAI.EntropyPhotonNumber.inverse_weightedRoot line 257
  31. theorem OAI.Annihilation.inner_inverse_pair line 272
  32. theorem OAI.Annihilation.gain_trace line 277
  33. theorem OAI.Annihilation.mode_trace_left line 286
  34. theorem OAI.Annihilation.mode_trace_right line 294
  35. theorem OAI.WeightedGenerator.pairing_inverse_zero line 310
  36. theorem OAI.WeightedGenerator.trace_zero line 317
  37. theorem OAI.CrossEnsemble.pairing_trace_sandwich line 327
  38. theorem OAI.WeightedGenerator.pairing_sandwich_hasSum line 346
  39. def OAI.EntropyPhotonNumber.thermalGenerator line 370
  40. theorem OAI.EntropyPhotonNumber.thermalGenerator_pairing line 373
  41. theorem OAI.EntropyPhotonNumber.thermalGenerator_traceless line 383
  42. theorem OAI.CrossEnsemble.sandwich_injective line 397
  43. theorem OAI.CrossEnsemble.pairing_transform line 410
  44. theorem OAI.CrossEnsemble.pairing_transform_eq line 418
  45. def OAI.CrossEnsemble.eigenEnsemble line 427
  46. theorem OAI.CrossEnsemble.eigenEnsemble_norm line 431
  47. theorem OAI.CrossEnsemble.eigenEnsemble_operator line 436
  48. theorem OAI.WeightedGenerator.pairing_eq_of_operator_eq line 461
  49. theorem OAI.EntropyPhotonNumber.weightedRoot_operator_eq line 476
  50. theorem OAI.Annihilation.log_mode_left line 497
  51. theorem OAI.Annihilation.log_mode_right line 515
  52. def OAI.WeightedGenerator.spectralGain line 532
  53. theorem OAI.WeightedGenerator.crossed_log_summable line 536
  54. theorem OAI.WeightedGenerator.uncrossed_log_summable line 555
  55. theorem OAI.WeightedGenerator.tsum_prod_columns line 574
  56. theorem OAI.WeightedGenerator.dissipator_log_sum line 580
  57. structure OAI.EntropyPhotonNumber.GibbsData line 642
  58. theorem OAI.EntropyPhotonNumber.inversePower_root_four line 659
  59. theorem OAI.EntropyPhotonNumber.finiteMoment_mono line 665
  60. def OAI.EntropyPhotonNumber.GibbsData.logSandwich line 675
  61. def OAI.EntropyPhotonNumber.GibbsData.probability line 679
  62. def OAI.EntropyPhotonNumber.GibbsData.logCoefficient line 681
  63. theorem OAI.EntropyPhotonNumber.GibbsData.probability_pos line 683
  64. theorem OAI.EntropyPhotonNumber.GibbsData.probability_sum line 687
  65. theorem OAI.EntropyPhotonNumber.GibbsData.logCoefficient_nonneg line 691
  66. theorem OAI.EntropyPhotonNumber.GibbsData.eigen line 697
  67. theorem OAI.EntropyPhotonNumber.GibbsData.logSandwich_symmetric line 702
  68. theorem OAI.EntropyPhotonNumber.GibbsData.logSandwich_parseval line 712
  69. theorem OAI.EntropyPhotonNumber.GibbsData.logSandwich_preimage line 725
  70. theorem OAI.EntropyPhotonNumber.GibbsData.weighted_columns line 751
  71. def OAI.WeightedGenerator.loweringEntry line 780
  72. theorem OAI.WeightedGenerator.spectralGain_adjoint line 784
  73. theorem OAI.WeightedGenerator.spectralGain_lowering line 799
  74. theorem OAI.WeightedGenerator.spectralGain_raising line 806
  75. theorem OAI.WeightedGenerator.spectralGain_lowering_sq line 817
  76. theorem OAI.WeightedGenerator.spectralGain_raising_sq line 823
  77. theorem OAI.WeightedGenerator.log_difference_summable line 832
  78. theorem OAI.WeightedGenerator.thermal_log_spectral line 844
  79. def OAI.EntropyPhotonNumber.GibbsData.spectralColumns line 885
  80. theorem OAI.EntropyPhotonNumber.GibbsData.spectralColumns_summable line 887
  81. theorem OAI.EntropyPhotonNumber.GibbsData.spectralColumns_inverse line 890
  82. theorem OAI.EntropyPhotonNumber.GibbsData.spectralColumns_normalized line 894
  83. theorem OAI.EntropyPhotonNumber.GibbsData.spectralColumns_operator line 900
  84. theorem OAI.EntropyPhotonNumber.GibbsData.thermalGenerator_logarithmic_trace line 907