OAI/Analysis/LaughlinFock/RelativePerturbation.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Relative Perturbation.

  1. def OAI.LaughlinFock.stackFamily line 18
  2. theorem OAI.LaughlinFock.stackFamily_mulVec line 22
  3. theorem OAI.LaughlinFock.stackFamily_gram line 26
  4. theorem OAI.LaughlinFock.stackFamily_kronecker line 33
  5. theorem OAI.LaughlinFock.isHermitian_kronecker line 56
  6. theorem OAI.LaughlinFock.family_gram_majorant line 62
  7. def OAI.LaughlinFock.localBlockError line 90
  8. theorem OAI.LaughlinFock.localBlockError_hermitian line 94
  9. theorem OAI.LaughlinFock.localBlockError_tendsto line 100
  10. theorem OAI.LaughlinFock.local_relative_error line 120
  11. theorem OAI.LaughlinFock.stackFamily_coupled line 164
  12. theorem OAI.LaughlinFock.stackFamily_mul line 177
  13. theorem OAI.LaughlinFock.quadratic_family_change line 183
  14. theorem OAI.LaughlinFock.tendsto_matrix_mul line 209
  15. theorem OAI.LaughlinFock.tendsto_matrix_adjoint line 222
  16. theorem OAI.LaughlinFock.hermitian_congruence line 231
  17. theorem OAI.LaughlinFock.quadratic_family_mix line 239
  18. def OAI.LaughlinFock.localFourScale line 247
  19. theorem OAI.LaughlinFock.localFourScale_tendsto line 250
  20. theorem OAI.LaughlinFock.local_transfer_of_limitpositive line 257
  21. def OAI.LaughlinFock.orbitalMerge line 313
  22. def OAI.LaughlinFock.localOrbital line 316
  23. def OAI.LaughlinFock.spectatorOrbital line 319
  24. theorem OAI.LaughlinFock.localOrbital_val line 322
  25. theorem OAI.LaughlinFock.spectatorOrbital_val line 325
  26. def OAI.LaughlinFock.occupationMerge line 330
  27. theorem OAI.LaughlinFock.occupationMerge_apply line 333
  28. theorem OAI.LaughlinFock.localOrbital_mem_occupationMerge line 336
  29. theorem OAI.LaughlinFock.occupationMerge_erase line 342
  30. theorem OAI.LaughlinFock.occupationMerge_lower_count line 355
  31. theorem OAI.LaughlinFock.annihilator_spectator_factorization line 376
  32. def OAI.LaughlinFock.spectatorExtension line 387
  33. theorem OAI.LaughlinFock.spectatorExtension_annihilator line 391
  34. theorem OAI.LaughlinFock.spectatorExtension_mul line 398
  35. theorem OAI.LaughlinFock.spectatorExtension_adjoint line 403
  36. theorem OAI.LaughlinFock.spectatorExtension_sum line 408
  37. theorem OAI.LaughlinFock.spectatorExtension_add line 414
  38. theorem OAI.LaughlinFock.spectatorExtension_smul line 420
  39. theorem OAI.LaughlinFock.spectatorExtension_real_smul line 426
  40. theorem OAI.LaughlinFock.spectatorExtension_posSemidef line 432
  41. theorem OAI.LaughlinFock.spectatorExtension_zero line 436
  42. theorem OAI.LaughlinFock.spectatorExtension_pair line 443
  43. def OAI.LaughlinFock.partialHamiltonian line 491
  44. theorem OAI.LaughlinFock.partialHamiltonian_posSemidef line 494
  45. theorem OAI.LaughlinFock.spectatorExtension_localHamiltonian line 498
  46. theorem OAI.LaughlinFock.fock_transfer_of_limitpositive line 509