b1

formal source

  47def b0 (N_f : ℕ) : ℝ := (11 * (N_c : ℝ) - 2 * (N_f : ℝ)) / (12 * Real.pi)
  48
  49/-- Two-loop beta coefficient in MS-bar (canonical SU(3) form). -/
  50def b1 (N_f : ℕ) : ℝ :=
  51  (102 - 38 * (N_f : ℝ) / 3) / (8 * Real.pi ^ 2)
  52
  53/-- For N_f <= 8 the two-loop coefficient is positive. -/
  54theorem b1_pos_lowNf (N_f : ℕ) (hNf : N_f ≤ 8) : 0 < b1 N_f := by
  55  unfold b1
  56  apply div_pos _ (by positivity : (0 : ℝ) < 8 * Real.pi ^ 2)
  57  have hNf_real : (N_f : ℝ) ≤ 8 := by exact_mod_cast hNf
  58  linarith
  59
  60/-- At N_f = 5 (canonical between bottom and top thresholds): b1 > 0. -/
  61theorem b1_at_Nf5_pos : 0 < b1 5 := b1_pos_lowNf 5 (by norm_num)
  62
  63/-- One-loop coefficient at N_f = 5 is positive (asymptotic freedom). -/
  64theorem b0_at_Nf5_pos : 0 < b0 5 := by
  65  unfold b0 N_c
  66  apply div_pos _ (by positivity : (0 : ℝ) < 12 * Real.pi)
  67  norm_num
  68
  69/-- The two-loop running closed form. -/
  70def alpha_s_two_loop (alpha_0 : ℝ) (N_f : ℕ) (mu_GeV mu_0_GeV : ℝ) : ℝ :=
  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. -/
  79theorem alpha_s_two_loop_b1_zero_eq_one_loop
  80    (alpha_0 : ℝ) (mu_GeV mu_0_GeV : ℝ) :