OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FockNorm.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Polynomial operator bounds from the actual exterior occupation basis.

  1. theorem OAI.ContinuumCoulomb.HubbardGlobal.create_unoccupied_basis_signed line 19

    Source documentation

    A creator sends an unoccupied canonical basis vector to the inserted occupation with its actual exterior permutation sign.

    theorem create_unoccupied_basis_signed (i : Fin (Q + 1))
    (A : Finset (Fin (Q + 1))) (hi : i ∉ A) :
    ∃ c : ℂ, (c = 1 ∨ c = -1) ∧
      create i (fockBasis Q A) = c • fockBasis Q (insert i A) := by
…

    Mentions: OAI.ContinuumCoulomb.HubbardGlobal.fockBasis

  2. def OAI.ContinuumCoulomb.HubbardGlobal.creationCoefficient line 42
  3. theorem OAI.ContinuumCoulomb.HubbardGlobal.creationCoefficient_signed line 45
  4. theorem OAI.ContinuumCoulomb.HubbardGlobal.creationCoefficient_occupied line 53
  5. theorem OAI.ContinuumCoulomb.HubbardGlobal.create_basis line 57
  6. theorem OAI.ContinuumCoulomb.HubbardGlobal.annihilate_create_unoccupied_basis line 65
  7. theorem OAI.ContinuumCoulomb.HubbardGlobal.annihilate_occupied_basis line 73
  8. def OAI.ContinuumCoulomb.HubbardGlobal.insertModeEquiv line 88
  9. theorem OAI.ContinuumCoulomb.HubbardGlobal.insertModeEquiv_val line 95
  10. theorem OAI.ContinuumCoulomb.HubbardGlobal.insertModeEquiv_erase line 99
  11. theorem OAI.ContinuumCoulomb.HubbardGlobal.insertModeEquiv_symm_insert line 103
  12. theorem OAI.ContinuumCoulomb.HubbardGlobal.create_coordinate line 107
  13. theorem OAI.ContinuumCoulomb.HubbardGlobal.annihilate_coordinate line 139
  14. theorem OAI.ContinuumCoulomb.HubbardGlobal.creationCoefficient_conj line 175
  15. theorem OAI.ContinuumCoulomb.HubbardGlobal.fock_inner_create_annihilate line 185

    Source documentation

    The creator and contraction are actual adjoints in the canonical occupation norm; the signs come from the exterior basis above.

    theorem fock_inner_create_annihilate (i : Fin (Q + 1)) (x y : Space Q) :
    (∑ B, star ((fockBasis Q).repr (create i x) B) * (fockBasis Q).repr y B) =
      ∑ A, star ((fockBasis Q).repr x A) * (fockBasis Q).repr (annihilate i y) A := by
…

    Mentions: OAI.ContinuumCoulomb.HubbardGlobal.fockBasis

  16. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockMass_create line 211
  17. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockMass_annihilate line 234
  18. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockMass_create_le line 257
  19. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockMass_annihilate_le line 269
  20. abbrev OAI.ContinuumCoulomb.HubbardGlobal.FockCoordinateSpace line 281
  21. def OAI.ContinuumCoulomb.HubbardGlobal.fockCoordinates line 283
  22. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockCoordinates_apply line 286
  23. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockCoordinates_norm_sq line 289
  24. def OAI.ContinuumCoulomb.HubbardGlobal.fockOperatorLinear line 294
  25. def OAI.ContinuumCoulomb.HubbardGlobal.fockOperator line 298
  26. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_coordinates line 302
  27. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_norm_le_one line 306
  28. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_create_norm line 318

    Source documentation

    Actual CAR creators and annihilators are contractions in the canonical occupation norm, uniformly in the number of spectator modes.

    theorem fockOperator_create_norm (i : Fin (Q + 1)) :
    ‖fockOperator (create i)‖ ≤ 1 :=
…

    Mentions: OAI.ContinuumCoulomb.HubbardGlobal.fockOperator

  29. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_annihilate_norm line 322
  30. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_create_adjoint line 326
  31. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_add line 339
  32. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_smul line 346
  33. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_mul line 353
  34. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_sum line 360
  35. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_transfer_norm line 368
  36. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_bondTransfer_norm line 375
  37. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_siteHopping_norm line 383
  38. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_graphHopping_norm line 397

    Source documentation

    The actual global hopping has an edge-sum bound, independent of the exponentially large Fock-space dimension.

    theorem fockOperator_graphHopping_norm {Edge : Type*} [Fintype Edge]
    (m : ℕ) (left right : Edge → Fin (m + 1)) (t : Edge → ℂ) :
    ‖fockOperator (graphHopping m left right t)‖ ≤ 4 * ∑ e, ‖t e‖ := by
…

    Mentions: OAI.ContinuumCoulomb.HubbardGlobal.fockOperator, OAI.ContinuumCoulomb.HubbardGlobal.graphHopping

  39. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_annihilate_adjoint line 411
  40. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_transfer_adjoint line 415
  41. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_bondTransfer_adjoint line 420
  42. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_siteHopping_adjoint line 425
  43. theorem OAI.ContinuumCoulomb.HubbardGlobal.fockOperator_graphHopping_adjoint line 430