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]
def goldenRatio :
ℝ

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

Instances For
    source
    @[reducible]
    def goldenConj :
    ℝ

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

    Instances For
      source
      def Real.termφ :
      Lean.ParserDescr

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

      Instances For
        source
        def Real.termψ :
        Lean.ParserDescr

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

        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 = Real.sqrt 5
          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 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.

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

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

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

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

            source
            theorem geom_gold_isSol_fibRec :
            LinearRecurrence.IsSolution fibRec fun x => goldenRatio ^ x

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

            source
            theorem geom_goldConj_isSol_fibRec :
            LinearRecurrence.IsSolution fibRec 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) / Real.sqrt 5

            Binet's formula as a function equality.

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

            Binet's formula as a dependent equality.