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]

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

Instances For
    @[reducible]

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

    Instances For

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

      Instances For

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

        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.

          Instances For
            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).

            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.

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

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

            Binet's formula as a function equality.

            theorem Real.coe_fib_eq (n : ) :

            Binet's formula as a dependent equality.