OAI/InformationTheory/PhotonNumber/SpectralForms.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BKM.reindexBasis line 28
  2. theorem OAI.BKM.reindexBasis_apply line 37
  3. theorem OAI.BKM.basis_hasSum_normSq line 41
  4. def OAI.BKM.entry line 45
  5. theorem OAI.BKM.entry_adjoint line 47
  6. theorem OAI.BKM.hasSum_column line 52
  7. theorem OAI.BKM.hasSum_row line 55
  8. theorem OAI.BKM.weighted_column_summable line 61
  9. theorem OAI.BKM.weighted_row_summable line 77
  10. theorem OAI.BKM.logMean_summable line 83
  11. theorem OAI.BKM.tendsto_square_finset line 102
  12. theorem OAI.BKM.hasSum_square_finset line 111
  13. theorem OAI.BKM.finite_hessian_to_variance line 116
  14. def OAI.SpectralTests.space line 141
  15. theorem OAI.SpectralTests.frequency_finite line 143
  16. def OAI.SpectralTests.multiplier line 167
  17. theorem OAI.SpectralTests.multiplier_generator line 172
  18. theorem OAI.SpectralTests.multiplier_mem line 181
  19. theorem OAI.SpectralTests.square_summable_iff line 193
  20. theorem OAI.SpectralTests.mass_summable line 198
  21. def OAI.CenteredTests.entryMap line 213
  22. theorem OAI.CenteredTests.entryMap_apply line 219
  23. theorem OAI.CenteredTests.entryMap_injective line 223
  24. def OAI.CenteredTests.generator line 240
  25. theorem OAI.CenteredTests.generator_entry line 245
  26. theorem OAI.CenteredTests.generator_frequency line 255
  27. def OAI.CenteredTests.operatorSpace line 276
  28. def OAI.CenteredTests.coordinates line 279
  29. theorem OAI.CenteredTests.coordinates_eq_span line 282
  30. theorem OAI.CenteredTests.coordinates_mass line 289
  31. theorem OAI.ThermalMetric.observable_summable line 309
  32. def OAI.ThermalMetric.observableMap line 329
  33. theorem OAI.ThermalMetric.observableMap_apply line 338
  34. theorem OAI.ThermalMetric.observableMap_id line 344
  35. def OAI.ThermalMetric.centerProjection line 358
  36. theorem OAI.ThermalMetric.centerProjection_apply line 362
  37. theorem OAI.ThermalMetric.centerProjection_mem line 365
  38. theorem OAI.ThermalMetric.centerProjection_eq line 370
  39. theorem OAI.ThermalMetric.centered_single_dense line 377
  40. theorem OAI.ThermalMetric.identityVector_apply line 405
  41. theorem OAI.ThermalMetric.identityVector_inner line 415
  42. def OAI.ThermalMetric.matrixGenerator line 430
  43. theorem OAI.ThermalMetric.matrixGenerator_projection line 436
  44. theorem OAI.ThermalMetric.matrixGenerator_dense line 451
  45. theorem OAI.ThermalMetric.observableMap_generator line 481
  46. theorem OAI.ThermalMetric.observable_core_dense line 504
  47. theorem OAI.ThermalMetric.functional_bound_of_core line 514
  48. theorem OAI.ThermalMetric.restricted_norm_bound_of_core line 532
  49. def OAI.CenteredTests.includeRange line 567
  50. def OAI.CenteredTests.realize line 573
  51. theorem OAI.CenteredTests.realize_entries line 579
  52. theorem OAI.CenteredTests.realize_mem line 584
  53. def OAI.CenteredTests.system line 591
  54. theorem OAI.ThermalMetric.reference_plus line 614
  55. theorem OAI.ThermalMetric.reference_minus line 621
  56. structure OAI.ThermalSpectral.Space line 634
  57. def OAI.ThermalSpectral.Space.param line 645
  58. def OAI.ThermalSpectral.Space.base line 646
  59. theorem OAI.ThermalSpectral.Space.base_pos line 647
  60. def OAI.ThermalSpectral.Space.coords line 648
  61. theorem OAI.ThermalSpectral.Space.coords_norm line 650
  62. def OAI.ThermalSpectral.Space.quad line 655
  63. def OAI.ThermalSpectral.Space.plus line 658
  64. def OAI.ThermalSpectral.Space.minus line 659
  65. theorem OAI.ThermalSpectral.Space.freq_cancel line 661
  66. theorem OAI.ThermalSpectral.Space.plus_entry line 666
  67. theorem OAI.ThermalSpectral.Space.minus_entry line 679
  68. theorem OAI.ThermalSpectral.Space.plus_summable line 692
  69. theorem OAI.ThermalSpectral.Space.minus_summable line 695
  70. theorem OAI.ThermalSpectral.Space.constant_summable line 698
  71. abbrev OAI.ThermalSpectral.Param line 704
  72. def OAI.ThermalSpectral.raw line 705
  73. def OAI.ThermalSpectral.Space.pparam line 706
  74. def OAI.ThermalSpectral.Space.pquad line 707
  75. def OAI.ThermalSpectral.targetMap line 710
  76. def OAI.ThermalSpectral.diagram line 717
  77. theorem OAI.ThermalSpectral.targetMap_norm line 725
  78. theorem OAI.ThermalSpectral.diagram_comparison line 732
  79. def OAI.ThermalSpectral.plusWeight line 766
  80. def OAI.ThermalSpectral.minusWeight line 767
  81. def OAI.ThermalSpectral.thermalWeight line 768
  82. theorem OAI.ThermalSpectral.plusWeight_pos line 770
  83. theorem OAI.ThermalSpectral.minusWeight_pos line 772
  84. theorem OAI.ThermalSpectral.diagram_thermal line 775
  85. theorem OAI.ThermalMetric.weight_bounds line 795
  86. def OAI.ThermalMetric.lowerWeight line 803
  87. theorem OAI.ThermalMetric.lowerWeight_bounds line 805
  88. theorem OAI.ThermalMetric.lowerWeight_pos line 812
  89. def OAI.ThermalMetric.mixtureConstant line 815
  90. theorem OAI.ThermalMetric.mixtureConstant_pos line 817
  91. theorem OAI.ThermalMetric.mixtureConstant_sq line 820
  92. theorem OAI.ThermalMetric.BKM_weight_bound line 824
  93. def OAI.ThermalSpectral.Space.observable line 839
  94. theorem OAI.ThermalSpectral.Space.observable_norm_sq line 842
  95. theorem OAI.ThermalSpectral.Space.thermal_summable line 851
  96. theorem OAI.ThermalSpectral.Space.BKM_thermal_bound line 863
  97. theorem OAI.ThermalSpectral.Space.observable_mem_core line 874
  98. def OAI.CrossEnsemble.pairingLM line 885
  99. theorem OAI.CrossEnsemble.pairing_sub_right line 895
  100. theorem OAI.CrossEnsemble.pairing_sub_left line 903
  101. theorem OAI.WeightedGenerator.centeredLadder_lower line 916
  102. theorem OAI.WeightedGenerator.centeredLadder_raise line 927
  103. theorem OAI.WeightedGenerator.weakDefect_uncentered line 940
  104. theorem OAI.ThermalSpectral.Space.defectFunctional_observable line 959
  105. theorem OAI.ThermalSpectral.Space.defectFunctional_one line 973
  106. theorem OAI.ThermalSpectral.Space.weakDefect_centered line 984