OAI/Analysis/Laughlin/Asymptotics/LocalMetricLimit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Laughlin.Fock.localMetricError line 9
2. theorem OAI.Laughlin.Fock.localMetricError_nonneg line 12
3. theorem OAI.Laughlin.Fock.localMetricError_tendsto line 14
4. theorem OAI.Laughlin.Fock.localMetricError_bound line 22
5. def OAI.Laughlin.Fock.localMetricMap line 29
6. theorem OAI.Laughlin.Fock.localMetricMap_coordinate line 32
7. theorem OAI.Laughlin.Fock.localMetric_error_quadratic line 43