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.

@[reducible, inline]

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

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

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

    Equations
    Instances For

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

      Equations
      Instances For

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

        Equations
        Instances For

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

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

          @[simp]

          Irrationality #

          The golden ratio is irrational.

          The conjugate of the golden ratio is irrational.

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

          The recurrence relation satisfied by the Fibonacci sequence.

          Equations
          • fibRec = { order := 2, coeffs := ![1, 1] }
          Instances For
            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).

            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.

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

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

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

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

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

            Binet's formula as a function equality.

            theorem Real.coe_fib_eq (n : ) :

            Binet's formula as a dependent equality.

            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 -

            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 -