K_2

formal source

  31def K_1 : ℝ := 4 / 3
  32
  33/-- Two-loop pole-to-MS-bar coefficient (canonical N_l = 5 for top quark). -/
  34def K_2 (N_l : ℕ) : ℝ := 11.1 - 1.04 * (N_l : ℝ)
  35
  36/-- The two-loop pole-to-MS-bar conversion factor.
  37
  38    `pole_factor alpha_s N_l = 1 + (4/3)(a/π) + K_2 (a/π)^2`
  39-/
  40def pole_factor (alpha_s : ℝ) (N_l : ℕ) : ℝ :=
  41  1 + K_1 * (alpha_s / Real.pi) + K_2 N_l * (alpha_s / Real.pi) ^ 2
  42
  43/-- Convert MS-bar mass at its own scale to pole mass. -/
  44def m_pole_from_MS (m_MS alpha_s : ℝ) (N_l : ℕ) : ℝ :=
  45  m_MS * pole_factor alpha_s N_l
  46
  47/-! ## Positivity (in the perturbative regime) -/
  48
  49theorem pole_factor_pos_top (alpha_s : ℝ)
  50    (h_alpha_pos : 0 < alpha_s) (h_alpha_lt : alpha_s < 0.5) :
  51    0 < pole_factor alpha_s 5 := by
  52  unfold pole_factor K_1 K_2
  53  have h_a_pos : 0 < alpha_s / Real.pi := div_pos h_alpha_pos Real.pi_pos
  54  have h_a_sq_pos : 0 < (alpha_s / Real.pi) ^ 2 := pow_pos h_a_pos 2
  55  have h_K2_at5_pos : 0 < (11.1 - 1.04 * (5 : ℝ)) := by norm_num
  56  -- 1 + positive + positive > 0 trivially
  57  have h1 : 0 < 1 + (4 / 3) * (alpha_s / Real.pi) := by
  58    have : 0 < (4 / 3) * (alpha_s / Real.pi) := mul_pos (by norm_num) h_a_pos
  59    linarith
  60  nlinarith [h_K2_at5_pos, h_a_sq_pos]
  61
  62theorem m_pole_from_MS_pos_top (m_MS alpha_s : ℝ)
  63    (h_m_MS_pos : 0 < m_MS) (h_alpha_pos : 0 < alpha_s) (h_alpha_lt : alpha_s < 0.5) :
  64    0 < m_pole_from_MS m_MS alpha_s 5 := by