OAI/Analysis/QuantumTrace/Basic.lean

GitHub source file

120 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuantumTrace.diagonalTrace line 17
  2. theorem OAI.QuantumTrace.basis_hasSum_norm_sq line 21
  3. theorem OAI.QuantumTrace.basis_tsum_enorm_sq line 32
  4. theorem OAI.QuantumTrace.sqrt_inner_eq line 38
  5. theorem OAI.QuantumTrace.diagonalTrace_eq_sqrt line 51
  6. theorem OAI.QuantumTrace.sum_norm_sq_basis_independent line 57
  7. theorem OAI.QuantumTrace.diagonalTrace_basis_independent line 73
  8. theorem OAI.QuantumTrace.quadratic_le_trace_mul_norm_sq line 87
  9. theorem OAI.QuantumTrace.operator_le_trace_smul_id line 106
  10. theorem OAI.QuantumTrace.norm_le_trace line 120
  11. theorem OAI.QuantumTrace.norm_apply_sq_le_basis_sum line 140
  12. theorem OAI.QuantumTrace.norm_le_sqrt_basis_sum line 164
  13. def OAI.QuantumTrace.basisApprox line 183
  14. theorem OAI.QuantumTrace.basisApprox_apply_basis line 187
  15. theorem OAI.QuantumTrace.basisApprox_isCompactOperator line 194
  16. theorem OAI.QuantumTrace.basisApprox_norm_sub_le line 206
  17. theorem OAI.QuantumTrace.compact_of_summable_basis_norm_sq line 222
  18. theorem OAI.QuantumTrace.compact_of_positive_finite_trace line 246
  19. theorem OAI.QuantumTrace.exists_eigenbasis line 257
  20. theorem OAI.QuantumTrace.cfc_apply_eigenvector line 297
  21. def OAI.QuantumTrace.entropyOperator line 333
  22. theorem OAI.QuantumTrace.entropyOperator_eq_complex line 335
  23. theorem OAI.QuantumTrace.entropyOperator_positive line 342
  24. theorem OAI.QuantumTrace.hasSum_trace_basis line 363
  25. theorem OAI.QuantumTrace.exists_positive_eigenbasis line 385
  26. theorem OAI.QuantumTrace.hasSum_quadratic_eigenbasis line 414
  27. theorem OAI.QuantumTrace.entropy_jensen_hasSum line 433
  28. theorem OAI.QuantumTrace.entropyOperator_apply_eigenvector line 451
  29. theorem OAI.QuantumTrace.entropyOperator_quadratic_le line 459
  30. theorem OAI.QuantumTrace.negMulLog_le_crossEntropy line 475
  31. theorem OAI.QuantumTrace.entropy_summable_and_le_crossEntropy line 490
  32. theorem OAI.QuantumTrace.tsum_finite_product line 509
  33. def OAI.QuantumTrace.thermalWeight line 519
  34. theorem OAI.QuantumTrace.thermalWeight_pos line 522
  35. theorem OAI.QuantumTrace.hasSum_thermalWeight line 528
  36. theorem OAI.QuantumTrace.log_thermalWeight line 551
  37. theorem OAI.QuantumTrace.summable_thermal_crossEntropy line 563
  38. theorem OAI.QuantumTrace.tsum_thermal_crossEntropy line 574
  39. theorem OAI.QuantumTrace.entropy_summable_finite_energy line 588
  40. theorem OAI.QuantumTrace.entropy_le_thermal_crossEntropy line 604
  41. theorem OAI.QuantumTrace.entropy_nonneg line 631
  42. theorem OAI.QuantumTrace.entropy_energy_bound line 637
  43. theorem OAI.QuantumTrace.entropy_summable_le_reference line 678
  44. theorem OAI.QuantumTrace.entropy_small_mass_bound line 695
  45. abbrev OAI.QuantumTrace.SequenceHilbert line 756
  46. def OAI.QuantumTrace.diagonalMap line 758
  47. theorem OAI.QuantumTrace.diagonalMap_apply line 778
  48. theorem OAI.QuantumTrace.diagonalMap_norm_le line 781
  49. theorem OAI.QuantumTrace.diagonalMap_injective line 792
  50. theorem OAI.QuantumTrace.diagonalMap_single line 798
  51. theorem OAI.QuantumTrace.diagonalMap_symmetric line 805
  52. theorem OAI.QuantumTrace.diagonalMap_positive line 815
  53. def OAI.QuantumTrace.sequenceBasis line 843
  54. theorem OAI.QuantumTrace.sequenceBasis_apply line 846
  55. theorem OAI.QuantumTrace.diagonalMap_cut line 848
  56. theorem OAI.QuantumTrace.diagonalMap_compact line 872
  57. theorem OAI.QuantumTrace.inversePower_bounded line 910
  58. def OAI.QuantumTrace.inversePower line 916
  59. theorem OAI.QuantumTrace.inversePower_apply line 920
  60. theorem OAI.QuantumTrace.inversePower_positive line 923
  61. theorem OAI.QuantumTrace.inversePower_adjoint line 927
  62. theorem OAI.QuantumTrace.inversePower_norm_le line 931
  63. theorem OAI.QuantumTrace.inversePower_injective line 938
  64. theorem OAI.QuantumTrace.inversePower_mul line 944
  65. theorem OAI.QuantumTrace.inversePower_zero line 950
  66. def OAI.QuantumTrace.gibbsFactor line 955
  67. theorem OAI.QuantumTrace.gibbsFactor_strictPositive line 961
  68. def OAI.QuantumTrace.gibbsInverse line 982
  69. theorem OAI.QuantumTrace.gibbsInverse_positive line 987
  70. theorem OAI.QuantumTrace.gibbsInverse_injective line 1010
  71. theorem OAI.QuantumTrace.gibbsInverse_compact line 1021
  72. theorem OAI.QuantumTrace.exists_strictly_positive_eigenbasis line 1034
  73. theorem OAI.QuantumTrace.gibbsFactor_inner_lower line 1070
  74. theorem OAI.QuantumTrace.gibbs_eigenvector_regular line 1084
  75. theorem OAI.QuantumTrace.sequenceBasis_inner line 1162
  76. theorem OAI.QuantumTrace.sequence_hasSum_norm_sq line 1168
  77. theorem OAI.QuantumTrace.real_exp_support line 1172
  78. theorem OAI.QuantumTrace.heat_weight_le_diagonal line 1177
  79. theorem OAI.QuantumTrace.basis_coordinate_hasSum line 1207
  80. theorem OAI.QuantumTrace.heat_trace_bound line 1215
  81. def OAI.QuantumTrace.numberWeight line 1245
  82. def OAI.QuantumTrace.rootNumberWeight line 1247
  83. theorem OAI.QuantumTrace.numberWeight_one_le line 1249
  84. theorem OAI.QuantumTrace.rootNumberWeight_one_le line 1253
  85. theorem OAI.QuantumTrace.rootNumberWeight_pow_four line 1257
  86. theorem OAI.QuantumTrace.rootNumberWeight_pow_eight line 1261
  87. theorem OAI.QuantumTrace.summable_exp_number line 1265
  88. theorem OAI.QuantumTrace.summable_exp_number_aux line 1292
  89. theorem OAI.QuantumTrace.inverseRootNumber_compact line 1305
  90. theorem OAI.QuantumTrace.gibbs_fock_spectral_regular line 1327
  91. theorem OAI.QuantumTrace.summable_polynomial_heat line 1360
  92. def OAI.QuantumTrace.basisDiagonal line 1390
  93. theorem OAI.QuantumTrace.basisDiagonal_positive line 1396
  94. theorem OAI.QuantumTrace.basisDiagonal_eigen line 1407
  95. theorem OAI.QuantumTrace.basisDiagonal_injective line 1418
  96. theorem OAI.QuantumTrace.basisDiagonal_trace line 1424
  97. theorem OAI.QuantumTrace.basisDiagonal_hasSum_trace line 1433
  98. def OAI.QuantumTrace.heatPartition line 1441
  99. def OAI.QuantumTrace.gibbsWeight line 1443
  100. theorem OAI.QuantumTrace.heatPartition_pos line 1445
  101. theorem OAI.QuantumTrace.gibbsWeight_pos line 1450
  102. theorem OAI.QuantumTrace.gibbsWeight_hasSum line 1453
  103. theorem OAI.QuantumTrace.gibbsWeight_bounded line 1459
  104. def OAI.QuantumTrace.spectralGibbs line 1466
  105. theorem OAI.QuantumTrace.spectralGibbs_positive line 1470
  106. theorem OAI.QuantumTrace.spectralGibbs_injective line 1474
  107. theorem OAI.QuantumTrace.spectralGibbs_trace_one line 1478
  108. theorem OAI.QuantumTrace.spectralGibbs_eigen line 1484
  109. theorem OAI.QuantumTrace.log_gibbsWeight line 1489
  110. theorem OAI.QuantumTrace.weighted_number_moment line 1499
  111. theorem OAI.QuantumTrace.gibbs_high_moment_summable line 1528
  112. theorem OAI.QuantumTrace.exists_gibbs_seventh_moment line 1567
  113. theorem OAI.QuantumTrace.polar_eigenbasis line 1616
  114. theorem OAI.QuantumTrace.inverse_factor_form_parseval line 1656
  115. def OAI.QuantumTrace.logarithmSandwich line 1716
  116. theorem OAI.QuantumTrace.logarithmSandwich_parseval line 1719
  117. theorem OAI.QuantumTrace.gibbs_logarithmSandwich_parseval line 1741
  118. theorem OAI.QuantumTrace.inverse_factor_eigen_preimage line 1755
  119. theorem OAI.QuantumTrace.logarithmSandwich_eigen_preimage line 1782
  120. theorem OAI.QuantumTrace.weighted_spectral_vectors line 1803