AnomalousDimension

formal source

  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 μ. -/
  81structure AnomalousDimension where
  82  /-- The anomalous dimension value for fermion f at scale μ. -/
  83  gamma : Fermion → ℝ → ℝ
  84  /-- The anomalous dimension is smooth (differentiable). -/
  85  smooth : ∀ f, Differentiable ℝ (gamma f)
  86  /-- Perturbative bound: |γ| is bounded in the perturbative regime. -/
  87  pert_bounded : ∃ B > 0, ∀ f μ, μ > 1 → |gamma f μ| < B
  88
  89/-! ## RG Transport Integral -/
  90
  91/-- The λ-normalization constant: `λ = ln(φ)`. -/
  92def lambda : ℝ := Real.log phi
  93
  94/-- λ is positive. -/
  95theorem lambda_pos : lambda > 0 := by
  96  have h : 1 < phi := one_lt_phi
  97  exact Real.log_pos h
  98
  99/-! ## Canonical one-loop beta/gamma kernels (Level-B groundwork) -/
 100
 101/-- One-loop QCD beta coefficient in the convention `beta0 = 11 - 2*nf/3`. -/
 102def beta0QCD (nf : ℕ) : ℚ := (11 : ℚ) - (2 : ℚ) * nf / 3
 103
 104/-- Real-valued view of `beta0QCD`. -/
 105def beta0QCDReal (nf : ℕ) : ℝ := (beta0QCD nf : ℝ)
 106
 107/-- One-loop QCD running for `alpha_s`:
 108`d alpha_s / d ln mu = -(beta0/(2*pi)) * alpha_s^2`. -/
 109noncomputable def betaQCD1L (nf : ℕ) (alphaS : ℝ) : ℝ :=
 110  -((beta0QCDReal nf) / (2 * Real.pi)) * alphaS ^ 2
 111