OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorOffsets.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact scalar offsets relating the shifted mediator penalty to the physical Hamiltonian containing only the specified Heisenberg bonds.

  1. theorem OAI.ContinuumCoulomb.mediatorLocal_add line 13
  2. theorem OAI.ContinuumCoulomb.mediatorLocal_smul line 18
  3. theorem OAI.ContinuumCoulomb.physicalMediatorPenalty_offset line 24
  4. def OAI.ContinuumCoulomb.physicalRawMediatorHamiltonian line 38
  5. theorem OAI.ContinuumCoulomb.physicalMediatorHamiltonian_offset line 46
  6. theorem OAI.ContinuumCoulomb.mediatorFullForm_add_scalar line 57
  7. theorem OAI.ContinuumCoulomb.mediatorFullBottom_add_scalar line 70
  8. theorem OAI.ContinuumCoulomb.physicalRawSimultaneousMediator_bottom line 108

    Source documentation

    Complete physical signed-to-positive mediator spectrum, with both central-bond and spoke self-energy offsets displayed explicitly.

    theorem physicalRawSimultaneousMediator_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 (physicalRawMediatorHamiltonian n r Delta C left right
        (fun e => signedMediatorMember (J e)) amplitude) + 3 * r * Delta + 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.physicalRawMediatorHamiltonian, OAI.ContinuumCoulomb.signedMediatorMember, OAI.ContinuumCoulomb.sourceMatrixBottom, OAI.ContinuumCoulomb.sourceHeisenbergMatrix

  9. theorem OAI.ContinuumCoulomb.physicalCanonicalMediator_bottom line 127

    Source documentation

    Canonical nonnegative spoke amplitudes, rather than arbitrary choices satisfying only a square calibration.

    theorem physicalCanonicalMediator_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 : Fin r → ℝ)
    {epsilon : ℝ} (hepsilon : 0 ≤ epsilon) (hsmall : epsilon ≤ 1 / 4)
    (hbound : ‖spinMatrixOperator (C ⊗ₖ (1 : Matrix (MediatorBasis r) (MediatorBasis r) ℂ))‖ +
      6 * ∑ e, signedMediatorAmplitude Delta (J e) ≤ epsilon * (4 * Delta)) :
    |mediatorFullBottom n r (physicalRawMediatorHamiltonian n r Delta C left right
        (fun e => signedMediatorMember (J e)) (fun e => signedMediatorAmplitude Delta (J e))) +
        3 * r * Delta + 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.signedMediatorAmplitude, OAI.ContinuumCoulomb.mediatorFullBottom, OAI.ContinuumCoulomb.physicalRawMediatorHamiltonian, OAI.ContinuumCoulomb.signedMediatorMember, OAI.ContinuumCoulomb.sourceMatrixBottom, OAI.ContinuumCoulomb.sourceHeisenbergMatrix