OAI/InformationTheory/PhotonNumber/Minimum.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EntropyPhotonNumber.twoPortLambda line 30
  2. def OAI.EntropyPhotonNumber.outputReference line 32
  3. theorem OAI.EntropyPhotonNumber.twoPortLambda_pos line 35
  4. theorem OAI.EntropyPhotonNumber.physical_defect_convolution line 41
  5. theorem OAI.EntropyPhotonNumber.physical_defect_mode_bound line 109
  6. theorem OAI.EntropyPhotonNumber.physical_mean_covariance line 188
  7. theorem OAI.EntropyPhotonNumber.physical_mean_bound line 225
  8. theorem OAI.EntropyPhotonNumber.physical_defect_triangle line 248
  9. theorem OAI.EntropyPhotonNumber.physical_defect_estimate line 285
  10. theorem OAI.BeamLadder.output_lower_square line 328
  11. theorem OAI.EnsembleL2.real_smul_add_square line 355
  12. theorem OAI.EnsembleL2.real_smul_add_hasSum line 364
  13. theorem OAI.TensorLp.tensorFamily_inner line 375
  14. def OAI.EntropyPhotonNumber.WeightedColumns.lowerEnergy line 393
  15. theorem OAI.EntropyPhotonNumber.WeightedColumns.weakMean_hasSum line 396
  16. theorem OAI.EntropyPhotonNumber.WeightedColumns.physical_lowerEnergy line 404
  17. theorem OAI.EnsembleL2.sub_smul_square line 450
  18. theorem OAI.EnsembleL2.centered_square line 456
  19. theorem OAI.EntropyPhotonNumber.SpectralLogData.centeredEnergy_lowerEnergy line 470
  20. theorem OAI.Annihilation.weighted_lowering_norm_sum line 502
  21. theorem OAI.EntropyPhotonNumber.WeightedColumns.lowerEnergy_hasSum line 520
  22. theorem OAI.EntropyPhotonNumber.WeightedColumns.lowerEnergy_affine line 549
  23. theorem OAI.EntropyPhotonNumber.WeightedColumns.thermal_lowerEnergy line 559
  24. theorem OAI.EntropyPhotonNumber.WeightedColumns.beam_weakMean line 585
  25. theorem OAI.EntropyPhotonNumber.WeightedColumns.weakMean_affine line 598
  26. def OAI.EntropyPhotonNumber.WeightedColumns.centeredLowerEnergy line 608
  27. theorem OAI.EntropyPhotonNumber.WeightedColumns.sqrt_complex_square line 611
  28. theorem OAI.EntropyPhotonNumber.WeightedColumns.beam_centeredLowerEnergy line 620
  29. theorem OAI.EntropyPhotonNumber.WeightedColumns.thermal_centeredLowerEnergy line 629
  30. theorem OAI.EntropyPhotonNumber.WeightedColumns.replacement_centeredLowerEnergy line 637
  31. theorem OAI.EntropyPhotonNumber.WeightedColumns.threeport_centered_energy_mode line 653
  32. theorem OAI.EntropyPhotonNumber.SpectralLogData.centeredEnergy_eq_sum line 677
  33. theorem OAI.EntropyPhotonNumber.physical_centered_energy_identity line 687
  34. theorem OAI.EntropyPhotonNumber.second_dual_conditional line 718
  35. theorem OAI.EntropyPhotonNumber.dual_composeKraus line 734
  36. theorem OAI.EntropyPhotonNumber.Regularization.firstFlow_dual_raw line 748
  37. theorem OAI.EntropyPhotonNumber.Regularization.secondFlow_dual_raw line 763
  38. theorem OAI.EntropyPhotonNumber.spectralLogData_of_sandwich line 783
  39. theorem OAI.EntropyPhotonNumber.GibbsData.quarticLogarithm_eq_logSandwich line 852
  40. theorem OAI.WeightedGenerator.drift_radial line 867
  41. theorem OAI.WeightedGenerator.drift_number line 882
  42. def OAI.WeightedGenerator.driftPolynomial line 891
  43. theorem OAI.WeightedGenerator.drift_fourth line 894
  44. theorem OAI.WeightedGenerator.driftPolynomial_expand line 900
  45. theorem OAI.WeightedGenerator.negative_quartic_bounded line 907
  46. theorem OAI.WeightedGenerator.driftPolynomial_bounded line 963
  47. theorem OAI.EntropyPhotonNumber.number_le_weight line 976
  48. theorem OAI.EntropyPhotonNumber.number_weight_eq line 979
  49. theorem OAI.EntropyPhotonNumber.number_div_weight_bound line 982
  50. def OAI.EntropyPhotonNumber.numberSandwich line 987
  51. theorem OAI.EntropyPhotonNumber.numberSandwich_positive line 990
  52. theorem OAI.EntropyPhotonNumber.numberSandwich_form line 999
  53. theorem OAI.EntropyPhotonNumber.numberSandwich_unique line 1013
  54. theorem OAI.EntropyPhotonNumber.drift_number_div_bound line 1024
  55. theorem OAI.EntropyPhotonNumber.thermalGenerator_number line 1038
  56. theorem OAI.EntropyPhotonNumber.polynomial_weight_six_bound line 1051
  57. def OAI.EntropyPhotonNumber.fourthDriftConstant line 1073
  58. theorem OAI.EntropyPhotonNumber.drift_fourth_div_bound line 1076
  59. theorem OAI.EntropyPhotonNumber.fourth_diagonal_eq_one line 1082
  60. theorem OAI.EntropyPhotonNumber.thermalGenerator_fourth line 1090
  61. theorem OAI.EntropyPhotonNumber.thermalGenerator_fourth_bound line 1098
  62. theorem OAI.EntropyPhotonNumber.Regularization.attenuation_mem line 1118
  63. theorem OAI.EntropyPhotonNumber.Regularization.thermal_state_diagonal line 1121
  64. theorem OAI.EntropyPhotonNumber.Regularization.minimum_spectral_pairing_balance line 1131
  65. structure OAI.EntropyPhotonNumber.ThermalSetup line 1207
  66. def OAI.EntropyPhotonNumber.ThermalSetup.r0 line 1228
  67. def OAI.EntropyPhotonNumber.ThermalSetup.w1 line 1229
  68. def OAI.EntropyPhotonNumber.ThermalSetup.w2 line 1230
  69. theorem OAI.EntropyPhotonNumber.ThermalSetup.r0_pos line 1231
  70. theorem OAI.EntropyPhotonNumber.ThermalSetup.w1_pos line 1235
  71. theorem OAI.EntropyPhotonNumber.ThermalSetup.w2_pos line 1236
  72. theorem OAI.EntropyPhotonNumber.ThermalSetup.η_mem line 1237
  73. theorem OAI.EntropyPhotonNumber.ThermalSetup.θ_mem line 1238
  74. theorem OAI.EntropyPhotonNumber.ThermalSetup.κ_mem line 1239
  75. theorem OAI.EntropyPhotonNumber.ThermalSetup.δ_mem line 1240
  76. def OAI.EntropyPhotonNumber.ThermalSetup.reg line 1242
  77. def OAI.EntropyPhotonNumber.ThermalSetup.middle line 1266
  78. def OAI.EntropyPhotonNumber.ThermalSetup.raw line 1267
  79. theorem OAI.EntropyPhotonNumber.ThermalSetup.raw_finiteMoment line 1269
  80. theorem OAI.EntropyPhotonNumber.ThermalSetup.output_op line 1272
  81. theorem OAI.EntropyPhotonNumber.WeightedColumns.sum_lowerEnergy line 1280
  82. theorem OAI.EntropyPhotonNumber.SpectralLogData.centeredEnergy_eq_energy line 1288
  83. def OAI.EntropyPhotonNumber.SpectralLogData.defectSquared line 1297
  84. def OAI.EntropyPhotonNumber.SpectralLogData.meanSquared line 1298
  85. theorem OAI.EntropyPhotonNumber.SpectralLogData.defectSquared_nonneg line 1299
  86. theorem OAI.EntropyPhotonNumber.SpectralLogData.meanSquared_nonneg line 1300
  87. theorem OAI.EntropyPhotonNumber.GibbsData.spectral_defect line 1304
  88. theorem OAI.EntropyPhotonNumber.GibbsData.spectral_mean line 1306
  89. theorem OAI.EntropyPhotonNumber.ThermalSetup.physical_estimate line 1312
  90. theorem OAI.EntropyPhotonNumber.ThermalSetup.physical_energy line 1373
  91. theorem OAI.EntropyPhotonNumber.ThermalDual.decay_from_cancellation line 1393
  92. theorem OAI.EntropyPhotonNumber.ThermalSetup.minimum_decay line 1406
  93. theorem OAI.EntropyPhotonNumber.ThermalSetup.uniform_minimum_decay line 1477