alpha_match

formal source

  46
  47/-- Matching factor for alpha_s at threshold (NLO accuracy).
  48    Returns alpha_s^(n) given alpha_s^(n+1) at the threshold scale. -/
  49def alpha_match (alpha_above : ℝ) : ℝ :=
  50  alpha_above * (1 + c_2_alpha * (alpha_above / Real.pi) ^ 2)
  51
  52/-- Matching factor for the mass at threshold (NLO accuracy).
  53    Returns m^(n) given m^(n+1) at the threshold scale. -/
  54def mass_match (mass_above alpha_at_threshold : ℝ) : ℝ :=
  55  mass_above * (1 + d_2_mass * (alpha_at_threshold / Real.pi) ^ 2)
  56
  57/-! ## Positivity of matching factors
  58
  59For the small alpha values that occur at the heavy-quark thresholds
  60(alpha_s(m_b) ~ 0.22, alpha_s(m_c) ~ 0.38), the corrections are at the
  61percent level and never threaten positivity. We prove this conditionally
  62on the input being positive and the alpha being below 1 (perturbative). -/
  63
  64theorem alpha_match_pos (alpha_above : ℝ)
  65    (h_pos : 0 < alpha_above) (h_lt : alpha_above < 1) :
  66    0 < alpha_match alpha_above := by
  67  unfold alpha_match
  68  apply mul_pos h_pos
  69  have h_a_over_pi_pos : 0 < alpha_above / Real.pi :=
  70    div_pos h_pos Real.pi_pos
  71  have h_a_over_pi_sq_pos : 0 < (alpha_above / Real.pi) ^ 2 :=
  72    pow_pos h_a_over_pi_pos 2
  73  have h_c_pos : 0 < c_2_alpha := by unfold c_2_alpha; norm_num
  74  positivity
  75
  76theorem mass_match_pos (mass_above alpha_at_threshold : ℝ)
  77    (h_mass_pos : 0 < mass_above) (h_alpha_pos : 0 < alpha_at_threshold)
  78    (h_alpha_small : alpha_at_threshold < 1) :
  79    0 < mass_match mass_above alpha_at_threshold := by