OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorSpectrum.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContinuumCoulomb.mediatorFullBottom line 13
2. def OAI.ContinuumCoulomb.sourceMatrixBottom line 18
3. theorem OAI.ContinuumCoulomb.mediatorFullBottom_eq_lowBlockBottom line 22
4. theorem OAI.ContinuumCoulomb.actualMediator_effectiveBottom_matrix line 53
5. theorem OAI.ContinuumCoulomb.sourceMatrixBottom_minimizer line 65
6. theorem OAI.ContinuumCoulomb.sourceMatrixForm_shift line 88
7. theorem OAI.ContinuumCoulomb.sourceMatrixBottom_shift line 101
8. theorem OAI.ContinuumCoulomb.simultaneousMediator_bottom line 120

   Source documentation

   Full simultaneous singlet-mediator spectrum, retaining unreplaced terms C and the exact constant shift. This compares actual variational infima and has only explicit construction norm/calibration hypotheses.

   theorem simultaneousMediator_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 (bellMediatorHamiltonian 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.bellMediatorHamiltonian, OAI.ContinuumCoulomb.signedMediatorMember, OAI.ContinuumCoulomb.sourceMatrixBottom, OAI.ContinuumCoulomb.sourceHeisenbergMatrix