# 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
theorem inv_gold :

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

theorem inv_goldConj :

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

@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem gold_sq :
@[simp]
theorem goldConj_sq :
=
theorem gold_pos :

## Irrationality #

theorem gold_irrational :

The golden ratio is irrational.

The conjugate of the golden ratio is irrational.

def fibRec {α : Type u_1} [] :

The recurrence relation satisfied by the Fibonacci sequence.

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

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

theorem fib_isSol_fibRec {α : Type u_1} [] :
LinearRecurrence.IsSolution fibRec fun 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 => ↑()) = fun n => ( - ) /

Binet's formula as a function equality.

theorem Real.coe_fib_eq (n : ) :
↑() = ( - ) /

Binet's formula as a dependent equality.