pith. machine review for the scientific record. sign in
def definition def or abbrev

alpha_s_two_loop

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  70def alpha_s_two_loop (alpha_0 : ℝ) (N_f : ℕ) (mu_GeV mu_0_GeV : ℝ) : ℝ :=

proof body

Definition body.

  71  let L := Real.log (mu_GeV ^ 2 / mu_0_GeV ^ 2)
  72  let denom := 1 + b0 N_f * alpha_0 * L +
  73               (b1 N_f / b0 N_f) * alpha_0 *
  74               Real.log (1 + b0 N_f * alpha_0 * L)
  75  alpha_0 / denom
  76
  77/-- The two-loop denominator collapses to the one-loop denominator when the
  78    `b1`-induced correction term vanishes. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.