OAI/Probability/ParisiFinite/ParisiEntropyDecomposition.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Parisi Entropy Decomposition.

  1. lemma OAI.ParisiSpectral.backwardC_entropy_integrable line 21
  2. lemma OAI.ParisiSpectral.backwardG_log_integrable line 35
  3. lemma OAI.ParisiSpectral.hankelCPD_entropy_sub_base line 48
  4. lemma OAI.ParisiSpectral.PositiveOnPD.heat_antitone line 93
  5. lemma OAI.ParisiSpectral.PositiveOnPD.heatObservation_antitone line 100
  6. lemma OAI.ParisiSpectral.hankelPD_heatObservation line 109
  7. lemma OAI.ParisiSpectral.heatObservation_pos line 126
  8. lemma OAI.ParisiSpectral.sechCube_PD line 139
  9. lemma OAI.ParisiSpectral.continuous_sechCube line 144
  10. lemma OAI.ParisiSpectral.hankelPD_baseCurvature line 147
  11. lemma OAI.ParisiSpectral.baseCurvature_strictAnti line 165
  12. lemma OAI.ParisiSpectral.baseCurvature_midpoint_lt line 181
  13. lemma OAI.ParisiFinite.BoundedCoefficient.expectedSquareCurvature_strict_midpoint line 201
  14. lemma OAI.ParisiSpectral.not_isLocalMax_of_strict_midpoint line 271
  15. lemma OAI.ParisiFinite.BoundedCoefficient.expectedSquareCurvature_not_isLocalMax line 294
  16. theorem OAI.ParisiFinite.full_support_minimizer line 306