OAI/InformationTheory/PhotonNumber/Contraction.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EnsembleL2.secondMoment line 31
  2. theorem OAI.EnsembleL2.shifted_secondMoment line 33
  3. theorem OAI.EnsembleL2.center_secondMoment line 51
  4. theorem OAI.EnsembleL2.mean_square_le line 58
  5. def OAI.EnsembleL2.mixture line 64
  6. theorem OAI.EnsembleL2.mixture_norm_left line 67
  7. theorem OAI.EnsembleL2.mixture_norm_right line 72
  8. theorem OAI.EnsembleL2.mixture_hasSum line 77
  9. theorem OAI.EnsembleL2.mixture_mean line 86
  10. theorem OAI.EnsembleL2.mixture_secondMoment line 103
  11. theorem OAI.EnsembleL2.complex_mixture_square line 120
  12. theorem OAI.EnsembleL2.mixture_variance line 127
  13. theorem OAI.EnsembleL2.mixture_variance_left line 138
  14. theorem OAI.EnsembleL2.mixture_between_variance line 147
  15. def OAI.ThermalSpectral.Space.ensemble line 164
  16. theorem OAI.ThermalSpectral.Space.ensemble_norm line 166
  17. theorem OAI.ThermalSpectral.Space.ensemble_hasSum line 171
  18. theorem OAI.ThermalSpectral.Space.image_ensemble_norm line 174
  19. theorem OAI.ThermalSpectral.Space.minus_quad_ensemble line 179
  20. theorem OAI.ThermalSpectral.Space.plus_quad_ensemble line 186
  21. theorem OAI.EnsembleL2.mean_eq_of_operator_eq line 197
  22. theorem OAI.EnsembleL2.secondMoment_eq_of_operator_eq line 203
  23. theorem OAI.EnsembleL2.center_eq_of_operator_eq line 221
  24. theorem OAI.EnsembleL2.variance_eq_of_operator_eq line 227
  25. def OAI.BKM.mean line 237
  26. def OAI.BKM.center line 239
  27. theorem OAI.ThermalSpectral.Space.ensemble_operator line 249
  28. theorem OAI.ThermalSpectral.Space.ensemble_mean line 254
  29. theorem OAI.ThermalSpectral.Space.ensemble_center line 262
  30. theorem OAI.ThermalSpectral.Space.minus_quad_of_ensemble line 265
  31. theorem OAI.ThermalSpectral.Space.plus_quad_of_ensemble line 271
  32. theorem OAI.TensorLp.conditionalLeft_center line 282
  33. theorem OAI.TensorLp.conditionalRight_center line 294
  34. abbrev OAI.EntropyPhotonNumber.RawIndex line 311
  35. def OAI.EntropyPhotonNumber.rawEnsemble line 314
  36. theorem OAI.EntropyPhotonNumber.rawEnsemble_norm line 318
  37. def OAI.EntropyPhotonNumber.rawEnsembleEquiv line 328
  38. theorem OAI.EntropyPhotonNumber.rawEnsemble_operator line 335
  39. theorem OAI.EntropyPhotonNumber.raw_centered_arithmetic line 350
  40. theorem OAI.EnsembleL2.mean_adjoint line 372
  41. theorem OAI.EnsembleL2.center_adjoint line 375
  42. def OAI.EntropyPhotonNumber.rawFirstSlice line 385
  43. def OAI.EntropyPhotonNumber.rawSecondSlice line 389
  44. theorem OAI.EntropyPhotonNumber.rawFirstSlice_adjoint line 393
  45. theorem OAI.EntropyPhotonNumber.rawSecondSlice_adjoint line 398
  46. theorem OAI.EntropyPhotonNumber.replaced_arithmetic line 403
  47. theorem OAI.EnsembleL2.mixture_operator line 436
  48. theorem OAI.ThermalSpectral.Space.minus_center_of_ensemble line 464
  49. theorem OAI.ThermalSpectral.Space.plus_center_of_ensemble line 470
  50. theorem OAI.EntropyPhotonNumber.replaced_spectral_arithmetic line 481
  51. theorem OAI.BKM.entry_add line 521
  52. theorem OAI.BKM.entry_sub line 523
  53. theorem OAI.BKM.entry_smul line 525
  54. theorem OAI.BKM.entry_norm_le line 527
  55. theorem OAI.BKM.mean_summable line 534
  56. theorem OAI.BKM.mean_add line 541
  57. theorem OAI.BKM.mean_smul line 546
  58. theorem OAI.BKM.entry_id line 550
  59. theorem OAI.BKM.mean_id line 554
  60. theorem OAI.BKM.mean_neg line 566
  61. theorem OAI.BKM.mean_sub line 570
  62. def OAI.BKM.centerLM line 574
  63. theorem OAI.BKM.centerLM_apply line 580
  64. theorem OAI.BKM.mean_center line 583
  65. theorem OAI.BKM.mean_rankOne line 591
  66. theorem OAI.CenteredTests.generator_eq_center line 608
  67. theorem OAI.CenteredTests.mean_eq_zero line 614
  68. theorem OAI.ThermalSpectral.Space.quad_smul line 630
  69. theorem OAI.ThermalSpectral.Space.pquad_smul line 635
  70. theorem OAI.ThermalSpectral.Space.pquad_constant line 640
  71. theorem OAI.ThermalSpectral.Space.pquad_nonneg line 644
  72. theorem OAI.ThermalSpectral.Space.center_of_mem line 648
  73. def OAI.ThermalSpectral.Space.normalize line 653
  74. theorem OAI.ThermalSpectral.Space.normalize_quad line 656
  75. theorem OAI.ThermalSpectral.Space.normalize_pquad line 661
  76. def OAI.EntropyPhotonNumber.rawFirstSliceLM line 672
  77. def OAI.EntropyPhotonNumber.rawSecondSliceLM line 678
  78. def OAI.EntropyPhotonNumber.normalizedSlices line 684
  79. theorem OAI.EntropyPhotonNumber.physical_diagram_arithmetic line 690
  80. def OAI.BKM.quadratic line 728
  81. theorem OAI.ThermalSpectral.Space.pquad_one line 737
  82. theorem OAI.ThermalSpectral.Space.normalized_hessian line 741
  83. theorem OAI.ThermalSpectral.diagram_constant line 763
  84. theorem OAI.ThermalSpectral.diagram_reference line 796
  85. theorem OAI.ThermalSpectral.diagram_observable line 812
  86. theorem OAI.EntropyPhotonNumber.physical_thermal_contraction line 851
  87. def OAI.EntropyPhotonNumber.SpectralLogData.thermalSpace line 894
  88. theorem OAI.EntropyPhotonNumber.SpectralLogData.inverse_spectralColumns_operator line 903
  89. def OAI.EntropyPhotonNumber.SpectralLogData.weightedColumns line 910
  90. def OAI.EntropyPhotonNumber.SpectralLogData.ambientDefect line 917
  91. theorem OAI.EntropyPhotonNumber.SpectralLogData.ambientDefect_observable line 921
  92. theorem OAI.EntropyPhotonNumber.SpectralLogData.ambientDefect_one line 927
  93. theorem OAI.EntropyPhotonNumber.SpectralLogData.ambientDefect_norm line 932
  94. theorem OAI.EntropyPhotonNumber.SpectralLogData.weakDefect_centered line 939
  95. theorem OAI.EntropyPhotonNumber.SpectralLogData.ambientDefect_centered line 945
  96. theorem OAI.EntropyPhotonNumber.SpectralLogData.weakMean_eq_conj line 949