OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/SourcePauli.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContinuumCoulomb.sourceTensor line 13

   Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:189 (same declaration text).

2. theorem OAI.ContinuumCoulomb.sourceTensor_one line 16
3. theorem OAI.ContinuumCoulomb.sourceTensor_mul line 26
4. def OAI.ContinuumCoulomb.sourceLocalPauli line 32
5. theorem OAI.ContinuumCoulomb.pauli_sq line 36
6. theorem OAI.ContinuumCoulomb.sourceLocalPauli_sq line 40
7. theorem OAI.ContinuumCoulomb.sourceLocalPauli_commute line 50
8. theorem OAI.ContinuumCoulomb.pauli_entry_sum line 66

   Source documentation

   The Pauli contraction on two actual two-state spins.

   theorem pauli_entry_sum (a b c d : Fin 2) :
       (∑ μ : Fin 3, pauli μ a c * pauli μ b d) =
         2 * (if a = d ∧ b = c then (1 : ℂ) else 0) -
           (if a = c ∧ b = d then 1 else 0) := by
   …

   Mentions: OAI.ContinuumCoulomb.pauli

9. def OAI.ContinuumCoulomb.sourceSpectatorDelta line 73
10. theorem OAI.ContinuumCoulomb.sourceSpectatorDelta_eq_one line 76
11. theorem OAI.ContinuumCoulomb.sourceSpectatorDelta_eq_zero line 84
12. theorem OAI.ContinuumCoulomb.sourceLocalPauli_product_entry line 93
13. theorem OAI.ContinuumCoulomb.sourceSpinSwap_eq_iff line 113
14. def OAI.ContinuumCoulomb.sourceHeisenbergMatrix line 134
15. theorem OAI.ContinuumCoulomb.sourceLocalPauli_sum line 140

    Source documentation

    The Pauli sum on distinct sites equals the complete source Hamiltonian matrix, with every other spin acting as an untouched spectator.

    theorem sourceLocalPauli_sum (n : ℕ) (i j : Fin n) (hij : i ≠ j) :
        (∑ μ : Fin 3, sourceLocalPauli n i μ * sourceLocalPauli n j μ) =
          sourceHeisenbergMatrix n i j := by
    …

    Mentions: OAI.ContinuumCoulomb.sourceLocalPauli, OAI.ContinuumCoulomb.sourceHeisenbergMatrix

16. theorem OAI.ContinuumCoulomb.sourceHeisenbergMatrix_mulVec line 179

    Source documentation

    Matrix multiplication agrees with the swap-based Heisenberg action.

    theorem sourceHeisenbergMatrix_mulVec (n : ℕ) (i j : Fin n) (u : SourceSpinVector n) :
        sourceHeisenbergMatrix n i j *ᵥ u = sourceHeisenbergAction i j u := by
    …

    Mentions: OAI.ContinuumCoulomb.SourceSpinVector, OAI.ContinuumCoulomb.sourceHeisenbergMatrix, OAI.ContinuumCoulomb.sourceHeisenbergAction