OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorBlocks.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Concrete low and high blocks for simultaneous singlet mediators. The nonzero original-spin block is retained throughout.

  1. abbrev OAI.ContinuumCoulomb.MediatorLowSpace line 14
  2. abbrev OAI.ContinuumCoulomb.MediatorHighSpace line 15
  3. abbrev OAI.ContinuumCoulomb.MediatorFullSpace line 16
  4. def OAI.ContinuumCoulomb.mediatorLowIndex line 18
  5. def OAI.ContinuumCoulomb.mediatorHighIndex line 21
  6. theorem OAI.ContinuumCoulomb.mediatorLowIndex_injective line 24
  7. theorem OAI.ContinuumCoulomb.mediatorHighIndex_injective line 28
  8. def OAI.ContinuumCoulomb.mediatorLowInclusion line 35
  9. def OAI.ContinuumCoulomb.mediatorLowRestriction line 38
  10. def OAI.ContinuumCoulomb.mediatorHighInclusion line 41
  11. def OAI.ContinuumCoulomb.mediatorHighRestriction line 44
  12. theorem OAI.ContinuumCoulomb.mediatorLowInclusion_norm line 47
  13. theorem OAI.ContinuumCoulomb.mediatorHighInclusion_norm line 50
  14. theorem OAI.ContinuumCoulomb.mediatorLowRestriction_norm line 53
  15. theorem OAI.ContinuumCoulomb.mediatorHighRestriction_norm line 56
  16. def OAI.ContinuumCoulomb.actualMediatorWeight line 59
  17. theorem OAI.ContinuumCoulomb.actualMediator_inverse_data line 62
  18. def OAI.ContinuumCoulomb.actualMediatorLowBlock line 77
  19. def OAI.ContinuumCoulomb.actualMediatorCoupling line 83
  20. def OAI.ContinuumCoulomb.actualMediatorHighBlock line 90
  21. theorem OAI.ContinuumCoulomb.actualMediatorLowBlock_norm line 98
  22. theorem OAI.ContinuumCoulomb.actualMediatorCoupling_norm line 106
  23. theorem OAI.ContinuumCoulomb.spinMatrixOperator_add_norm_bound line 115
  24. theorem OAI.ContinuumCoulomb.liftedMediatorPerturbation_norm line 124
  25. theorem OAI.ContinuumCoulomb.actualMediatorHighBlock_norm line 133
  26. theorem OAI.ContinuumCoulomb.actualMediator_second_order line 146

    Source documentation

    A supporting block estimate for the actual simultaneous mediator construction, retaining the unreplaced low Hamiltonian C.

    theorem actualMediator_second_order (n r : ℕ) {Delta : ℝ} (hDelta : 0 < Delta)
    (C : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ)
    (left right : Fin r → Fin n) (member : Fin r → Fin 2) (amplitude : Fin r → ℝ)
    {epsilon : ℝ} (hepsilon : 0 ≤ epsilon) (hsmall : epsilon ≤ 1 / 4)
    (hbound : ‖spinMatrixOperator (C ⊗ₖ (1 : Matrix (MediatorBasis r) (MediatorBasis r) ℂ))‖ +
      6 * ∑ e, |amplitude e| ≤ epsilon * (4 * Delta)) :
    |Perturbation.lowBlockBottom (actualMediatorLowBlock n r C)
        (diagonalPenalty (actualMediatorWeight n r Delta))
        (actualMediatorHighBlock n r C left right member amplitude)
        (actualMediatorCoupling n r left right member amplitude) -
      Perturbation.effectiveBottom (actualMediatorLowBlock n r C)
        (diagonalPenalty (fun s => (actualMediatorWeight n r Delta s)⁻¹))
…

    Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.spinMatrixOperator, OAI.ContinuumCoulomb.MediatorBasis, OAI.ContinuumCoulomb.Perturbation.lowBlockBottom, OAI.ContinuumCoulomb.actualMediatorLowBlock, OAI.ContinuumCoulomb.diagonalPenalty, OAI.ContinuumCoulomb.actualMediatorWeight, OAI.ContinuumCoulomb.actualMediatorHighBlock, OAI.ContinuumCoulomb.actualMediatorCoupling, OAI.ContinuumCoulomb.Perturbation.effectiveBottom