  46      apply div_le_div_of_nonneg_left (by norm_num) (by nlinarith) (by nlinarith)
  47    linarith [show (2 : ℝ) / (45 * 2.59) < 0.020 from by norm_num]
  48
  49structure TensorRatioCert where
  50  r_pos : 0 < tensorToScalarRatio
  51  r_band : (0.015 : ℝ) < tensorToScalarRatio ∧ tensorToScalarRatio < 0.020
  52
  53noncomputable def tensorRatioCert : TensorRatioCert where
  54  r_pos := r_pos
  55  r_band := r_band
  56
  57end IndisputableMonolith.Cosmology.TensorToScalarRatioFromRS

papers checked against this theorem

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