phi2_eq

formal source

  14
  15noncomputable def tensorToScalarRatio : ℝ := 2 / (45 * phi ^ 2)
  16
  17theorem phi2_eq : phi ^ 2 = phi + 1 := phi_sq_eq
  18
  19theorem r_pos : 0 < tensorToScalarRatio :=
  20  div_pos (by norm_num) (mul_pos (by norm_num) (pow_pos phi_pos 2))
  21
  22theorem r_lt_one : tensorToScalarRatio < 1 := by
  23  unfold tensorToScalarRatio
  24  rw [phi2_eq]
  25  have h1 := phi_gt_onePointSixOne
  26  have hpos : (0:ℝ) < 45 * (phi + 1) := by nlinarith
  27  rw [div_lt_iff₀ hpos]
  28  nlinarith
  29
  30theorem r_band : (0.015 : ℝ) < tensorToScalarRatio ∧ tensorToScalarRatio < 0.020 := by
  31  constructor
  32  · unfold tensorToScalarRatio
  33    rw [phi2_eq]
  34    have h1 := phi_gt_onePointSixOne
  35    have hpos : (0:ℝ) < 45 * (phi + 1) := by nlinarith
  36    have hlt : 45 * (phi + 1) < 45 * 2.63 := by nlinarith [phi_lt_onePointSixTwo]
  37    have hup : 2 / (45 * 2.63) ≤ 2 / (45 * (phi + 1)) := by
  38      apply div_le_div_of_nonneg_left (by norm_num) hpos (by nlinarith)
  39    linarith [show (0.015:ℝ) < 2 / (45 * 2.63) from by norm_num]
  40  · unfold tensorToScalarRatio
  41    rw [phi2_eq]
  42    have h1 := phi_gt_onePointSixOne
  43    have hpos : (0:ℝ) < 45 * (phi + 1) := by nlinarith
  44    have hgt : 45 * (phi + 1) > 45 * 2.59 := by nlinarith
  45    have hlo : 2 / (45 * (phi + 1)) ≤ 2 / (45 * 2.59) := by
  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]