inv_pole_factor

formal source

  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
  80/-- The inverse expression is positive for small enough alpha_s. The product
  81    `pole_factor * inv_pole_factor` agrees with 1 to two-loop accuracy
  82    (i.e., differs only by terms of order `alpha_s^3` or higher), but we do
  83    not state that algebraic identity explicitly here; it is straightforward
  84    algebra and not used in the downstream scorecards. -/
  85theorem inv_pole_factor_at_zero (N_l : ℕ) :
  86    inv_pole_factor 0 N_l = 1 := by
  87  unfold inv_pole_factor
  88  simp
  89
  90/-! ## Master cert -/
  91
  92structure PoleToMSbarCert where
  93  K_1_eq : K_1 = 4 / 3
  94  K_2_at5_pos : 0 < K_2 5
  95  pole_factor_pos_lemma : ∀ alpha_s : ℝ,
  96      0 < alpha_s → alpha_s < 0.5 → 0 < pole_factor alpha_s 5
  97  m_pole_pos_lemma : ∀ m_MS alpha_s : ℝ,
  98      0 < m_MS → 0 < alpha_s → alpha_s < 0.5 →
  99      0 < m_pole_from_MS m_MS alpha_s 5
 100
 101theorem K_2_at5_pos : 0 < K_2 5 := by unfold K_2; norm_num
 102
 103theorem poleToMSbarCert_holds : PoleToMSbarCert :=