OAI/MathematicalPhysics/PEPSSubvolume/EntropyMoments.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Dyadic log moments and ground-state spectral tails.

  1. lemma OAI.PolynomialPEPS.Subvolume.Dyadic.dyadic_linear_bound line 24
  2. theorem OAI.PolynomialPEPS.Subvolume.Dyadic.quadratic_bound line 68
  3. def OAI.PolynomialPEPS.Subvolume.MGFScalar.moment line 93
  4. def OAI.PolynomialPEPS.Subvolume.MGFScalar.entropy line 94
  5. def OAI.PolynomialPEPS.Subvolume.MGFScalar.logMoment line 95
  6. lemma OAI.PolynomialPEPS.Subvolume.MGFScalar.moment_zero line 97
  7. lemma OAI.PolynomialPEPS.Subvolume.MGFScalar.moment_pos line 100
  8. lemma OAI.PolynomialPEPS.Subvolume.MGFScalar.summand_derivative line 107
  9. lemma OAI.PolynomialPEPS.Subvolume.MGFScalar.moment_derivative line 120
  10. lemma OAI.PolynomialPEPS.Subvolume.MGFScalar.logMoment_zero line 125
  11. lemma OAI.PolynomialPEPS.Subvolume.MGFScalar.logMoment_derivative line 128
  12. lemma OAI.PolynomialPEPS.Subvolume.MGFScalar.neg_log_one_sub_le line 135
  13. lemma OAI.PolynomialPEPS.Subvolume.MGFScalar.log_recurrence line 145
  14. theorem OAI.PolynomialPEPS.Subvolume.MGFScalar.subgaussian_of_gap_recurrence line 156
  15. def OAI.PolynomialPEPS.Subvolume.HermitianReplacement.symmetrize line 174
  16. lemma OAI.PolynomialPEPS.Subvolume.HermitianReplacement.symmetrize_hermitian line 176
  17. lemma OAI.PolynomialPEPS.Subvolume.HermitianReplacement.symmetrize_supported line 180
  18. lemma OAI.PolynomialPEPS.Subvolume.HermitianReplacement.symmetrize_norm line 188
  19. lemma OAI.PolynomialPEPS.Subvolume.HermitianReplacement.symmetrize_self line 199
  20. lemma OAI.PolynomialPEPS.Subvolume.HermitianReplacement.symmetrize_sum line 203
  21. lemma OAI.PolynomialPEPS.Subvolume.HermitianReplacement.symmetrize_add line 207
  22. lemma OAI.PolynomialPEPS.Subvolume.HermitianReplacement.replacement_preserves_H line 211
  23. lemma OAI.PolynomialPEPS.Subvolume.GroundMGF.gap_moment_recurrence line 226
  24. theorem OAI.PolynomialPEPS.Subvolume.GroundMGF.log_moment_bound line 255