pole_factor_pos_top

formal source

  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
  65  unfold m_pole_from_MS
  66  exact mul_pos h_m_MS_pos (pole_factor_pos_top alpha_s h_alpha_pos h_alpha_lt)
  67
  68/-! ## Inverse direction (MS-bar from pole)
  69
  70To NLO this is just `1 - K_1 (a/π)`; to two-loop one solves the perturbative
  71inverse explicitly. We expose the closed form. -/
  72
  73def inv_pole_factor (alpha_s : ℝ) (N_l : ℕ) : ℝ :=
  74  1 - K_1 * (alpha_s / Real.pi) +
  75  (K_1 ^ 2 - K_2 N_l) * (alpha_s / Real.pi) ^ 2
  76
  77def m_MS_from_pole (m_pole alpha_s : ℝ) (N_l : ℕ) : ℝ :=
  78  m_pole * inv_pole_factor alpha_s N_l
  79