alpha_match_pos

formal source

  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
  80  unfold mass_match
  81  apply mul_pos h_mass_pos
  82  -- d_2_mass = -89/432 ≈ -0.206. We bound (a/π)^2 < 1, so the correction is > -1.
  83  have h_d_gt : (-1 : ℝ) < d_2_mass := by unfold d_2_mass; norm_num
  84  have h_d_neg : d_2_mass < 0 := by unfold d_2_mass; norm_num
  85  have h_a_pos : 0 < alpha_at_threshold / Real.pi := div_pos h_alpha_pos Real.pi_pos
  86  have h_a_sq_pos : 0 < (alpha_at_threshold / Real.pi) ^ 2 := pow_pos h_a_pos 2
  87  -- Bound (a/π)^2 < 1: a < 1 and π > 1, so a/π < 1, so (a/π)^2 < 1.
  88  have h_pi_gt_one : (1 : ℝ) < Real.pi := by
  89    linarith [Real.pi_gt_three]
  90  have h_a_over_pi_lt_one : alpha_at_threshold / Real.pi < 1 := by
  91    rw [div_lt_one Real.pi_pos]; linarith
  92  have h_a_sq_lt_one : (alpha_at_threshold / Real.pi) ^ 2 < 1 := by
  93    have : (alpha_at_threshold / Real.pi) ^ 2 < 1 ^ 2 := by
  94      apply sq_lt_sq' <;> nlinarith [h_a_pos]