OAI/InformationTheory/PhotonNumber/Entropy.lean

GitHub source file

157 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Annihilation.diagonal line 18
  2. theorem OAI.Annihilation.diagonal_apply line 23
  3. theorem OAI.Annihilation.diagonal_quadratic line 27
  4. theorem OAI.Annihilation.gain_lower_sq line 37
  5. theorem OAI.Annihilation.gain_raise_sq line 44
  6. theorem OAI.Annihilation.gain_raise_zero line 51
  7. theorem OAI.Annihilation.gain_lower_diagonal line 54
  8. theorem OAI.Annihilation.gain_raise_diagonal line 74
  9. theorem OAI.Annihilation.diagonal_mode_left line 91
  10. theorem OAI.Annihilation.diagonal_selfAdjoint line 110
  11. theorem OAI.Annihilation.diagonal_mode_right line 120
  12. def OAI.WeightedGenerator.columnPairing line 138
  13. theorem OAI.WeightedGenerator.columnPairing_hasSum line 146
  14. def OAI.WeightedGenerator.drift line 167
  15. theorem OAI.WeightedGenerator.mode_pairing_hasSum line 170
  16. def OAI.WeightedGenerator.componentPairing line 183
  17. theorem OAI.WeightedGenerator.component_pairing_hasSum line 191
  18. theorem OAI.WeightedGenerator.drift_column line 204
  19. theorem OAI.WeightedShift.family_coordinates_summable line 217
  20. theorem OAI.EntropyPhotonNumber.weightedRoot_row line 228
  21. theorem OAI.EntropyPhotonNumber.thermalGenerator_drift line 240
  22. def OAI.QuantumTrace.numberBox line 284
  23. theorem OAI.QuantumTrace.numberBox_compl_weight line 287
  24. theorem OAI.QuantumTrace.number_tail_mass_le line 297
  25. theorem OAI.QuantumTrace.entropy_tail_le_modulus line 313
  26. theorem OAI.QuantumTrace.entropy_uniform_tail line 355
  27. theorem OAI.QuantumTrace.tendsto_tsum_of_uniform_tail line 381
  28. theorem OAI.QuantumTrace.diagonal_le_one line 419
  29. theorem OAI.QuantumTrace.entropyOperator_tendsto line 424
  30. theorem OAI.QuantumTrace.entropy_tendsto_finite_energy line 447
  31. def OAI.QuantumTrace.basisProjection line 502
  32. theorem OAI.QuantumTrace.basisProjection_apply_basis line 506
  33. theorem OAI.QuantumTrace.basisProjection_adjoint line 510
  34. theorem OAI.QuantumTrace.basisProjection_idempotent line 515
  35. theorem OAI.QuantumTrace.basisProjection_norm_le line 523
  36. theorem OAI.QuantumTrace.basisApprox_eq_comp line 529
  37. theorem OAI.QuantumTrace.double_compression_norm_le line 537
  38. theorem OAI.QuantumTrace.tsum_bound_of_tendsto line 585
  39. def OAI.QuantumTrace.energySet line 600
  40. theorem OAI.QuantumTrace.energySet_limit line 606
  41. def OAI.QuantumTrace.matrixEmbed line 664
  42. theorem OAI.QuantumTrace.matrixEmbed_continuous line 668
  43. theorem OAI.QuantumTrace.matrixEmbed_entries line 674
  44. theorem OAI.QuantumTrace.entry_norm_le_one line 704
  45. theorem OAI.QuantumTrace.double_compressions_compact line 714
  46. theorem OAI.QuantumTrace.energySet_isClosed line 728
  47. theorem OAI.QuantumTrace.energySet_totallyBounded line 740
  48. theorem OAI.QuantumTrace.energySet_isCompact line 788
  49. def OAI.QuantumTrace.momentSet line 797
  50. theorem OAI.QuantumTrace.momentSet_limit line 803
  51. theorem OAI.QuantumTrace.momentSet_isCompact line 819
  52. theorem OAI.QuantumTrace.lowerSemicontinuous_tsum_nonneg line 828
  53. theorem OAI.QuantumTrace.moment_lowerSemicontinuous line 840
  54. theorem OAI.QuantumTrace.energy_lowerSemicontinuous line 852
  55. theorem OAI.QuantumTrace.entropy_continuous_energySet line 863
  56. def OAI.EntropyPhotonNumber.energy line 889
  57. theorem OAI.EntropyPhotonNumber.energy_nonneg line 892
  58. theorem OAI.EntropyPhotonNumber.entropy_eq_quantumTrace line 896
  59. theorem OAI.EntropyPhotonNumber.entropy_summable line 902
  60. theorem OAI.EntropyPhotonNumber.entropy_nonneg line 909
  61. theorem OAI.EntropyPhotonNumber.entropy_energy_bound line 913
  62. theorem OAI.TraceEnsemble.norm_tail_le line 940
  63. theorem OAI.TraceEnsemble.tendsto_tsum_fixed_norm line 953
  64. theorem OAI.TraceEnsemble.tendsto_operator line 987
  65. theorem OAI.TraceEnsemble.tendsto_positiveRoot line 1002
  66. def OAI.TensorLp.tensorBilinear line 1015
  67. theorem OAI.TensorLp.tensorBilinear_apply line 1038
  68. theorem OAI.TensorLp.tendsto_tensor line 1040
  69. theorem OAI.EntropyPhotonNumber.tendsto_rootColumn line 1052
  70. theorem OAI.EntropyPhotonNumber.tendsto_beamOutput line 1059
  71. theorem OAI.EntropyPhotonNumber.diagonalState_entropy line 1076
  72. theorem OAI.EntropyPhotonNumber.mixture_entry line 1085
  73. theorem OAI.EntropyPhotonNumber.mixture_finiteEnergy line 1091
  74. theorem OAI.EntropyPhotonNumber.mixture_energy line 1100
  75. theorem OAI.QuantumTrace.summable_finite_product line 1119
  76. theorem OAI.QuantumTrace.one_add_sum_le_product line 1129
  77. theorem OAI.QuantumTrace.summable_shift_pow_geometric line 1140
  78. theorem OAI.QuantumTrace.thermalWeight_moment_summable line 1151
  79. theorem OAI.EntropyPhotonNumber.numberMoment_nonneg line 1174
  80. theorem OAI.EntropyPhotonNumber.thermalState_finiteMoment line 1177
  81. theorem OAI.EntropyPhotonNumber.finiteMoment_finiteEnergy line 1182
  82. theorem OAI.EntropyPhotonNumber.thermalState_finiteEnergy line 1192
  83. theorem OAI.EntropyPhotonNumber.mixture_finiteMoment line 1196
  84. theorem OAI.EntropyPhotonNumber.energyMoment_ofReal line 1209
  85. theorem OAI.EntropyPhotonNumber.beamOutput_energy_bound line 1215
  86. def OAI.EntropyPhotonNumber.regularizedOutput line 1224
  87. theorem OAI.EntropyPhotonNumber.regularizedOutput_finiteEnergy line 1230
  88. theorem OAI.EntropyPhotonNumber.regularizedOutput_energy_bound line 1236
  89. theorem OAI.EntropyPhotonNumber.tendsto_regularizedOutput line 1254
  90. theorem OAI.EntropyPhotonNumber.tendsto_entropy line 1264
  91. theorem OAI.EntropyPhotonNumber.entropy_linear_bound line 1277
  92. instance OAI.EntropyPhotonNumber.stateTopology line 1298
  93. theorem OAI.EntropyPhotonNumber.continuous_state_op line 1301
  94. theorem OAI.EntropyPhotonNumber.State.ext_op line 1304
  95. def OAI.EntropyPhotonNumber.boundedStates line 1310
  96. def OAI.EntropyPhotonNumber.stateOfMomentSet line 1313
  97. theorem OAI.EntropyPhotonNumber.stateOfMomentSet_mem line 1319
  98. theorem OAI.EntropyPhotonNumber.op_mem_momentSet line 1330
  99. theorem OAI.EntropyPhotonNumber.boundedStates_isCompact line 1338
  100. theorem OAI.EntropyPhotonNumber.continuous_entropy_boundedStates line 1354
  101. theorem OAI.EntropyPhotonNumber.penalty_lowerSemicontinuous line 1362
  102. structure OAI.EntropyPhotonNumber.Regularization line 1384
  103. def OAI.EntropyPhotonNumber.Regularization.output line 1411
  104. def OAI.EntropyPhotonNumber.Regularization.objective line 1414
  105. def OAI.EntropyPhotonNumber.Regularization.entropyConstant line 1418
  106. theorem OAI.EntropyPhotonNumber.Regularization.coercive line 1421
  107. theorem OAI.EntropyPhotonNumber.Regularization.continuous_output_entropy line 1430
  108. theorem OAI.EntropyPhotonNumber.Regularization.objective_lowerSemicontinuous line 1448
  109. theorem OAI.EntropyPhotonNumber.Regularization.sublevel_bounds line 1460
  110. theorem OAI.EntropyPhotonNumber.Regularization.sublevel_mem_bounded line 1479
  111. theorem OAI.EntropyPhotonNumber.Regularization.exists_constrained_minimum line 1493
  112. theorem OAI.EntropyPhotonNumber.Regularization.exists_minimum line 1504
  113. def OAI.QuantumTrace.basisMoment line 1530
  114. def OAI.QuantumTrace.basisExpectation line 1533
  115. theorem OAI.QuantumTrace.basisMoment_one line 1536
  116. theorem OAI.QuantumTrace.basisMoment_ofReal line 1542
  117. theorem OAI.QuantumTrace.basisExpectation_ensemble line 1551
  118. theorem OAI.QuantumTrace.basisExpectation_le_of_form_le line 1561
  119. def OAI.EntropyPhotonNumber.numberVectorMoment line 1585
  120. theorem OAI.EntropyPhotonNumber.numberVectorMoment_eq line 1588
  121. theorem OAI.EntropyPhotonNumber.finiteVectorEnergy_iff line 1593
  122. theorem OAI.EntropyPhotonNumber.numberVectorMoment_ofReal line 1603
  123. theorem OAI.EntropyPhotonNumber.thermal_log_constants line 1609
  124. theorem OAI.EntropyPhotonNumber.negativeLog_extended_le_thermal line 1619
  125. theorem OAI.EntropyPhotonNumber.negativeLog_expectation_le_thermal line 1639
  126. def OAI.QuantumTrace.sliceMoment line 1656
  127. theorem OAI.QuantumTrace.sliceMoment_bound line 1660
  128. def OAI.QuantumTrace.sliceCoordinates line 1678
  129. theorem OAI.QuantumTrace.sliceCoordinates_square line 1684
  130. theorem OAI.QuantumTrace.sliceCoordinates_sum line 1691
  131. theorem OAI.QuantumTrace.sliceMoment_bounded_representation line 1698
  132. theorem OAI.EntropyPhotonNumber.numberVectorMoment_eq_tensor line 1727
  133. theorem OAI.EntropyPhotonNumber.numberWeight_eq line 1732
  134. def OAI.EntropyPhotonNumber.energyInverse line 1736
  135. theorem OAI.EntropyPhotonNumber.energyInverse_quadratic line 1739
  136. theorem OAI.EntropyPhotonNumber.energyInverse_norm line 1747
  137. theorem OAI.EntropyPhotonNumber.energyInverse_finiteEnergy line 1753
  138. theorem OAI.EntropyPhotonNumber.energyInverse_energy line 1766
  139. theorem OAI.EntropyPhotonNumber.logarithmic_slice_representation line 1779
  140. theorem OAI.EntropyPhotonNumber.number_form_representation line 1825
  141. theorem OAI.EntropyPhotonNumber.combined_form_representation line 1843
  142. theorem OAI.EntropyPhotonNumber.gibbsFactor_quadratic line 1865
  143. theorem OAI.EntropyPhotonNumber.energyInverse_mul_three line 1877
  144. theorem OAI.EntropyPhotonNumber.gibbsFactor_slice_form line 1883
  145. theorem OAI.QuantumTrace.gibbs_form_energy_identity line 1907
  146. theorem OAI.QuantumTrace.sliceMoment_ensemble line 1978
  147. theorem OAI.QuantumTrace.basisMoment_smul line 1988
  148. theorem OAI.QuantumTrace.sliceMoment_smul line 1998
  149. theorem OAI.EntropyPhotonNumber.firstKraus_slice_expectation line 2008
  150. theorem OAI.EntropyPhotonNumber.secondKraus_slice_expectation line 2017
  151. theorem OAI.EntropyPhotonNumber.composedKraus_first_ensemble line 2026
  152. theorem OAI.EntropyPhotonNumber.composed_slice_expectation line 2039
  153. theorem OAI.QuantumTrace.basisExpectation_ofReal line 2057
  154. theorem OAI.QuantumTrace.basisExpectation_finite_iff line 2066
  155. theorem OAI.TraceEnsemble.diagonalVector_operator line 2086
  156. theorem OAI.EntropyPhotonNumber.sequenceBasis_numberKet line 2103
  157. theorem OAI.EntropyPhotonNumber.gibbs_slice_trace line 2111