 211    mul_lt_mul h16_lo (le_of_lt hφ_lo) (by norm_num) (le_of_lt hpos16)
 212  linarith [show (3569 : ℝ) < (46.97 : ℝ) * (46.97 : ℝ) * (1.618 : ℝ) from by norm_num]
 213
 214private lemma phi17_lt : Constants.phi ^ (17 : ℕ) < (3574 : ℝ) := by
 215  rw [phi_eq_goldenRatio]
 216  have h8_hi := Numerics.phi_pow8_lt
 217  have hφ_hi := Numerics.phi_lt_16185
 218  have hpos8 : (0 : ℝ) < Real.goldenRatio ^ 8 := by positivity
 219  have hφ_pos : (0 : ℝ) < Real.goldenRatio := by simpa using Real.goldenRatio_pos
 220  have heq : Real.goldenRatio ^ 17 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio := by ring_nf
 221  rw [heq]
 222  have h16_hi : Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 < (46.99 : ℝ) * (46.99 : ℝ) :=
 223    mul_lt_mul h8_hi (le_of_lt h8_hi) hpos8 (by norm_num)
 224  have h17_hi : Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio <
 225      (46.99 : ℝ) * (46.99 : ℝ) * (1.6185 : ℝ) :=
 226    mul_lt_mul h16_hi (le_of_lt hφ_hi) hφ_pos (by norm_num)
 227  linarith [show (46.99 : ℝ) * (46.99 : ℝ) * (1.6185 : ℝ) < (3574 : ℝ) from by norm_num]
 228
 229theorem muon_ratio_undershoot :
 230    Constants.phi ^ (11 : ℕ) < ratio_mu_e_exp := by
 231  linarith [phi11_lt, ratio_mu_e_exp_bounds.1]
 232
 233theorem tau_ratio_overshoot :
 234    ratio_tau_e_exp < Constants.phi ^ (17 : ℕ) := by
 235  linarith [phi17_gt, ratio_tau_e_exp_bounds.2]
 236
 237theorem muon_electron_ratio_error :
 238    |Constants.phi ^ (11 : ℕ) - ratio_mu_e_exp| / ratio_mu_e_exp < 0.04 := by
 239  have hr := ratio_mu_e_exp_bounds
 240  have hexp_pos : (0 : ℝ) < ratio_mu_e_exp := by linarith [hr.1]
 241  rw [div_lt_iff₀ hexp_pos, abs_lt]
 242  constructor <;> nlinarith [phi11_gt, phi11_lt, hr.1, hr.2]
 243
 244theorem tau_electron_ratio_error :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.