SpinEmbedding.lean`

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The canonical, norm-preserving embedding of the spin sector in Fock space.

theorem OAI.ContinuumCoulomb.HubbardGlobal.siteMode_val line 12
def OAI.ContinuumCoulomb.HubbardGlobal.spinModeOrderEmbedding line 15
def OAI.ContinuumCoulomb.HubbardGlobal.spinOccupationSet line 26
theorem OAI.ContinuumCoulomb.HubbardGlobal.spinOccupationSet_injective line 30
theorem OAI.ContinuumCoulomb.HubbardGlobal.spinWedge_eq_fockBasis line 41
Source documentation
The ordered spin wedge is exactly a canonical occupation-basis vector, with no arbitrary normalization or phase.
```
theorem spinWedge_eq_fockBasis (m : ℕ) (s : SourceSpinBasis (m + 1)) :
    spinWedge m s = fockBasis (2 * m + 1) (spinOccupationSet m s) := by
…
```
Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.HubbardGlobal.spinWedge, OAI.ContinuumCoulomb.HubbardGlobal.fockBasis, OAI.ContinuumCoulomb.HubbardGlobal.spinOccupationSet
def OAI.ContinuumCoulomb.HubbardGlobal.spinEmbedding line 54
theorem OAI.ContinuumCoulomb.HubbardGlobal.spinEmbedding_coordinate line 59
theorem OAI.ContinuumCoulomb.HubbardGlobal.spinEmbedding_coordinate_outside line 65
theorem OAI.ContinuumCoulomb.HubbardGlobal.spinEmbedding_injective line 71
theorem OAI.ContinuumCoulomb.HubbardGlobal.spinEmbedding_swap line 78
theorem OAI.ContinuumCoulomb.HubbardGlobal.spinEmbedding_heisenberg line 93
Source documentation
The actual Fock Heisenberg operator intertwines the source action on arbitrary, possibly entangled, spin vectors.
```
theorem spinEmbedding_heisenberg (m : ℕ) (u : SourceSpinVector (m + 1))
    (i j : Fin (m + 1)) (hij : i ≠ j) :
    siteHeisenberg (siteMode m i 0) (siteMode m i 1) (siteMode m j 0) (siteMode m j 1)
        (spinEmbedding m u) = spinEmbedding m (sourceHeisenbergAction i j u) := by
…
```
Mentions: OAI.ContinuumCoulomb.SourceSpinVector, OAI.ContinuumCoulomb.HubbardGlobal.siteHeisenberg, OAI.ContinuumCoulomb.HubbardGlobal.siteMode, OAI.ContinuumCoulomb.HubbardGlobal.spinEmbedding, OAI.ContinuumCoulomb.sourceHeisenbergAction
def OAI.ContinuumCoulomb.HubbardGlobal.fockMass line 111
theorem OAI.ContinuumCoulomb.HubbardGlobal.spinEmbedding_mass line 115
Source documentation
The embedding preserves the entire many-spin squared norm.
```
theorem spinEmbedding_mass (m : ℕ) (u : SourceSpinVector (m + 1)) :
    fockMass (spinEmbedding m u) = sourceSpinMass u := by
…
```
Mentions: OAI.ContinuumCoulomb.SourceSpinVector, OAI.ContinuumCoulomb.HubbardGlobal.fockMass, OAI.ContinuumCoulomb.HubbardGlobal.spinEmbedding, OAI.ContinuumCoulomb.sourceSpinMass