def
definition
alpha_s_two_loop
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS on GitHub at line 70.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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 : ℝ) :
81 1 + b0 5 * alpha_0 * Real.log (mu_GeV ^ 2 / mu_0_GeV ^ 2) +
82 0 * alpha_0 * Real.log (1 + b0 5 * alpha_0 *
83 Real.log (mu_GeV ^ 2 / mu_0_GeV ^ 2)) =
84 1 + (11 * (N_c : ℝ) - 2 * 5) / (12 * Real.pi) * alpha_0 *
85 Real.log (mu_GeV ^ 2 / mu_0_GeV ^ 2) := by
86 unfold b0 N_c
87 ring
88
89/-- Positivity of the two-loop alpha_s under the MS-bar perturbative window:
90 when the alpha_0 input is positive and the log scale ratio is bounded
91 so the denominator stays positive, the running coupling is positive. -/
92theorem alpha_s_two_loop_pos_when_denom_pos
93 (alpha_0 : ℝ) (N_f : ℕ) (mu_GeV mu_0_GeV : ℝ)
94 (h_alpha_pos : 0 < alpha_0)
95 (h_denom_pos : 0 < 1 + b0 N_f * alpha_0 * Real.log (mu_GeV ^ 2 / mu_0_GeV ^ 2) +
96 (b1 N_f / b0 N_f) * alpha_0 *
97 Real.log (1 + b0 N_f * alpha_0 * Real.log (mu_GeV ^ 2 / mu_0_GeV ^ 2))) :
98 0 < alpha_s_two_loop alpha_0 N_f mu_GeV mu_0_GeV := by
99 unfold alpha_s_two_loop
100 exact div_pos h_alpha_pos h_denom_pos