OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorPhysical.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContinuumCoulomb.physicalMediatorEdgeSpoke line 12
2. def OAI.ContinuumCoulomb.physicalTotalMediatorSpokes line 18
3. def OAI.ContinuumCoulomb.physicalMediatorHamiltonian line 25

   Source documentation

   Central antiferromagnetic bonds with their explicit three-Delta singlet shifts, plus the physical original-spin and spoke interactions.

   def physicalMediatorHamiltonian (n r : ℕ) (Delta : ℝ)
       (C : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ)
       (left right : Fin r → Fin n) (member : Fin r → Fin 2) (amplitude : Fin r → ℝ) :
       Matrix (MediatedSpinBasis n r) (MediatedSpinBasis n r) ℂ :=
   …

   Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.MediatedSpinBasis

4. theorem OAI.ContinuumCoulomb.physicalMediatorPenalty_full_transform line 32
5. theorem OAI.ContinuumCoulomb.liftedSource_full_transform line 44
6. theorem OAI.ContinuumCoulomb.physicalMediatorEdgeSpoke_transform line 54
7. theorem OAI.ContinuumCoulomb.physicalTotalMediatorSpokes_transform line 60
8. theorem OAI.ContinuumCoulomb.physicalMediatorHamiltonian_transform line 70

   Source documentation

   Exact change of coordinates for the entire physical construction.

   theorem physicalMediatorHamiltonian_transform (n r : ℕ) (Delta : ℝ)
       (C : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ)
       (left right : Fin r → Fin n) (member : Fin r → Fin 2) (amplitude : Fin r → ℝ) :
       (fullMediatorBellMatrix n r).conjTranspose *
         physicalMediatorHamiltonian n r Delta C left right member amplitude *
           fullMediatorBellMatrix n r = bellMediatorHamiltonian n r Delta C left right member amplitude := by
   …

   Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.fullMediatorBellMatrix, OAI.ContinuumCoulomb.physicalMediatorHamiltonian, OAI.ContinuumCoulomb.bellMediatorHamiltonian

9. theorem OAI.ContinuumCoulomb.spinMatrixOperator_unitary_form line 80
10. theorem OAI.ContinuumCoulomb.mediatorFullBottom_unitary line 91

    Source documentation

    The complete variational infimum is invariant under the explicit unitary.

    theorem mediatorFullBottom_unitary (n r : ℕ)
        (U H : Matrix (MediatedSpinBasis n r) (MediatedSpinBasis n r) ℂ)
        (hGram : U.conjTranspose * U = 1) (hCogram : U * U.conjTranspose = 1) :
        mediatorFullBottom n r (U.conjTranspose * H * U) = mediatorFullBottom n r H := by
    …

    Mentions: OAI.ContinuumCoulomb.MediatedSpinBasis, OAI.ContinuumCoulomb.mediatorFullBottom

11. theorem OAI.ContinuumCoulomb.physicalSimultaneousMediator_bottom line 119

    Source documentation

    Physical full-spin spectral comparison for the simultaneous positive singlet spokes, including all excited sectors and unreplaced terms.

    theorem physicalSimultaneousMediator_bottom (n r : ℕ) {Delta : ℝ} (hDelta : 0 < Delta)
        (C : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ) (hC : C.conjTranspose = C)
        (left right : Fin r → Fin n) (hneq : ∀ e, left e ≠ right e)
        (J amplitude : Fin r → ℝ) (hcal : ∀ e, amplitude e ^ 2 = 2 * Delta * |J e|)
        {epsilon : ℝ} (hepsilon : 0 ≤ epsilon) (hsmall : epsilon ≤ 1 / 4)
        (hbound : ‖spinMatrixOperator (C ⊗ₖ (1 : Matrix (MediatorBasis r) (MediatorBasis r) ℂ))‖ +
          6 * ∑ e, |amplitude e| ≤ epsilon * (4 * Delta)) :
        |mediatorFullBottom n r (physicalMediatorHamiltonian n r Delta C left right
            (fun e => signedMediatorMember (J e)) amplitude) + 3 * ∑ e, |J e| -
          sourceMatrixBottom n (C + ∑ e, (J e : ℂ) • sourceHeisenbergMatrix n (left e) (right e))| ≤
            16 * Delta * epsilon ^ 3 := by
    …

    Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.spinMatrixOperator, OAI.ContinuumCoulomb.MediatorBasis, OAI.ContinuumCoulomb.mediatorFullBottom, OAI.ContinuumCoulomb.physicalMediatorHamiltonian, OAI.ContinuumCoulomb.signedMediatorMember, OAI.ContinuumCoulomb.sourceMatrixBottom, OAI.ContinuumCoulomb.sourceHeisenbergMatrix