OAI/MathematicalPhysics/PEPSMove/RenyiSlack.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolynomialPEPS.PhysicalMove.RenyiSlack.gap line 16
2. theorem OAI.PolynomialPEPS.PhysicalMove.RenyiSlack.gap_ge_square line 18
3. theorem OAI.PolynomialPEPS.PhysicalMove.RenyiSlack.gap_nonneg line 30
4. theorem OAI.PolynomialPEPS.PhysicalMove.RenyiSlack.square_negative line 33
5. theorem OAI.PolynomialPEPS.PhysicalMove.RenyiSlack.exp_neg_linear line 42
6. theorem OAI.PolynomialPEPS.PhysicalMove.RenyiSlack.square_small line 55
7. theorem OAI.PolynomialPEPS.PhysicalMove.RenyiSlack.linear_middle line 69
8. theorem OAI.PolynomialPEPS.PhysicalMove.RenyiSlack.constant_large line 84
9. theorem OAI.PolynomialPEPS.PhysicalMove.RenyiSlack.phase_le_gap line 99
10. theorem OAI.PolynomialPEPS.PhysicalMove.RenyiSlack.weighted_phase_le line 157
11. theorem OAI.PolynomialPEPS.PhysicalMove.RenyiSlack.phase_young line 184
12. theorem OAI.PolynomialPEPS.PhysicalMove.RenyiSlack.weighted_phase_no_support line 230