alphaG_pred_upper

formal source

 166    simpa [mul_assoc, mul_left_comm, mul_comm] using hltNum
 167  simpa [alphaG_pred_closed] using h1
 168
 169theorem alphaG_pred_upper : row_alphaG_pred < (4.85e9 : ℝ) := by
 170  have hφ : phi < (1.6185 : ℝ) := by
 171    simpa [show phi = (Real.goldenRatio : ℝ) from rfl] using phi_lt_16185
 172  have hpiLB : (3.1415 : ℝ) < (Real.pi : ℝ) := by
 173    linarith [Real.pi_gt_d6, Real.pi_pos]
 174  have hN : (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) < (2 : ℝ) ^ (-(44 : ℤ)) * (1.6185 : ℝ) ^ (112 : ℝ) := by
 175    have hr112 : (phi : ℝ) ^ (112 : ℝ) < (1.6185 : ℝ) ^ (112 : ℝ) := by
 176      exact Real.rpow_lt_rpow (by nlinarith [phi_pos, hφ]) hφ (by nlinarith)
 177    nlinarith [hr112, zpow_pos (by norm_num : (0 : ℝ) < (2 : ℝ))]
 178  have h0 :
 179      (2 : ℝ) ^ (-(44 : ℤ)) * (1.6185 : ℝ) ^ (112 : ℝ) < (4.85e9 : ℝ) * (3.1415 : ℝ) := by
 180    nlinarith
 181  have h1 : (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) / Real.pi < (4.85e9 : ℝ) := by
 182    have hltNum : (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) < (4.85e9 : ℝ) * Real.pi := by
 183      nlinarith [h0, hN, hpiLB, Real.pi_pos]
 184    rw [div_lt_iff₀ Real.pi_pos]
 185    simpa [mul_assoc, mul_left_comm, mul_comm] using hltNum
 186  simpa [alphaG_pred_closed] using h1
 187
 188theorem alphaG_pred_bracket : (4.5e9 : ℝ) < row_alphaG_pred ∧ row_alphaG_pred < (4.85e9 : ℝ) :=
 189  ⟨alphaG_pred_lower, alphaG_pred_upper⟩
 190
 191/-! ## CODATA reference (SI units, dimensionless) -/
 192
 193def alphaG_codata : ℝ := 1.7518e-45
 194
 195theorem codata_very_small : alphaG_codata < 1e-40 := by
 196  unfold alphaG_codata; norm_num
 197
 198theorem native_very_not_codata : alphaG_codata < row_alphaG_pred := by
 199  have h1 := alphaG_pred_lower