OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorParameters.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Explicit polynomial scales and rational positive spokes for one actual simultaneous singlet-mediator stage. The norm hypothesis concerns the unchanged low-block terms; no spectral conclusion is assumed.

  1. def OAI.ContinuumCoulomb.MediatorParameters.scale line 14
  2. def OAI.ContinuumCoulomb.MediatorParameters.delta line 15
  3. def OAI.ContinuumCoulomb.MediatorParameters.precision line 16
  4. def OAI.ContinuumCoulomb.MediatorParameters.epsilon line 18
  5. theorem OAI.ContinuumCoulomb.MediatorParameters.scale_pos line 20
  6. theorem OAI.ContinuumCoulomb.MediatorParameters.scale_lower line 24
  7. theorem OAI.ContinuumCoulomb.MediatorParameters.epsilon_nonneg line 36
  8. theorem OAI.ContinuumCoulomb.MediatorParameters.epsilon_small line 38
  9. theorem OAI.ContinuumCoulomb.MediatorParameters.second_order_error line 46
  10. theorem OAI.ContinuumCoulomb.MediatorParameters.canonical_amplitude_upper line 56
  11. theorem OAI.ContinuumCoulomb.MediatorParameters.canonical_amplitude_lower line 70
  12. def OAI.ContinuumCoulomb.MediatorParameters.radicand line 89
  13. def OAI.ContinuumCoulomb.MediatorParameters.spoke line 91
  14. theorem OAI.ContinuumCoulomb.MediatorParameters.rational_sqrt_error line 95
  15. theorem OAI.ContinuumCoulomb.MediatorParameters.spoke_error line 105
  16. theorem OAI.ContinuumCoulomb.MediatorParameters.spoke_pos line 114
  17. theorem OAI.ContinuumCoulomb.MediatorParameters.precision_power line 124
  18. theorem OAI.ContinuumCoulomb.MediatorParameters.rounding_error line 137
  19. theorem OAI.ContinuumCoulomb.MediatorParameters.canonical_bottom line 153

    Source documentation

    Explicit parameters discharge the small-perturbation hypotheses of the actual simultaneous-mediator theorem, retaining arbitrary unchanged C.

    theorem canonical_bottom (n r : ℕ) {W G : ℕ} (hW : 0 < W) (hG : 0 < G)
    (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 → ℚ) (hJ : ∀ e, |(J e : ℝ)| ≤ W)
    (hNorm : ‖spinMatrixOperator (C ⊗ₖ (1 : Matrix (MediatorBasis r) (MediatorBasis r) ℂ))‖ ≤ W) :
    |mediatorFullBottom n r (physicalRawMediatorHamiltonian n r (delta r W G) C left right
        (fun e => signedMediatorMember (J e))
        (fun e => signedMediatorAmplitude (delta r W G) (J e))) +
      3 * r * delta r W G + 3 * ∑ e, |(J e : ℝ)| -
        sourceMatrixBottom n (C + ∑ e, (J e : ℂ) • sourceHeisenbergMatrix n (left e) (right e))| ≤
          1 / (1024 * (G : ℝ)) := by
…

    Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.spinMatrixOperator, OAI.ContinuumCoulomb.MediatorBasis, OAI.ContinuumCoulomb.mediatorFullBottom, OAI.ContinuumCoulomb.physicalRawMediatorHamiltonian, OAI.ContinuumCoulomb.MediatorParameters.delta, OAI.ContinuumCoulomb.signedMediatorMember, OAI.ContinuumCoulomb.signedMediatorAmplitude, OAI.ContinuumCoulomb.sourceMatrixBottom, OAI.ContinuumCoulomb.sourceHeisenbergMatrix

  20. theorem OAI.ContinuumCoulomb.MediatorParameters.rational_bottom line 196

    Source documentation

    A concrete positive rational-spoke stage, with a full-spin spectral error bound including the arithmetic approximation of every spoke.

    theorem rational_bottom (n r : ℕ) {W G : ℕ} (hW : 0 < W) (hG : 0 < G)
    (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 → ℚ) (hJ : ∀ e, |(J e : ℝ)| ≤ W)
    (hJlower : ∀ e, 1 / (W : ℝ) ≤ |(J e : ℝ)|)
    (hNorm : ‖spinMatrixOperator (C ⊗ₖ (1 : Matrix (MediatorBasis r) (MediatorBasis r) ℂ))‖ ≤ W) :
    (∀ e, 0 < spoke r W G (J e)) ∧
    |mediatorFullBottom n r (physicalRawMediatorHamiltonian n r (delta r W G) C left right
        (fun e => signedMediatorMember (J e)) (fun e => (spoke r W G (J e) : ℝ))) +
      3 * r * delta r W G + 3 * ∑ e, |(J e : ℝ)| -
        sourceMatrixBottom n (C + ∑ e, (J e : ℂ) • sourceHeisenbergMatrix n (left e) (right e))| ≤
          1 / (512 * (G : ℝ)) := by
…

    Mentions: OAI.ContinuumCoulomb.SourceSpinBasis, OAI.ContinuumCoulomb.spinMatrixOperator, OAI.ContinuumCoulomb.MediatorBasis, OAI.ContinuumCoulomb.MediatorParameters.spoke, OAI.ContinuumCoulomb.mediatorFullBottom, OAI.ContinuumCoulomb.physicalRawMediatorHamiltonian, OAI.ContinuumCoulomb.MediatorParameters.delta, OAI.ContinuumCoulomb.signedMediatorMember, OAI.ContinuumCoulomb.sourceMatrixBottom, OAI.ContinuumCoulomb.sourceHeisenbergMatrix