OAI/Analysis/Laughlin/Operators/Certificate.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Laughlin.Certificate.rows line 9
2. def OAI.Laughlin.Certificate.U line 18
3. def OAI.Laughlin.Certificate.X line 25
4. def OAI.Laughlin.Certificate.e line 28
5. def OAI.Laughlin.Certificate.limitBound line 37
6. theorem OAI.Laughlin.Certificate.eta_numerator line 40
7. theorem OAI.Laughlin.Certificate.allowance_count line 43
8. theorem OAI.Laughlin.Certificate.final_margin line 47
9. theorem OAI.Laughlin.Certificate.final_margin_gt line 51