selfSimilarityDefect_pos

formal source

  28def simplifiedCascadeCost (r : ℝ) : ℝ :=
  29  Jcost (selfSimilarityDefect r)
  30
  31theorem selfSimilarityDefect_pos {r : ℝ} (hr : 1 < r) :
  32    0 < selfSimilarityDefect r := by
  33  unfold selfSimilarityDefect
  34  positivity
  35
  36theorem selfSimilarityDefect_phi : selfSimilarityDefect phi = 1 := by
  37  unfold selfSimilarityDefect
  38  have hphi1 : phi + 1 ≠ 0 := by linarith [phi_pos]
  39  rw [phi_sq_eq]
  40  field_simp [hphi1]
  41
  42theorem simplifiedCascadeCost_phi : simplifiedCascadeCost phi = 0 := by
  43  unfold simplifiedCascadeCost
  44  rw [selfSimilarityDefect_phi]
  45  exact Jcost_one
  46
  47theorem selfSimilarityDefect_eq_one_iff {r : ℝ} (hr : 1 < r) :
  48    selfSimilarityDefect r = 1 ↔ r ^ 2 = r + 1 := by
  49  unfold selfSimilarityDefect
  50  have hr1 : r + 1 ≠ 0 := by linarith
  51  constructor
  52  · intro h
  53    field_simp [hr1] at h
  54    linarith
  55  · intro h
  56    rw [h]
  57    field_simp [hr1]
  58
  59theorem positive_root_unique_above_one {r : ℝ} (hr : 1 < r)
  60    (hroot : r ^ 2 = r + 1) : r = phi := by
  61  have hroot0 : r ^ 2 - r - 1 = 0 := by nlinarith [hroot]