OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumSingletStar.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContinuumCoulomb.qmaPauliKernel line 12
2. theorem OAI.ContinuumCoulomb.qmaPauliKernel_self line 15
3. theorem OAI.ContinuumCoulomb.qmaPauliKernel_eq line 20
4. theorem OAI.ContinuumCoulomb.qmaHeisenberg_symm line 23
5. def OAI.ContinuumCoulomb.qmaSingletStar line 30
6. theorem OAI.ContinuumCoulomb.qmaSingletStar_compression line 35
7. theorem OAI.ContinuumCoulomb.qmaSingletStar_cross_zero line 57

   Source documentation

   Separate singlet pairs have zero mixed second-order compression.

   theorem qmaSingletStar_cross_zero (n r : ℕ) (Delta : ℝ) (e f : Fin r) (hef : e ≠ f)
       (site site' : κ → Fin n) (member member' : κ → Fin 2) (amplitude amplitude' : κ → ℝ) :
       mediatorCompression n r (qmaSingletStar n r e site member amplitude *
         liftedMediatorInverse n r Delta * qmaSingletStar n r f site' member' amplitude') = 0 := by
   …

   Mentions: OAI.ContinuumCoulomb.mediatorCompression, OAI.ContinuumCoulomb.qmaSingletStar, OAI.ContinuumCoulomb.liftedMediatorInverse

8. def OAI.ContinuumCoulomb.qmaRoutingStars line 65

   Source documentation

   All routing stars are applied simultaneously, one per distinct singlet pair.

   def qmaRoutingStars (n r : ℕ) (site : Fin r → κ → Fin n)
       (member : Fin r → κ → Fin 2) (amplitude : Fin r → κ → ℝ) :
       Matrix (MediatedSpinBasis n r) (MediatedSpinBasis n r) ℂ :=
   …

   Mentions: OAI.ContinuumCoulomb.MediatedSpinBasis

9. theorem OAI.ContinuumCoulomb.qmaRoutingStars_compression line 70