OAI/InformationTheory/PhotonNumber/ThermalMetric.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThermalMetric.h line 18
  2. theorem OAI.ThermalMetric.h_pos line 20
  3. def OAI.ThermalMetric.frequency line 23
  4. def OAI.ThermalMetric.weight line 25
  5. theorem OAI.ThermalMetric.logMean_reference line 27
  6. theorem OAI.ThermalMetric.weight_pos line 33
  7. theorem OAI.ThermalMetric.tilted_logMean line 36
  8. theorem OAI.ThermalMetric.weight_frequency_bounds line 43
  9. theorem OAI.ThermalMetric.logMean_mul_log_sub line 59
  10. def OAI.ThermalMetric.defectCoefficient line 69
  11. def OAI.ThermalMetric.metricCoefficient line 71
  12. theorem OAI.ThermalMetric.metricCoefficient_pos line 74
  13. theorem OAI.ThermalMetric.defect_multiplier line 78
  14. theorem OAI.ThermalMetric.defect_dual_square line 89
  15. def OAI.ThermalMetric.weightedVector line 101
  16. theorem OAI.ThermalMetric.weightedVector_apply line 111
  17. theorem OAI.ThermalMetric.weightedVector_norm_sq line 115
  18. theorem OAI.ThermalMetric.defectVector_entry_norm line 122
  19. def OAI.ThermalMetric.defectVector line 128
  20. theorem OAI.ThermalMetric.defectVector_apply line 139
  21. theorem OAI.ThermalMetric.defectVector_norm_sq line 144
  22. theorem OAI.ThermalMetric.defectVector_pairing line 152
  23. def OAI.ThermalMetric.defectFunctional line 175
  24. theorem OAI.ThermalMetric.defectFunctional_norm_sq line 182
  25. theorem OAI.ThermalMetric.defectFunctional_restrict_norm line 188
  26. theorem OAI.ThermalMetric.metricCoefficient_self line 204
  27. theorem OAI.ThermalMetric.hasSum_diagonal line 210
  28. theorem OAI.ThermalMetric.summable_diagonal line 221
  29. def OAI.ThermalMetric.identityEntry line 231
  30. theorem OAI.ThermalMetric.identityEntry_summable line 235
  31. def OAI.ThermalMetric.identityVector line 247
  32. def OAI.ThermalMetric.centeredSpace line 252
  33. theorem OAI.ThermalMetric.defectVector_mem_centeredSpace line 256
  34. theorem OAI.ThermalMetric.centered_defect_norm_sq line 282
  35. theorem OAI.ThermalMetric.defect_series_summable line 290
  36. theorem OAI.ThermalMetric.coefficient_series_summable line 306
  37. theorem OAI.ThermalMetric.production_series_subtraction line 315
  38. theorem OAI.ThermalMetric.diagonal_mean_summable line 330
  39. def OAI.ThermalMetric.diagonalMean line 341
  40. theorem OAI.ThermalMetric.diagonal_centering line 343
  41. def OAI.WeightedGenerator.centeredEntry line 356
  42. theorem OAI.WeightedGenerator.nonlog_summable line 361
  43. theorem OAI.WeightedGenerator.centered_weight_summable line 368
  44. theorem OAI.WeightedGenerator.entropy_weight_summable line 396
  45. theorem OAI.WeightedGenerator.centered_six_sums line 427
  46. theorem OAI.Annihilation.centered_canonical_norm line 473
  47. def OAI.Annihilation.centeredLadder line 492
  48. theorem OAI.Annihilation.centeredLadder_summable line 495
  49. theorem OAI.Annihilation.centeredLadder_ccr line 500
  50. theorem OAI.Annihilation.centeredLadder_ensemble_gap line 509
  51. theorem OAI.WeightedGenerator.centered_lowering_coordinate line 528
  52. theorem OAI.WeightedGenerator.centered_raising_coordinate line 545
  53. theorem OAI.WeightedGenerator.centered_down_sq line 566
  54. theorem OAI.WeightedGenerator.centered_up_sq line 575
  55. theorem OAI.WeightedGenerator.centered_down_sum line 584
  56. theorem OAI.WeightedGenerator.centered_up_sum line 600
  57. theorem OAI.WeightedGenerator.centered_K_sum line 612
  58. def OAI.EntropyPhotonNumber.GibbsData.annihilationMatrix line 639
  59. def OAI.EntropyPhotonNumber.GibbsData.annihilationMean line 642
  60. def OAI.EntropyPhotonNumber.GibbsData.centeredMatrix line 644
  61. theorem OAI.EntropyPhotonNumber.GibbsData.annihilation_mean_summable line 647
  62. theorem OAI.EntropyPhotonNumber.GibbsData.centeredMatrix_mean_zero line 655
  63. theorem OAI.EntropyPhotonNumber.GibbsData.centeredMatrix_six_sums line 662
  64. theorem OAI.EntropyPhotonNumber.GibbsData.centeredMatrix_defect_summable line 675
  65. def OAI.EntropyPhotonNumber.GibbsData.defect line 683
  66. theorem OAI.EntropyPhotonNumber.GibbsData.defect_norm_sq line 689
  67. def OAI.EntropyPhotonNumber.GibbsData.centeredEnergy line 696
  68. theorem OAI.EntropyPhotonNumber.GibbsData.thermalGenerator_centered_logarithmic_trace line 699
  69. theorem OAI.EntropyPhotonNumber.GibbsData.entropy_production line 714
  70. theorem OAI.CrossEnsemble.pairing_rows line 741
  71. theorem OAI.CrossEnsemble.pairing_columns line 754
  72. def OAI.WeightedGenerator.weakDefect line 769
  73. theorem OAI.WeightedGenerator.weakDefect_spectral line 776
  74. theorem OAI.ThermalMetric.bounded_matrix_summable line 820
  75. def OAI.ThermalMetric.matrixVector line 852
  76. theorem OAI.ThermalMetric.weightedVector_centered line 859
  77. def OAI.EntropyPhotonNumber.GibbsData.observableVector line 892
  78. theorem OAI.EntropyPhotonNumber.GibbsData.observableVector_mem line 899
  79. theorem OAI.EntropyPhotonNumber.GibbsData.defect_on_observable line 906
  80. theorem OAI.Annihilation.lowering_weighted_apply line 926
  81. theorem OAI.Annihilation.raising_weighted_apply line 933
  82. def OAI.EntropyPhotonNumber.numberMatrixUnit line 950
  83. theorem OAI.EntropyPhotonNumber.numberKet_inner line 953
  84. theorem OAI.EntropyPhotonNumber.inner_numberKet line 957
  85. theorem OAI.EntropyPhotonNumber.numberMatrixUnit_inner line 961
  86. theorem OAI.WeightedGenerator.inverseColumns_entry line 972
  87. theorem OAI.WeightedGenerator.weakDefect_numberMatrixUnit line 981
  88. theorem OAI.EntropyPhotonNumber.GibbsData.inverse_spectralColumns_operator line 1025
  89. theorem OAI.EntropyPhotonNumber.GibbsData.weakDefect_numberMatrixUnit line 1032