OAI/Analysis/LaughlinGap/Contraction.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Contraction.

  1. abbrev OAI.LaughlinGap.ColumnSpace line 18
  2. def OAI.LaughlinGap.columnProjection line 20
  3. def OAI.LaughlinGap.columnInclusion line 23
  4. lemma OAI.LaughlinGap.columnProjection_apply line 28
  5. lemma OAI.LaughlinGap.columnInclusion_apply line 31
  6. def OAI.LaughlinGap.blockOperator line 36
  7. lemma OAI.LaughlinGap.blockOperator_apply line 40
  8. lemma OAI.LaughlinGap.blockOperator_inner line 45
  9. theorem OAI.LaughlinGap.blockOperator_tendsto line 50
  10. theorem OAI.LaughlinGap.matrixLift_inner_eq_block line 64
  11. theorem OAI.LaughlinGap.conjugated_matrix_transfer line 73
  12. theorem OAI.LaughlinGap.matrixLift_conjugated_inner line 107
  13. theorem OAI.LaughlinGap.matrix_compression_tendsto line 117
  14. theorem OAI.LaughlinGap.Occupation.extendLocal_relative_energy_bound line 140
  15. theorem OAI.LaughlinGap.Occupation.local_relative_matrix_transfer line 149
  16. theorem OAI.LaughlinGap.Occupation.localFour_factor_tendsto line 190
  17. theorem OAI.LaughlinGap.Occupation.local_four_family_transfer line 196
  18. lemma OAI.LaughlinGap.Occupation.word_nil line 256
  19. lemma OAI.LaughlinGap.Occupation.word_cons line 257
  20. lemma OAI.LaughlinGap.Occupation.annihilation_anticommute line 260
  21. lemma OAI.LaughlinGap.Occupation.word_perm_scalar line 268
  22. lemma OAI.LaughlinGap.Occupation.word_eq_zero_of_not_nodup line 285
  23. theorem OAI.LaughlinGap.Occupation.word_normal_form line 298
  24. lemma OAI.LaughlinGap.Occupation.inner_vacuum_left line 305
  25. theorem OAI.LaughlinGap.Occupation.basisContraction_adjoint_vacuum line 309
  26. def OAI.LaughlinGap.Occupation.allBasisContraction line 316
  27. def OAI.LaughlinGap.Occupation.fullContraction line 319
  28. theorem OAI.LaughlinGap.Occupation.fullContraction_single line 322
  29. theorem OAI.LaughlinGap.Occupation.fullContraction_add line 327
  30. theorem OAI.LaughlinGap.Occupation.fullContraction_smul line 331
  31. theorem OAI.LaughlinGap.Occupation.fullContraction_zero line 335
  32. def OAI.LaughlinGap.Occupation.reconstruct line 338
  33. lemma OAI.LaughlinGap.Occupation.reconstruct_allBasisContraction line 346
  34. theorem OAI.LaughlinGap.Occupation.reconstruct_word line 352
  35. theorem OAI.LaughlinGap.Occupation.reconstruct_four_pair line 358
  36. def OAI.LaughlinGap.Occupation.createdGram line 375
  37. theorem OAI.LaughlinGap.Occupation.annihilator_gram_positive line 378
  38. theorem OAI.LaughlinGap.Occupation.local_four_family_transfer_of_gram line 393
  39. theorem OAI.LaughlinGap.monic_eval_pos_of_nonnegative_coefficients line 420
  40. theorem OAI.LaughlinGap.symmetric_posSemidef_of_charpoly_coefficients line 430
  41. theorem OAI.LaughlinGap.rational_charpoly_certificate_sound line 445
  42. theorem OAI.LaughlinGap.comparison_coefficient_tendsto line 468
  43. theorem OAI.LaughlinGap.comparison_coefficient_eventually_lt line 476
  44. theorem OAI.LaughlinGap.comparison_coefficient_eventually_one_div_twenty_five line 483
  45. abbrev OAI.LaughlinGap.Occupation.PairLabel line 494
  46. def OAI.LaughlinGap.Occupation.basicPair line 496
  47. def OAI.LaughlinGap.Occupation.pairContraction line 499
  48. def OAI.LaughlinGap.Occupation.oneContraction line 502
  49. lemma OAI.LaughlinGap.Occupation.basicPair_middle line 508
  50. lemma OAI.LaughlinGap.Occupation.annihilation_commute_basicPair line 528
  51. lemma OAI.LaughlinGap.Occupation.basicPair_commute line 534
  52. lemma OAI.LaughlinGap.Occupation.pairContraction_commute line 541
  53. def OAI.LaughlinGap.Occupation.pairOneContraction line 553
  54. theorem OAI.LaughlinGap.Occupation.pairContraction_middle line 557
  55. def OAI.LaughlinGap.Occupation.pairHamiltonian line 576
  56. def OAI.LaughlinGap.Occupation.pairThreeTerm line 580
  57. def OAI.LaughlinGap.Occupation.pairFourTerm line 585
  58. theorem OAI.LaughlinGap.Occupation.pairHamiltonian_square line 590