integratedResidue

formal source

 224
 225    This is the abstract definition; the actual computation requires the SM kernels.
 226    We parameterize by an `AnomalousDimension` structure. -/
 227def integratedResidue (γ : AnomalousDimension) (f : Fermion) (lnμ₀ lnμ₁ : ℝ) : ℝ :=
 228  (1 / lambda) * ∫ t in Set.Icc lnμ₀ lnμ₁, γ.gamma f (Real.exp t)
 229
 230/-! ## Connection to Mass Formula -/
 231
 232/-- The running mass at scale μ, given the mass at scale μ₀ and an anomalous dimension.
 233
 234    `m(μ) = m(μ₀) · exp(-∫_{ln μ₀}^{ln μ} γ(μ') d(ln μ'))`
 235
 236    This is the solution to `d(ln m)/d(ln μ) = -γ_m(μ)`. -/
 237def runningMass (γ : AnomalousDimension) (f : Fermion) (m_μ₀ : ℝ) (lnμ₀ lnμ : ℝ) : ℝ :=
 238  m_μ₀ * Real.exp (-(∫ t in Set.Icc lnμ₀ lnμ, γ.gamma f (Real.exp t)))
 239
 240/-- The mass ratio between two scales.
 241
 242    `m(μ₁)/m(μ₀) = exp(-∫_{ln μ₀}^{ln μ₁} γ d(ln μ))` -/
 243theorem mass_ratio_formula (γ : AnomalousDimension) (f : Fermion) (m_μ₀ : ℝ)
 244    (lnμ₀ lnμ₁ : ℝ) (hm : m_μ₀ ≠ 0) :
 245    runningMass γ f m_μ₀ lnμ₀ lnμ₁ / m_μ₀ =
 246      Real.exp (-(∫ t in Set.Icc lnμ₀ lnμ₁, γ.gamma f (Real.exp t))) := by
 247  simp only [runningMass]
 248  field_simp
 249
 250/-! ## Anchor Relation -/
 251
 252/-- The anchor scale from the papers: μ⋆ = 182.201 GeV. -/
 253def muStar : ℝ := 182.201
 254
 255theorem muStar_pos : muStar > 0 := by norm_num [muStar]
 256
 257/-- ln(μ⋆) for use in integral bounds. -/