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.
The golden ratio φ := (1 + √5)/2
.
Equations
- Real.goldenRatio = (1 + √5) / 2
Instances For
The conjugate of the golden ratio ψ := (1 - √5)/2
.
Equations
- Real.goldenConj = (1 - √5) / 2
Instances For
The golden ratio φ := (1 + √5)/2
.
Equations
- goldenRatio.termφ = Lean.ParserDescr.node `goldenRatio.termφ 1024 (Lean.ParserDescr.symbol "φ")
Instances For
The conjugate of the golden ratio ψ := (1 - √5)/2
.
Equations
- goldenRatio.termψ = Lean.ParserDescr.node `goldenRatio.termψ 1024 (Lean.ParserDescr.symbol "ψ")
Instances For
The inverse of the golden ratio is the opposite of its conjugate.
Alias of Real.inv_goldenRatio
.
The inverse of the golden ratio is the opposite of its conjugate.
The opposite of the golden ratio is the inverse of its conjugate.
Alias of Real.inv_goldenConj
.
The opposite of the golden ratio is the inverse of its conjugate.
Alias of Real.goldenRatio_mul_goldenConj
.
Alias of Real.goldenConj_mul_goldenRatio
.
Alias of Real.goldenRatio_add_goldenConj
.
Alias of Real.one_sub_goldenConj
.
Alias of Real.one_sub_goldenRatio
.
Alias of Real.goldenRatio_sub_goldenConj
.
Alias of Real.goldenRatio_pow_sub_goldenRatio_pow
.
Alias of Real.goldenRatio_sq
.
Alias of Real.goldenConj_sq
.
Alias of Real.goldenRatio_pos
.
Alias of Real.goldenRatio_ne_zero
.
Alias of Real.one_lt_goldenRatio
.
Alias of Real.goldenRatio_lt_two
.
Alias of Real.goldenConj_neg
.
Alias of Real.goldenConj_ne_zero
.
Alias of Real.neg_one_lt_goldenConj
.
Irrationality #
Alias of Real.goldenRatio_irrational
.
The golden ratio is irrational.
The conjugate of the golden ratio is irrational.
Alias of Real.goldenConj_irrational
.
The conjugate of the golden ratio is irrational.
Links with Fibonacci sequence #
The recurrence relation satisfied by the Fibonacci sequence.
Instances For
The characteristic polynomial of fibRec
is X² - (X + 1)
.
As expected, the Fibonacci sequence is a solution of fibRec
.
The geometric sequence fun n ↦ φ^n
is a solution of fibRec
.
Alias of Real.geom_goldenRatio_isSol_fibRec
.
The geometric sequence fun n ↦ φ^n
is a solution of fibRec
.
The geometric sequence fun n ↦ ψ^n
is a solution of fibRec
.
Alias of Real.geom_goldenConj_isSol_fibRec
.
The geometric sequence fun n ↦ ψ^n
is a solution of fibRec
.
Binet's formula as a function equality.
Binet's formula as a dependent equality.
Relationship between the Fibonacci Sequence, Golden Ratio and its conjugate's exponents
Alias of Real.fib_succ_sub_goldenRatio_mul_fib
.
Relationship between the Fibonacci Sequence, Golden Ratio and its conjugate's exponents
Relationship between the Fibonacci Sequence, Golden Ratio and its exponents
Alias of Real.goldenRatio_mul_fib_succ_add_fib
.
Relationship between the Fibonacci Sequence, Golden Ratio and its exponents