OAI/Analysis/Laughlin/Operators/MatrixMetricError.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Laughlin.Fock.entrySum line 9
2. theorem OAI.Laughlin.Fock.entrySum_nonneg line 11
3. theorem OAI.Laughlin.Fock.abs_le_entrySum line 15
4. def OAI.Laughlin.Fock.matrixMetricError line 19
5. theorem OAI.Laughlin.Fock.matrixMetricError_nonneg line 22
6. theorem OAI.Laughlin.Fock.matrixMetricError_bound line 26
7. theorem OAI.Laughlin.Fock.entrySum_tendsto line 40
8. theorem OAI.Laughlin.Fock.matrixMetricError_tendsto line 49