OAI/InformationTheory/PhotonNumber/SpectralLog.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SquareAnalysis.H line 27
  2. def OAI.SquareAnalysis.vector line 29
  3. theorem OAI.SquareAnalysis.vector_apply line 33
  4. theorem OAI.SquareAnalysis.hasSum_square line 36
  5. theorem OAI.SquareAnalysis.vector_norm_sq line 39
  6. def OAI.SquareAnalysis.linearMap line 43
  7. theorem OAI.SquareAnalysis.vector_norm_le line 49
  8. def OAI.SquareAnalysis.continuousMap line 58
  9. theorem OAI.SquareAnalysis.continuousMap_apply line 62
  10. def OAI.SquareAnalysis.gram line 69
  11. theorem OAI.SquareAnalysis.gram_positive line 73
  12. theorem OAI.SquareAnalysis.gram_quadratic line 78
  13. theorem OAI.SquareAnalysis.exists_positive_representation line 84
  14. def OAI.QuantumTrace.logCoordinates line 97
  15. theorem OAI.QuantumTrace.logCoordinates_square line 101
  16. theorem OAI.QuantumTrace.spectral_form_representation line 107
  17. structure OAI.EntropyPhotonNumber.SpectralLogData line 156
  18. def OAI.EntropyPhotonNumber.GibbsData.toSpectralLogData line 178
  19. def OAI.EntropyPhotonNumber.SpectralLogData.logCoefficient line 196
  20. theorem OAI.EntropyPhotonNumber.SpectralLogData.logCoefficient_nonneg line 197
  21. theorem OAI.EntropyPhotonNumber.SpectralLogData.spectralColumns_normalized line 201
  22. theorem OAI.EntropyPhotonNumber.SpectralLogData.spectralColumns_operator line 207
  23. theorem OAI.EntropyPhotonNumber.SpectralLogData.thermalGenerator_logarithmic_trace line 214
  24. def OAI.EntropyPhotonNumber.SpectralLogData.annihilationMatrix line 234
  25. def OAI.EntropyPhotonNumber.SpectralLogData.annihilationMean line 237
  26. def OAI.EntropyPhotonNumber.SpectralLogData.centeredMatrix line 239
  27. theorem OAI.EntropyPhotonNumber.SpectralLogData.annihilation_mean_summable line 242
  28. theorem OAI.EntropyPhotonNumber.SpectralLogData.centeredMatrix_mean_zero line 250
  29. theorem OAI.EntropyPhotonNumber.SpectralLogData.centeredMatrix_six_sums line 257
  30. theorem OAI.EntropyPhotonNumber.SpectralLogData.centeredMatrix_defect_summable line 270
  31. def OAI.EntropyPhotonNumber.SpectralLogData.defect line 278
  32. theorem OAI.EntropyPhotonNumber.SpectralLogData.defect_norm_sq line 284
  33. def OAI.EntropyPhotonNumber.SpectralLogData.centeredEnergy line 291
  34. theorem OAI.EntropyPhotonNumber.SpectralLogData.thermalGenerator_centered_logarithmic_trace line 294
  35. theorem OAI.EntropyPhotonNumber.SpectralLogData.entropy_production line 309
  36. theorem OAI.EntropyPhotonNumber.spectral_weighted_columns line 336
  37. theorem OAI.EntropyPhotonNumber.exists_spectralLogData_of_bound line 359
  38. def OAI.EntropyPhotonNumber.numberBasis line 399
  39. theorem OAI.EntropyPhotonNumber.numberBasis_apply line 402
  40. theorem OAI.EntropyPhotonNumber.trace_one_numberBasis line 407
  41. def OAI.TraceEnsemble.diagonalVector line 417
  42. theorem OAI.TraceEnsemble.diagonalVector_norm_sq line 421
  43. theorem OAI.TraceEnsemble.diagonalVector_eigen line 425
  44. def OAI.EntropyPhotonNumber.diagonalState line 450
  45. theorem OAI.EntropyPhotonNumber.diagonalState_eigen line 458
  46. theorem OAI.EntropyPhotonNumber.diagonalState_diagonal line 463
  47. def OAI.EntropyPhotonNumber.thermalState line 469
  48. theorem OAI.EntropyPhotonNumber.thermalState_diagonal line 473
  49. def OAI.EntropyPhotonNumber.mixture line 477
  50. theorem OAI.QuantumTrace.log_apply_eigenvector line 499
  51. def OAI.QuantumTrace.regularNegLog line 514
  52. theorem OAI.QuantumTrace.add_scalar_strictPositive line 517
  53. theorem OAI.QuantumTrace.regularNegLog_eigen line 522
  54. theorem OAI.QuantumTrace.regularNegLog_antitone line 531
  55. theorem OAI.QuantumTrace.regularNegLog_scalar_bounds line 543
  56. theorem OAI.QuantumTrace.negativeLog_form_mono line 553
  57. theorem OAI.QuantumTrace.eigenbasis_quadratic_pos line 616
  58. theorem OAI.EntropyPhotonNumber.mixture_replacement_le line 642
  59. theorem OAI.EntropyPhotonNumber.exists_faithful_eigenbasis_of_thermal_le line 650
  60. def OAI.EntropyPhotonNumber.vectorEnergy line 673
  61. def OAI.EntropyPhotonNumber.FiniteVectorEnergy line 676
  62. theorem OAI.EntropyPhotonNumber.thermal_negativeLog_hasSum line 679
  63. theorem OAI.EntropyPhotonNumber.negativeLog_le_thermal line 694
  64. theorem OAI.EntropyPhotonNumber.inverseWeight_two_norm line 720
  65. theorem OAI.EntropyPhotonNumber.inverseWeight_two_energy_term line 728
  66. theorem OAI.EntropyPhotonNumber.inverseWeight_two_finiteEnergy line 748
  67. theorem OAI.EntropyPhotonNumber.inverseWeight_two_energy line 753
  68. theorem OAI.EntropyPhotonNumber.exists_spectralLogData_of_thermal_le line 758