alphaInv_pos

formal source

  48/-- CODATA electron anomalous magnetic moment, dimensionless. -/
  49def row_electron_ae_codata : ℝ := 0.00115965218059
  50
  51private theorem alphaInv_pos : 0 < alphaInv := by
  52  linarith [alphaInv_gt]
  53
  54theorem row_electron_ae_leading_eq :
  55    row_electron_ae_leading = 1 / (2 * Real.pi * alphaInv) := by
  56  unfold row_electron_ae_leading alpha
  57  field_simp [ne_of_gt alphaInv_pos, Real.pi_ne_zero]
  58
  59private theorem ae_den_pos : 0 < 2 * Real.pi * alphaInv := by
  60  nlinarith [Real.pi_pos, alphaInv_pos]
  61
  62theorem row_electron_ae_leading_lower :
  63    (0.001161 : ℝ) < row_electron_ae_leading := by
  64  rw [row_electron_ae_leading_eq]
  65  rw [lt_div_iff₀ ae_den_pos]
  66  have hpiUB : (Real.pi : ℝ) < 3.142 := by
  67    linarith [Real.pi_lt_d6, Real.pi_pos]
  68  have h2piUB : (2 : ℝ) * Real.pi < 2 * 3.142 := by
  69    exact mul_lt_mul_of_pos_left hpiUB (by norm_num)
  70  have hden1 : (2 : ℝ) * Real.pi * alphaInv < (2 * 3.142) * alphaInv := by
  71    exact mul_lt_mul_of_pos_right h2piUB alphaInv_pos
  72  have hden2 : (2 * 3.142 : ℝ) * alphaInv < (2 * 3.142) * (137.039 : ℝ) := by
  73    exact mul_lt_mul_of_pos_left alphaInv_lt (by norm_num)
  74  have hnum : (0.001161 : ℝ) * ((2 * 3.142 : ℝ) * (137.039 : ℝ)) < 1 := by
  75    norm_num
  76  have hLpos : (0 : ℝ) < 0.001161 := by norm_num
  77  have hden : (2 : ℝ) * Real.pi * alphaInv < (2 * 3.142 : ℝ) * (137.039 : ℝ) := by
  78    linarith
  79  have hmul : (0.001161 : ℝ) * ((2 : ℝ) * Real.pi * alphaInv) <
  80      (0.001161 : ℝ) * ((2 * 3.142 : ℝ) * (137.039 : ℝ)) := by
  81    exact mul_lt_mul_of_pos_left hden hLpos