OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorRounding.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Full finite-spin spectral stability under rational approximation of the physical mediator spokes. The infimum ranges over all entangled states.

  1. theorem OAI.ContinuumCoulomb.mediatorRayleigh_abs_le line 13
  2. theorem OAI.ContinuumCoulomb.mediatorRayleigh_boundedBelow line 23
  3. theorem OAI.ContinuumCoulomb.mediatorRayleigh_nonempty line 33
  4. theorem OAI.ContinuumCoulomb.mediatorRayleigh_difference line 40
  5. theorem OAI.ContinuumCoulomb.mediatorFullBottom_lipschitz line 49
  6. theorem OAI.ContinuumCoulomb.spinMatrixOperator_conjugate_norm_le line 70
  7. theorem OAI.ContinuumCoulomb.physicalMediatorEdgeSpoke_operator_norm line 86
  8. theorem OAI.ContinuumCoulomb.physicalTotalMediatorSpokes_operator_norm line 104
  9. theorem OAI.ContinuumCoulomb.physicalTotalMediatorSpokes_sub line 122
  10. theorem OAI.ContinuumCoulomb.physicalRawMediator_bottom_rounding line 135

    Source documentation

    The physical rounded Hamiltonian is compared on the entire tensor space, without a restriction to the singlet kernel.

    theorem physicalRawMediator_bottom_rounding (n r : ℕ) (Delta : ℝ)
    (C : Matrix (SourceSpinBasis n) (SourceSpinBasis n) ℂ)
    (left right : Fin r → Fin n) (member : Fin r → Fin 2) (a b : Fin r → ℝ) :
    |mediatorFullBottom n r (physicalRawMediatorHamiltonian n r Delta C left right member a) -
      mediatorFullBottom n r (physicalRawMediatorHamiltonian n r Delta C left right member b)| ≤
        6 * ∑ e, |a e - b e| := by
…

    Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.mediatorFullBottom, OAI.ContinuumCoulomb.physicalRawMediatorHamiltonian