OAI/Analysis/Laughlin/Pair/AffineChart.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Laughlin.pairAffineChart line 10
2. theorem OAI.Laughlin.pairAffineChart_bracket line 18
3. theorem OAI.Laughlin.pairAffineChart_pair line 24
4. def OAI.Laughlin.spectatorWeight line 38
5. def OAI.Laughlin.affineExponent line 41
6. theorem OAI.Laughlin.affineExponent_injective line 44
7. theorem OAI.Laughlin.spectatorWeight_ne_zero line 51
8. theorem OAI.Laughlin.pairAffineChart_spectator line 59