OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FockSector.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Fixed-particle support and the true low/high Fock projections.

  1. theorem OAI.ContinuumCoulomb.HubbardGlobal.totalNumber_basis line 14
  2. theorem OAI.ContinuumCoulomb.HubbardGlobal.totalNumber_eq_diagonal line 25
  3. theorem OAI.ContinuumCoulomb.HubbardGlobal.totalNumber_eigen_coordinate_zero line 31
  4. def OAI.ContinuumCoulomb.HubbardGlobal.IsHalfFilled line 42
  5. theorem OAI.ContinuumCoulomb.HubbardGlobal.isHalfFilled_of_totalNumber line 45
  6. theorem OAI.ContinuumCoulomb.HubbardGlobal.totalNumber_spinWedge line 49
  7. theorem OAI.ContinuumCoulomb.HubbardGlobal.totalNumber_spinEmbedding line 54
  8. theorem OAI.ContinuumCoulomb.HubbardGlobal.spinOccupationSet_range_iff line 63
  9. theorem OAI.ContinuumCoulomb.HubbardGlobal.highOccupationIndex_range_iff line 71
  10. theorem OAI.ContinuumCoulomb.HubbardGlobal.coordinateInclusion_restriction_apply line 80
  11. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowFock_projector_coordinates line 93
  12. def OAI.ContinuumCoulomb.HubbardGlobal.highProjection line 103
  13. theorem OAI.ContinuumCoulomb.HubbardGlobal.highFock_projector_coordinates line 107
  14. theorem OAI.ContinuumCoulomb.HubbardGlobal.highProjection_of_halfFilled_lowZero line 117
  15. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowProjection_transfer_spinWedge_zero line 130
  16. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowProjection_siteHopping_spinWedge_zero line 137
  17. theorem OAI.ContinuumCoulomb.HubbardGlobal.totalNumber_commute_siteHopping line 146
  18. theorem OAI.ContinuumCoulomb.HubbardGlobal.totalNumber_commute_graphHopping line 152
  19. theorem OAI.ContinuumCoulomb.HubbardGlobal.graphHopping_preserves_halfFilling line 159
  20. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowProjection_graphHopping_spinEmbedding_zero line 170
  21. theorem OAI.ContinuumCoulomb.HubbardGlobal.highProjection_graphHopping_spinEmbedding line 181

    Source documentation

    A true hop from an arbitrary spin state lies entirely in the actual half-filled charge-defect space.

    theorem highProjection_graphHopping_spinEmbedding (m : ℕ)
    (left right : Edge → Fin (m + 1)) (t : Edge → ℂ)
    (hloop : ∀ e, left e ≠ right e) (u : SourceSpinVector (m + 1)) :
    highProjection m (graphHopping m left right t (spinEmbedding m u)) =
      graphHopping m left right t (spinEmbedding m u) :=
…

    Mentions: OAI.ContinuumCoulomb.SourceSpinVector, OAI.ContinuumCoulomb.HubbardGlobal.highProjection, OAI.ContinuumCoulomb.HubbardGlobal.graphHopping, OAI.ContinuumCoulomb.HubbardGlobal.spinEmbedding