OAI/InformationTheory/PhotonNumber/FiniteVariation.lean

GitHub source file

188 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteBlock.embedLinear line 27
  2. theorem OAI.FiniteBlock.embedLinear_basis line 30
  3. theorem OAI.FiniteBlock.embedLinear_orthonormal line 34
  4. def OAI.FiniteBlock.embed line 42
  5. theorem OAI.FiniteBlock.embed_basis line 46
  6. theorem OAI.FiniteBlock.embed_apply line 49
  7. def OAI.FiniteBlock.vectors line 57
  8. theorem OAI.FiniteBlock.vectors_orthonormal line 59
  9. def OAI.FiniteBlock.basis line 83
  10. theorem OAI.FiniteBlock.basis_inl line 97
  11. theorem OAI.FiniteBlock.basis_inr line 99
  12. def OAI.FiniteBlock.block line 104
  13. theorem OAI.FiniteBlock.inner_basis_embed line 108
  14. theorem OAI.FiniteBlock.block_embed line 114
  15. theorem OAI.FiniteBlock.block_tail line 123
  16. theorem OAI.FiniteBlock.block_eigen line 129
  17. theorem OAI.FiniteBlock.exp_spectral line 143
  18. theorem OAI.FiniteBlock.exp_eigenvector line 161
  19. theorem OAI.FiniteBlock.trace_exp line 170
  20. def OAI.FiniteBlock.partition line 176
  21. def OAI.FiniteBlock.weights line 179
  22. theorem OAI.FiniteBlock.partition_pos line 183
  23. theorem OAI.FiniteBlock.weights_pos line 203
  24. theorem OAI.FiniteBlock.weights_hasSum line 210
  25. theorem OAI.QuantumTrace.basisMoment_smul_coeff line 231
  26. theorem OAI.QuantumTrace.basisMoment_add_le line 240
  27. def OAI.QuantumTrace.momentDomain line 260
  28. theorem OAI.QuantumTrace.mem_momentDomain line 273
  29. theorem OAI.QuantumTrace.basisExpectation_diagonal line 278
  30. theorem OAI.QuantumTrace.eigenvector_moment_finite line 289
  31. theorem OAI.TraceEnsemble.summable_basis_square line 307
  32. theorem OAI.TraceEnsemble.summable_map_square line 315
  33. theorem OAI.TraceEnsemble.summable_trace_pair line 322
  34. def OAI.TraceEnsemble.expectation line 333
  35. theorem OAI.TraceEnsemble.hasSum_expectation line 337
  36. theorem OAI.TraceEnsemble.hasSum_expectation_basis line 341
  37. theorem OAI.TraceEnsemble.expectation_eq_of_operator_eq line 360
  38. def OAI.EntropyPhotonNumber.expectation line 375
  39. theorem OAI.EntropyPhotonNumber.expectation_ensemble line 378
  40. theorem OAI.EntropyPhotonNumber.hasSum_expectation_basis line 384
  41. theorem OAI.EntropyPhotonNumber.expectation_add line 390
  42. theorem OAI.EntropyPhotonNumber.expectation_smul line 396
  43. def OAI.EntropyPhotonNumber.spectralState line 406
  44. theorem OAI.EntropyPhotonNumber.spectralState_eigen line 415
  45. def OAI.EntropyPhotonNumber.blockState line 420
  46. theorem OAI.FiniteBlock.basis_domain line 436
  47. theorem OAI.FiniteBlock.tilted_moment_finite line 451
  48. theorem OAI.FiniteBlock.block_adjoint line 495
  49. theorem OAI.FiniteBlock.block_symmetric line 503
  50. theorem OAI.FiniteBlock.block_add line 510
  51. theorem OAI.FiniteBlock.block_smul line 515
  52. theorem OAI.EntropyPhotonNumber.expectation_block_eigen line 525
  53. theorem OAI.EntropyPhotonNumber.expectation_block_diagonal line 550
  54. theorem OAI.FiniteBlock.inner_block line 599
  55. theorem OAI.FiniteBlock.inner_tail_block line 605
  56. theorem OAI.FiniteBlock.block_sub line 610
  57. theorem OAI.FiniteBlock.block_exp_eigen line 614
  58. theorem OAI.FiniteBlock.reference_on_block line 624
  59. theorem OAI.EntropyPhotonNumber.expectation_block_matrix line 640
  60. theorem OAI.EntropyPhotonNumber.blockState_operator line 658
  61. theorem OAI.EntropyPhotonNumber.block_crossEntropy line 694
  62. theorem OAI.EntropyPhotonNumber.block_relativeEntropy_lower line 745
  63. theorem OAI.EntropyPhotonNumber.blockState_finiteMoment line 767
  64. theorem OAI.EntropyPhotonNumber.crossEntropy_self_summable line 782
  65. theorem OAI.EntropyPhotonNumber.blockState_crossEntropy_finite line 794
  66. theorem OAI.EntropyPhotonNumber.blockState_relativeEntropy line 811
  67. theorem OAI.EntropyPhotonNumber.blockState_block_entry line 831
  68. theorem OAI.EntropyPhotonNumber.blockState_block_expectation line 845
  69. theorem OAI.QuantumCalculus.exp_sub_eq_integral line 884
  70. theorem OAI.QuantumCalculus.exp_add_smul_sub line 903
  71. theorem OAI.QuantumCalculus.continuous_duhamel line 911
  72. theorem OAI.QuantumCalculus.hasDerivAt_exp_add_smul_zero line 921
  73. theorem OAI.QuantumCalculus.hasDerivAt_exp_add_smul line 934
  74. theorem OAI.QuantumCalculus.trace_duhamel line 950
  75. theorem OAI.QuantumCalculus.hasDerivAt_trace_exp line 962
  76. theorem OAI.QuantumCalculus.hasDerivAt_trace_exp_mul line 968
  77. def OAI.QuantumCalculus.matrixReTrace line 983
  78. theorem OAI.QuantumCalculus.matrixReTrace_apply line 987
  79. theorem OAI.QuantumCalculus.matrixReTrace_cyclic line 991
  80. theorem OAI.QuantumCalculus.exp_real_diagonal line 995
  81. theorem OAI.QuantumCalculus.matrix_duhamel_integrand line 1003
  82. theorem OAI.QuantumCalculus.matrix_duhamel_hessian line 1032
  83. theorem OAI.QuantumCalculus.quadratic_expansion line 1071
  84. theorem OAI.QuantumCalculus.log_partition_expansion line 1099
  85. theorem OAI.QuantumCalculus.finite_block_partition_expansion line 1132
  86. theorem OAI.QuantumCalculus.relative_partition_expansion line 1162
  87. theorem OAI.QuantumCalculus.finite_block_relative_expansion line 1198
  88. def OAI.FiniteBlock.tiltMatrix line 1228
  89. theorem OAI.FiniteBlock.tiltMatrix_hermitian line 1232
  90. theorem OAI.FiniteBlock.partition_trace line 1238
  91. theorem OAI.FiniteBlock.tail_normalization line 1244
  92. def OAI.EntropyPhotonNumber.blockTilt line 1257
  93. theorem OAI.EntropyPhotonNumber.blockTilt_relativeEntropy line 1261
  94. theorem OAI.EntropyPhotonNumber.blockTilt_relativeEntropy_expansion line 1285
  95. theorem OAI.EntropyPhotonNumber.blockTilt_finiteMoment line 1298
  96. theorem OAI.EntropyPhotonNumber.blockTilt_relativeEntropy_expansion_of_moment line 1306
  97. theorem OAI.EntropyPhotonNumber.block_relativeEntropy_tilt_lower line 1318
  98. theorem OAI.FiniteBlock.block_basis line 1346
  99. def OAI.FiniteBlock.entries line 1350
  100. theorem OAI.FiniteBlock.trace_block_bounded line 1354
  101. theorem OAI.EntropyPhotonNumber.blockState_expectation line 1379
  102. theorem OAI.QuantumCalculus.matrix_duhamel_mixed_integrand line 1409
  103. theorem OAI.QuantumCalculus.matrix_duhamel_mixed line 1434
  104. theorem OAI.QuantumCalculus.normalized_expectation_deriv line 1465
  105. theorem OAI.QuantumCalculus.quadratic_coefficient_nonneg line 1519
  106. theorem OAI.QuantumCalculus.hessian_comparison line 1533
  107. def OAI.EntropyPhotonNumber.KrausFlow.dual line 1579
  108. theorem OAI.EntropyPhotonNumber.KrausFlow.dual_entry line 1582
  109. theorem OAI.EntropyPhotonNumber.KrausFlow.expectation_dual line 1586
  110. theorem OAI.EntropyPhotonNumber.KrausFlow.dual_selfAdjoint line 1598
  111. theorem OAI.EntropyPhotonNumber.expectation_mixture line 1602
  112. theorem OAI.EntropyPhotonNumber.blockTilt_expectation_formula line 1617
  113. theorem OAI.EntropyPhotonNumber.blockTilt_expectation_deriv line 1631
  114. theorem OAI.EntropyPhotonNumber.blockTilt_expectation_zero line 1644
  115. theorem OAI.EntropyPhotonNumber.expectation_block_of_eigen line 1658
  116. theorem OAI.EntropyPhotonNumber.expectation_block_of_eigen_re line 1673
  117. theorem OAI.EntropyPhotonNumber.crossEntropy_mixture_summable line 1684
  118. theorem OAI.EntropyPhotonNumber.one_port_relative_entropy_bound line 1696
  119. def OAI.FiniteBlock.mean line 1747
  120. def OAI.FiniteBlock.variance line 1749
  121. def OAI.FiniteBlock.covariance line 1752
  122. theorem OAI.EntropyPhotonNumber.flow_finite_hessian line 1760
  123. theorem OAI.FiniteBlock.mean_scale line 1833
  124. theorem OAI.FiniteBlock.variance_scale line 1840
  125. theorem OAI.FiniteBlock.covariance_scale_self line 1853
  126. theorem OAI.BKM.compression_mean line 1877
  127. theorem OAI.BKM.compression_quadratic line 1886
  128. theorem OAI.BKM.compression_hessian_to_variance line 1894
  129. theorem OAI.EntropyPhotonNumber.crossEntropy_reindex line 1929
  130. theorem OAI.EntropyPhotonNumber.finite_entries_selfAdjoint line 1934
  131. theorem OAI.EntropyPhotonNumber.expectation_eigen_hasSum line 1942
  132. theorem OAI.EntropyPhotonNumber.flow_full_hessian line 1949
  133. theorem OAI.EntropyPhotonNumber.minimum_component_hessian line 2003
  134. theorem OAI.BKM.entry_real_smul line 2054
  135. theorem OAI.BKM.entry_realPart line 2061
  136. theorem OAI.BKM.entry_imaginaryPart line 2067
  137. theorem OAI.Complex.normSq_polar_parts line 2079
  138. theorem OAI.BKM.quadratic_adjoint line 2093
  139. theorem OAI.BKM.quadratic_parts line 2102
  140. theorem OAI.BKM.mean_adjoint line 2133
  141. theorem OAI.BKM.mean_parts line 2137
  142. def OAI.BKM.variance line 2175
  143. theorem OAI.BKM.variance_parts line 2178
  144. theorem OAI.BKM.entry_block line 2194
  145. theorem OAI.BKM.mean_block line 2204
  146. theorem OAI.BKM.quadratic_block line 2211
  147. theorem OAI.BKM.normSq_mean_selfAdjoint line 2229
  148. theorem OAI.BKM.variance_block line 2238
  149. theorem OAI.BKM.block_realPart line 2247
  150. theorem OAI.BKM.block_imaginaryPart line 2254
  151. theorem OAI.EntropyPhotonNumber.mean_expectation line 2267
  152. theorem OAI.EntropyPhotonNumber.KrausFlow.dual_add line 2274
  153. theorem OAI.EntropyPhotonNumber.KrausFlow.dual_smul line 2276
  154. theorem OAI.EntropyPhotonNumber.KrausFlow.dual_real_smul line 2278
  155. theorem OAI.EntropyPhotonNumber.KrausFlow.dual_sub line 2282
  156. theorem OAI.EntropyPhotonNumber.KrausFlow.dual_adjoint line 2289
  157. theorem OAI.EntropyPhotonNumber.KrausFlow.dual_realPart line 2291
  158. theorem OAI.EntropyPhotonNumber.KrausFlow.dual_imaginaryPart line 2296
  159. theorem OAI.EntropyPhotonNumber.complex_component_hessian line 2308
  160. theorem OAI.EntropyPhotonNumber.minimum_complex_hessian line 2329
  161. theorem OAI.EntropyPhotonNumber.flow_complex_hessian line 2362
  162. theorem OAI.BKM.mean_reindex line 2398
  163. theorem OAI.BKM.quadratic_reindex line 2403
  164. theorem OAI.BKM.variance_reindex line 2408
  165. theorem OAI.EntropyPhotonNumber.minimum_all_blocks_hessian line 2417
  166. def OAI.BKM.vector line 2489
  167. theorem OAI.BKM.vector_apply line 2497
  168. theorem OAI.BKM.vector_add line 2501
  169. theorem OAI.BKM.vector_sub line 2507
  170. theorem OAI.BKM.vector_smul line 2513
  171. theorem OAI.BKM.vector_norm line 2519
  172. theorem OAI.BKM.vector_id_inner line 2526
  173. theorem OAI.BKM.vector_id_norm line 2545
  174. theorem OAI.BKM.quadratic_center line 2553
  175. theorem OAI.BKM.center_id line 2569
  176. theorem OAI.BKM.center_center line 2572
  177. theorem OAI.BKM.center_sub_scalar line 2577
  178. theorem OAI.BKM.variance_sub_scalar line 2585
  179. theorem OAI.CenteredTests.exists_block line 2595
  180. theorem OAI.EntropyPhotonNumber.KrausFlow.dual_id line 2626
  181. theorem OAI.EntropyPhotonNumber.blocks_to_centered_hessian line 2630
  182. theorem OAI.EntropyPhotonNumber.minimum_centered_hessian line 2653
  183. theorem OAI.EntropyPhotonNumber.minimum_all_blocks_hessian_data line 2679
  184. theorem OAI.EntropyPhotonNumber.minimum_centered_hessian_data line 2748
  185. theorem OAI.QuantumTrace.positive_eq_of_quadratic line 2783
  186. def OAI.EntropyPhotonNumber.GibbsData.quarticLogarithm line 2804
  187. theorem OAI.EntropyPhotonNumber.GibbsData.quarticLogarithm_parseval line 2808
  188. theorem OAI.EntropyPhotonNumber.GibbsData.exact_logarithmic_identity line 2819