70structure RunningCoupling where 71 /-- The coupling value at scale μ (in GeV). -/ 72 at_scale : ℝ → ℝ 73 /-- The coupling is positive in the perturbative regime. -/ 74 positive_in_pert : ∀ μ, μ > 1 → at_scale μ > 0 75 /-- Asymptotic freedom: coupling decreases at high scale (for QCD). -/ 76 asymp_free : ∀ μ₁ μ₂, μ₁ < μ₂ → μ₂ > 100 → at_scale μ₂ < at_scale μ₁ 77 78/-- The mass anomalous dimension γ_m(μ). 79 In general, this is a function of the scale and the fermion species. 80 It encodes how the running mass changes with μ. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.