selfSimilarityDefect

formal source

  21noncomputable section
  22
  23/-- Self-similarity defect ratio for a geometric cascade. -/
  24def selfSimilarityDefect (r : ℝ) : ℝ :=
  25  r ^ 2 / (r + 1)
  26
  27/-- Simplified cascade cost: the J-cost of the self-similarity defect. -/
  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