OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorSector.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContinuumCoulomb.mediatorLowInclusion_apply line 13
2. theorem OAI.ContinuumCoulomb.mediatorHighInclusion_apply line 26
3. theorem OAI.ContinuumCoulomb.mediatorHighInclusion_vacuum line 32
4. theorem OAI.ContinuumCoulomb.mediatorLowRestriction_apply line 38
5. theorem OAI.ContinuumCoulomb.mediatorHighRestriction_apply line 42
6. theorem OAI.ContinuumCoulomb.mediatorLowRestriction_inclusion line 47
7. theorem OAI.ContinuumCoulomb.mediatorHighRestriction_inclusion line 51
8. theorem OAI.ContinuumCoulomb.mediatorLowRestriction_high line 55
9. theorem OAI.ContinuumCoulomb.mediatorHighRestriction_low line 60
10. theorem OAI.ContinuumCoulomb.mediator_full_decomposition line 67

    Source documentation

    Every full spin state decomposes into its singlet and triplet sectors.

    theorem mediator_full_decomposition (n r : ℕ) (x : MediatorFullSpace n r) :
        mediatorLowInclusion n r (mediatorLowRestriction n r x) +
          mediatorHighInclusion n r (mediatorHighRestriction n r x) = x := by
    …

    Mentions: OAI.ContinuumCoulomb.MediatorFullSpace, OAI.ContinuumCoulomb.mediatorLowInclusion, OAI.ContinuumCoulomb.mediatorLowRestriction, OAI.ContinuumCoulomb.mediatorHighInclusion, OAI.ContinuumCoulomb.mediatorHighRestriction

11. theorem OAI.ContinuumCoulomb.mediatorLow_real_inner line 80
12. theorem OAI.ContinuumCoulomb.mediatorHigh_real_inner line 84
13. theorem OAI.ContinuumCoulomb.mediatorLowInclusion_norm_map line 88
14. theorem OAI.ContinuumCoulomb.mediatorHighInclusion_norm_map line 92
15. def OAI.ContinuumCoulomb.assembleMediator line 96
16. theorem OAI.ContinuumCoulomb.assembleMediator_norm_sq line 99
17. theorem OAI.ContinuumCoulomb.mediatorLow_operator_compression line 107

    Source documentation

    The matrix vacuum compression agrees with the actual Hilbert-space block.

    theorem mediatorLow_operator_compression (n r : ℕ)
        (M : Matrix (MediatedSpinBasis n r) (MediatedSpinBasis n r) ℂ) :
        (mediatorLowRestriction n r).comp
          ((spinMatrixOperator M).comp (mediatorLowInclusion n r)) =
            spinMatrixOperator (mediatorCompression n r M) := by
    …

    Mentions: OAI.ContinuumCoulomb.MediatedSpinBasis, OAI.ContinuumCoulomb.mediatorLowRestriction, OAI.ContinuumCoulomb.spinMatrixOperator, OAI.ContinuumCoulomb.mediatorLowInclusion, OAI.ContinuumCoulomb.mediatorCompression

18. theorem OAI.ContinuumCoulomb.spinMatrixOperator_diagonal line 120
19. theorem OAI.ContinuumCoulomb.liftedMediatorInverse_diagonal line 125
20. theorem OAI.ContinuumCoulomb.mediatorInverse_highInclusion line 134

    Source documentation

    The full inverse matrix is the actual diagonal high-sector inverse, extended by zero on the singlet sector.

    theorem mediatorInverse_highInclusion (n r : ℕ) (Delta : ℝ) (q : MediatorHighSpace n r) :
        spinMatrixOperator (liftedMediatorInverse n r Delta) (mediatorHighInclusion n r q) =
          mediatorHighInclusion n r (diagonalPenalty
            (fun s => (actualMediatorWeight n r Delta s)⁻¹) q) := by
    …

    Mentions: OAI.ContinuumCoulomb.MediatorHighSpace, OAI.ContinuumCoulomb.spinMatrixOperator, OAI.ContinuumCoulomb.liftedMediatorInverse, OAI.ContinuumCoulomb.mediatorHighInclusion, OAI.ContinuumCoulomb.diagonalPenalty, OAI.ContinuumCoulomb.actualMediatorWeight

21. theorem OAI.ContinuumCoulomb.liftedSource_lowInclusion line 152

    Source documentation

    The original Hamiltonian acts only on the original-spin coordinates.

    theorem liftedSource_lowInclusion (n r : ℕ)
        (C : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ) (p : MediatorLowSpace n) :
        spinMatrixOperator (C ⊗ₖ (1 : Matrix (MediatorBasis r) (MediatorBasis r) ℂ))
            (mediatorLowInclusion n r p) = mediatorLowInclusion n r (spinMatrixOperator C p) := by
    …

    Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.MediatorLowSpace, OAI.ContinuumCoulomb.spinMatrixOperator, OAI.ContinuumCoulomb.MediatorBasis, OAI.ContinuumCoulomb.mediatorLowInclusion