OAI/Analysis/Laughlin/Asymptotics/LocalDiagonalLimit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Laughlin.Fock.localDiagonals line 11
  2. theorem OAI.Laughlin.Fock.localDiagonals_tendsto line 14
  3. theorem OAI.Laughlin.Fock.localInverseDiagonals_tendsto line 24
  4. theorem OAI.Laughlin.Fock.localMetricDiagonals_tendsto line 31
  5. def OAI.Laughlin.Fock.localDiagonalError line 38
  6. theorem OAI.Laughlin.Fock.localDiagonalError_nonneg line 41
  7. theorem OAI.Laughlin.Fock.localDiagonalError_tendsto line 43
  8. theorem OAI.Laughlin.Fock.localDiagonalError_bound line 49
  9. theorem OAI.Laughlin.Fock.localDiagonalError_quadratic line 54