OAI/MathematicalPhysics/PEPSMove/LogMoments.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolynomialPEPS.PhysicalMove.RelativeLogMoment.square_le_cutoff line 16
2. theorem OAI.PolynomialPEPS.PhysicalMove.RelativeLogMoment.second_moment line 31
3. theorem OAI.PolynomialPEPS.PhysicalMove.RelativeLogMoment.exp_linear_remainder line 73
4. theorem OAI.PolynomialPEPS.PhysicalMove.RelativeLogMoment.tilted_second_moment line 94
5. theorem OAI.PolynomialPEPS.PhysicalMove.RelativeLogMoment.mgf_bound line 158
6. theorem OAI.PolynomialPEPS.PhysicalMove.RelativeLogMoment.spectral_mgf line 192