OAI/Analysis/Laughlin/Fock/OrbitIntegration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Laughlin.Fock.linearMap_rotation_coordinate_continuous line 11
2. theorem OAI.Laughlin.Fock.linearMap_rotation_norm_continuous line 24
3. theorem OAI.Laughlin.Fock.linearMap_rotation_norm_integrable line 31
4. theorem OAI.Laughlin.Fock.physical_pair_norm_haar_real line 36
5. theorem OAI.Laughlin.Fock.sourcePairWindow_haar line 44