OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FockBlocks.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Concrete hopping blocks on the actual half-filled Fock basis.

  1. def OAI.ContinuumCoulomb.HubbardGlobal.coordinateInclusionLinear line 17
  2. def OAI.ContinuumCoulomb.HubbardGlobal.coordinateInclusion line 25
  3. theorem OAI.ContinuumCoulomb.HubbardGlobal.coordinateInclusion_single line 29
  4. theorem OAI.ContinuumCoulomb.HubbardGlobal.coordinateInclusion_apply_image line 37
  5. theorem OAI.ContinuumCoulomb.HubbardGlobal.coordinateInclusion_apply_outside line 42
  6. theorem OAI.ContinuumCoulomb.HubbardGlobal.coordinateInclusion_norm_map line 49
  7. theorem OAI.ContinuumCoulomb.HubbardGlobal.coordinateInclusion_norm_le line 72
  8. def OAI.ContinuumCoulomb.HubbardGlobal.coordinateRestriction line 78
  9. theorem OAI.ContinuumCoulomb.HubbardGlobal.coordinateRestriction_apply line 81
  10. theorem OAI.ContinuumCoulomb.HubbardGlobal.coordinateRestriction_norm_le line 90
  11. theorem OAI.ContinuumCoulomb.HubbardGlobal.coordinateCompression_norm line 96
  12. abbrev OAI.ContinuumCoulomb.HubbardGlobal.ActualHubbardLowSpace line 109
  13. abbrev OAI.ContinuumCoulomb.HubbardGlobal.ActualHubbardHighSpace line 110
  14. def OAI.ContinuumCoulomb.HubbardGlobal.highOccupationIndex line 112
  15. theorem OAI.ContinuumCoulomb.HubbardGlobal.highOccupationIndex_injective line 115
  16. def OAI.ContinuumCoulomb.HubbardGlobal.lowFockInclusion line 120
  17. def OAI.ContinuumCoulomb.HubbardGlobal.highFockInclusion line 123
  18. def OAI.ContinuumCoulomb.HubbardGlobal.lowFockRestriction line 126
  19. def OAI.ContinuumCoulomb.HubbardGlobal.highFockRestriction line 129
  20. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowFockInclusion_norm line 132
  21. theorem OAI.ContinuumCoulomb.HubbardGlobal.highFockInclusion_norm line 135
  22. theorem OAI.ContinuumCoulomb.HubbardGlobal.lowFockRestriction_norm line 138
  23. theorem OAI.ContinuumCoulomb.HubbardGlobal.highFockRestriction_norm line 141
  24. def OAI.ContinuumCoulomb.HubbardGlobal.actualHubbardCoupling line 146
  25. def OAI.ContinuumCoulomb.HubbardGlobal.actualHubbardHighHopping line 152
  26. theorem OAI.ContinuumCoulomb.HubbardGlobal.actualHubbardCoupling_norm line 158
  27. theorem OAI.ContinuumCoulomb.HubbardGlobal.actualHubbardHighHopping_norm line 169
  28. theorem OAI.ContinuumCoulomb.HubbardGlobal.actual_hubbard_second_order line 182

    Source documentation

    The global perturbation bound with the actual Fock hopping blocks. Its only smallness condition is the explicit polynomial edge-sum bound.

    theorem actual_hubbard_second_order (m : ℕ) (U R : ℝ)
    (V : Fin (m + 1) → Fin (m + 1) → ℝ)
    (hsymm : ∀ i j, V i j = V j i) (hrow : ∀ i, ∑ j, |V i j| ≤ R)
    (hUR : R < U) (left right : Edge → Fin (m + 1)) (t : Edge → ℝ)
    {epsilon : ℝ} (hepsilon : 0 ≤ epsilon) (hsmall : epsilon < 1 / 2)
    (ht : 4 * ∑ e, |t e| ≤ epsilon * (U - R)) :
    let weight : HalfFilledHighBasis m → ℝ :=
…

    Mentions: OAI.ContinuumCoulomb.HubbardGlobal.HalfFilledHighBasis