add_inv_mono_on_one

formal source

  70/-! ## Helper lemmas -/
  71
  72/-- On `[1,∞)`, `x ↦ x + x⁻¹` is monotone increasing. -/
  73private lemma add_inv_mono_on_one {x y : ℝ} (hx1 : 1 ≤ x) (hxy : x ≤ y) :
  74    x + x⁻¹ ≤ y + y⁻¹ := by
  75  have hxpos : 0 < x := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) hx1
  76  have hypos : 0 < y := lt_of_lt_of_le hxpos hxy
  77  have hxy1 : 1 ≤ x * y := by
  78    nlinarith [hx1, hxy]
  79  have hfac : (y + y⁻¹) - (x + x⁻¹) = (y - x) * (1 - (x * y)⁻¹) := by
  80    field_simp [hxpos.ne', hypos.ne']
  81    ring
  82  have hA : 0 ≤ y - x := sub_nonneg.mpr hxy
  83  have hB : 0 ≤ 1 - (x * y)⁻¹ := by
  84    have hrepr : 1 - (x * y)⁻¹ = ((x * y) - 1) / (x * y) := by
  85      field_simp [hxpos.ne', hypos.ne']
  86    rw [hrepr]
  87    exact div_nonneg (sub_nonneg.mpr hxy1) (le_of_lt (mul_pos hxpos hypos))
  88  have hdiff : 0 ≤ (y + y⁻¹) - (x + x⁻¹) := by
  89    rw [hfac]
  90    exact mul_nonneg hA hB
  91  linarith
  92
  93/-- On `[1,∞)`, `Jcost` is monotone increasing. -/
  94private lemma Jcost_mono_on_one {x y : ℝ} (hx1 : 1 ≤ x) (hxy : x ≤ y) :
  95    Jcost x ≤ Jcost y := by
  96  unfold Jcost
  97  have hsum : x + x⁻¹ ≤ y + y⁻¹ := add_inv_mono_on_one hx1 hxy
  98  linarith
  99
 100/-! ## §1. φ as a Continued Fraction Fixed Point -/
 101
 102/-- φ satisfies x = 1 + 1/x (the continued fraction defining equation). -/
 103theorem phi_continued_fraction_eq : phi = 1 + 1 / phi := by