lambdaRS

formal source

  21open Constants
  22
  23/-- Λ_RS = 8φ⁵/45. -/
  24noncomputable def lambdaRS : ℝ := 8 * phi ^ 5 / 45
  25
  26/-- φ⁵ = 5φ + 3. -/
  27theorem phi5_eq : phi ^ 5 = 5 * phi + 3 := by
  28  have h2 := phi_sq_eq
  29  have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
  30  have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
  31  nlinarith
  32
  33/-- Λ_RS ∈ (1.88, 2.03). -/
  34theorem lambdaRS_band :
  35    (1.88 : ℝ) < lambdaRS ∧ lambdaRS < 2.03 := by
  36  unfold lambdaRS
  37  have h5 : phi ^ 5 = 5 * phi + 3 := phi5_eq
  38  have h1 := phi_gt_onePointSixOne
  39  have h2 := phi_lt_onePointSixTwo
  40  constructor
  41  · have : 8 * phi ^ 5 / 45 > 8 * (5 * 1.61 + 3) / 45 := by
  42      apply div_lt_div_of_pos_right _ (by norm_num)
  43      nlinarith
  44    linarith
  45  · have : 8 * phi ^ 5 / 45 < 8 * (5 * 1.62 + 3) / 45 := by
  46      apply div_lt_div_of_pos_right _ (by norm_num)
  47      nlinarith
  48    linarith
  49
  50/-- Λ_RS > 0. -/
  51theorem lambdaRS_pos : 0 < lambdaRS := by
  52  unfold lambdaRS
  53  apply div_pos _ (by norm_num)
  54  apply mul_pos (by norm_num)