Documentation

Mathlib.Data.Real.GoldenRatio

The golden ratio and its conjugate #

This file defines the golden ratio φ := (1 + √5)/2 and its conjugate ψ := (1 - √5)/2, which are the two real roots of X² - X - 1.

Along with various computational facts about them, we prove their irrationality, and we link them to the Fibonacci sequence by proving Binet's formula.

source
@[reducible, inline]
abbrev goldenRatio :
ℝ

The golden ratio φ := (1 + √5)/2.

Equations
    Instances For
      source
      @[reducible, inline]
      abbrev goldenConj :
      ℝ

      The conjugate of the golden ratio ψ := (1 - √5)/2.

      Equations
        Instances For
          source
          def goldenRatio.termφ :
          Lean.ParserDescr

          The golden ratio φ := (1 + √5)/2.

          Equations
            Instances For
              source
              def goldenRatio.termψ :
              Lean.ParserDescr

              The conjugate of the golden ratio ψ := (1 - √5)/2.

              Equations
                Instances For
                  source
                  theorem inv_gold :
                  goldenRatio⁻¹ = -goldenConj

                  The inverse of the golden ratio is the opposite of its conjugate.

                  source
                  theorem inv_goldConj :
                  goldenConj⁻¹ = -goldenRatio

                  The opposite of the golden ratio is the inverse of its conjugate.

                  source
                  @[simp]
                  theorem gold_mul_goldConj :
                  goldenRatio * goldenConj = -1
                  source
                  @[simp]
                  theorem goldConj_mul_gold :
                  goldenConj * goldenRatio = -1
                  source
                  @[simp]
                  theorem gold_add_goldConj :
                  goldenRatio + goldenConj = 1
                  source
                  theorem one_sub_goldConj :
                  1 - goldenRatio = goldenConj
                  source
                  theorem one_sub_gold :
                  1 - goldenConj = goldenRatio
                  source
                  @[simp]
                  theorem gold_sub_goldConj :
                  goldenRatio - goldenConj = √5
                  source
                  theorem gold_pow_sub_gold_pow (n : ℕ) :
                  goldenRatio ^ (n + 2) - goldenRatio ^ (n + 1) = goldenRatio ^ n
                  source
                  @[simp]
                  theorem gold_sq :
                  goldenRatio ^ 2 = goldenRatio + 1
                  source
                  @[simp]
                  theorem goldConj_sq :
                  goldenConj ^ 2 = goldenConj + 1
                  source
                  theorem gold_pos :
                  0 < goldenRatio
                  source
                  theorem gold_ne_zero :
                  goldenRatio ≠ 0
                  source
                  theorem one_lt_gold :
                  1 < goldenRatio
                  source
                  theorem gold_lt_two :
                  goldenRatio < 2
                  source
                  theorem goldConj_neg :
                  goldenConj < 0
                  source
                  theorem goldConj_ne_zero :
                  goldenConj ≠ 0
                  source
                  theorem neg_one_lt_goldConj :
                  -1 < goldenConj

                  Irrationality #

                  source
                  theorem gold_irrational :
                  Irrational goldenRatio

                  The golden ratio is irrational.

                  source
                  theorem goldConj_irrational :
                  Irrational goldenConj

                  The conjugate of the golden ratio is irrational.

                  source
                  def fibRec {α : Type u_1} [CommSemiring α] :
                  LinearRecurrence α

                  The recurrence relation satisfied by the Fibonacci sequence.

                  Equations
                    Instances For
                      source
                      theorem fibRec_charPoly_eq {β : Type u_2} [CommRing β] :
                      fibRec.charPoly = Polynomial.X ^ 2 - (Polynomial.X + 1)

                      The characteristic polynomial of fibRec is X² - (X + 1).

                      source
                      theorem fib_isSol_fibRec {α : Type u_1} [CommSemiring α] :
                      fibRec.IsSolution fun (x : ℕ) => ↑(Nat.fib x)

                      As expected, the Fibonacci sequence is a solution of fibRec.

                      source
                      theorem geom_gold_isSol_fibRec :
                      fibRec.IsSolution fun (x : ℕ) => goldenRatio ^ x

                      The geometric sequence fun n ↦ φ^n is a solution of fibRec.

                      source
                      theorem geom_goldConj_isSol_fibRec :
                      fibRec.IsSolution fun (x : ℕ) => goldenConj ^ x

                      The geometric sequence fun n ↦ ψ^n is a solution of fibRec.

                      source
                      theorem Real.coe_fib_eq' :
                      (fun (n : ℕ) => ↑(Nat.fib n)) = fun (n : ℕ) => (goldenRatio ^ n - goldenConj ^ n) / √5

                      Binet's formula as a function equality.

                      source
                      theorem Real.coe_fib_eq (n : ℕ) :
                      ↑(Nat.fib n) = (goldenRatio ^ n - goldenConj ^ n) / √5

                      Binet's formula as a dependent equality.

                      source
                      theorem fib_golden_conj_exp (n : ℕ) :
                      ↑(Nat.fib (n + 1)) - goldenRatio * ↑(Nat.fib n) = goldenConj ^ n

                      Relationship between the Fibonacci Sequence, Golden Ratio and its conjugate's exponents

                      source
                      theorem fib_golden_exp' (n : ℕ) :
                      goldenRatio * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = goldenRatio ^ (n + 1)

                      Relationship between the Fibonacci Sequence, Golden Ratio and its exponents