Revision #1217 → #2187 · back to history
modifiedFibonacci recurrence relationcebad57fd60f
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Definition","snippet":"The Fibonacci numbers may be defined by the recurrence relation"},{"type":"math_alttext","value":"{\\displaystyle F_{0}=0,\\quad F_{1}=1,}"},{"type":"math_alttext","value":"{\\displaystyle F_{n}=F_{n-1}+F_{n-2}}"}] | — |
modifiedNegative-index extension26c221e1fdf5
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Definition","snippet":"The Fibonacci sequence can be extended to negative integer indices by following the same recurrence relation in the negative direction"},{"type":"math_alttext","value":"{\\displaystyle F_{-n}=(-1)^{n+1}F_{n}.}"}] | — |
| note | `Int.fib` extends `Nat.fib` to all integers and `Int.fib_add_two` verifies the recurrence continues to hold. | `Int.fib` extends `Nat.fib` to all integers and `Int.fib_add_two` (same module) verifies the recurrence continues to hold. |
modifiedFibonacci by rounding7b06141bedbf
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Computation by rounding","snippet":"the number F n is the closest integer to"},{"type":"math_alttext","value":"{\\displaystyle F_{n}=\\left\\lfloor {\\frac {\\varphi ^{n}}{\\sqrt {5}}}\\right\\rceil ,\\ n\\geq 0.}"}] | — |
modifiedFloor-function index formulaee45c892fb84
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Computation by rounding","snippet":"Instead using the floor function gives the largest index of a Fibonacci number that is not greater than F"},{"type":"math_alttext","value":"{\\displaystyle n_{\\mathrm {largest} }(F)=\\left\\lfloor \\log _{\\varphi }{\\sqrt {5}}(F+1/2)\\right\\rfloor ,\\ F\\geq 0,}"}] | — |
addedAsymptotic growth of F_n3df78f8ae402
modifiedConvergence of consecutive ratios to golden ratiodb43f7d80292
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Limit of consecutive quotients","snippet":"the ratio of consecutive Fibonacci numbers converges"},{"type":"math_alttext","value":"{\\displaystyle \\lim _{n\\to \\infty }{\\frac {F_{n+1}}{F_{n}}}=\\varphi .}"}] | — |
modifiedDecomposition of powers of phie90302fc3db8
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Decomposition of powers","snippet":"The resulting recurrence relationships yield Fibonacci numbers as the linear coefficients"},{"type":"math_alttext","value":"{\\displaystyle \\varphi ^{n}=F_{n}\\varphi +F_{n-1}.}"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\varphi ^{n+1}&=(F_{n}\\varphi +F_{n-1})\\varphi =F_{n}\\varphi ^{2}+F_{n-1}\\varphi \\\\&=F_{n}(\\varphi +1)+F_{n-1}\\varphi =(F_{n}+F_{n-1})\\varphi +F_{n}=F_{n+1}\\varphi +F_{n}.\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle \\psi ^{n}=F_{n}\\psi +F_{n-1}.}"}] | — |
| note | `goldenRatio_mul_fib_succ_add_fib` proves `φ^(n+1) = φ · fib(n+1) + fib n`, expressing powers of φ as linear combinations with Fibonacci coefficients. | `Real.goldenRatio_mul_fib_succ_add_fib` proves `φ^(n+1) = φ · fib(n+1) + fib n`, expressing powers of φ as linear combinations with Fibonacci coefficients. |
modifiedCassini's identity (via determinant)08d19ee84aca
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Matrix form","snippet":"Taking the determinant of both sides of this equation yields Cassini's identity"},{"type":"math_alttext","value":"{\\displaystyle (-1)^{n}=F_{n+1}F_{n-1}-{F_{n}}^{2}.}"}] | — |
modifiedSum of first n Fibonacci numbersb6b82f4b9a60
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Combinatorial proofs","snippet":"the sum of the first Fibonacci numbers up to the n -th is equal to the ( n + 2) -th Fibonacci number minus 1"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{i=1}^{n}F_{i}=F_{n+2}-1}"}] | — |
modifiedSums by odd/even indexbae34135b10c
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Combinatorial proofs","snippet":"the sum of the first Fibonacci numbers with odd index up to"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{i=0}^{n-1}F_{2i+1}=F_{2n}}"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{i=1}^{n}F_{2i}=F_{2n+1}-1.}"}] | — |
modifiedSum of squares identity724a14aacdff
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Combinatorial proofs","snippet":"the sum of the squares of the first Fibonacci numbers up to"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{i=1}^{n}F_{i}^{2}=F_{n}F_{n+1}}"}] | — |
modifiedCassini's identity1014cfc12462
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Cassini's and Catalan's identities","snippet":"Cassini's identity states that"},{"type":"math_alttext","value":"{\\displaystyle F_{n}^{2}-F_{n+1}F_{n-1}=(-1)^{n-1}}"},{"type":"math_alttext","value":"{\\displaystyle F_{n}^{2}-F_{n+r}F_{n-r}=(-1)^{n-r}F_{r}^{2}}"}] | — |
modifiedCatalan's identity1f2a061fd975
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Cassini's and Catalan's identities","snippet":"Catalan's identity is a generalization"},{"type":"math_alttext","value":"{\\displaystyle F_{n}^{2}-F_{n+1}F_{n-1}=(-1)^{n-1}}"},{"type":"math_alttext","value":"{\\displaystyle F_{n}^{2}-F_{n+r}F_{n-r}=(-1)^{n-r}F_{r}^{2}}"}] | — |
modifiedd'Ocagne's identityff7056a7ad99
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"d'Ocagne's identity","snippet":"where L n is the n -th Lucas number"},{"type":"math_alttext","value":"{\\displaystyle F_{m}F_{n+1}-F_{m+1}F_{n}=(-1)^{n}F_{m-n}}"},{"type":"math_alttext","value":"{\\displaystyle F_{2n}=F_{n+1}^{2}-F_{n-1}^{2}=F_{n}\\left(F_{n+1}+F_{n-1}\\right)=F_{n}L_{n}}"},{"type":"math_alttext","value":"{\\displaystyle F_{3n}=2F_{n}^{3}+3F_{n}F_{n+1}F_{n-1}=5F_{n}^{3}+3(-1)^{n}F_{n}}"}] | — |
modifiedExponential generating function30b7f4cacaae
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Exponential","snippet":"The exponential generating function of the Fibonacci sequence may also be derived from the recurrence relation"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\sum _{k=0}^{\\infty }F_{k+2}{\\frac {x^{k}}{k!}}={}&\\sum _{k=0}^{\\infty }F_{k+1}{\\frac {x^{k}}{k!}}+\\sum _{k=0}^{\\infty }F_{k}{\\frac {x^{k}}{k!}}\\\\F^{\\prime \\prime }(x)={}&F^{\\prime }(x)+F(x)\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle F(x)={\\frac {e^{\\varphi x}-e^{\\psi x}}{\\sqrt {5}}}}"},{"type":"math_alttext","value":"{\\displaystyle F^{(n)}(0)=F_{n}={\\frac {\\varphi ^{n}-\\psi ^{n}}{\\sqrt {5}}}}"}] | — |
modifiedSum of odd-indexed reciprocals4ac8dc420017
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Reciprocal sums","snippet":"the sum of every odd-indexed reciprocal Fibonacci number can be written as"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=1}^{\\infty }{\\frac {1}{F_{2k-1}}}={\\frac {\\sqrt {5}}{4}}\\;\\vartheta _{2}\\!\\left(0,{\\frac {3-{\\sqrt {5}}}{2}}\\right)^{2},}"}] | — |
modifiedSum of squared reciprocalsc8e5d9d28941
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Reciprocal sums","snippet":"the sum of squared reciprocal Fibonacci numbers as"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=1}^{\\infty }{\\frac {1}{{F_{k}}^{2}}}={\\frac {5}{24}}\\!\\left(\\vartheta _{2}\\!\\left(0,{\\frac {3-{\\sqrt {5}}}{2}}\\right)^{4}-\\vartheta _{4}\\!\\left(0,{\\frac {3-{\\sqrt {5}}}{2}}\\right)^{4}+1\\right).}"}] | — |
modifiedSum of even-indexed reciprocals30a4113f15f4
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Reciprocal sums","snippet":"The sum of all even-indexed reciprocal Fibonacci numbers is"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=1}^{\\infty }{\\frac {1}{F_{2k}}}={\\sqrt {5}}\\left(L(\\psi ^{2})-L(\\psi ^{4})\\right)}"}] | — |
modifiedMillin's series31a4b29e2d1d
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Reciprocal sums","snippet":"Millin's series gives the identity"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=0}^{\\infty }{\\frac {1}{F_{2^{k}}}}={\\frac {7-{\\sqrt {5}}}{2}},}"},{"type":"math_alttext","value":"{\\displaystyle \\sum _{k=0}^{N}{\\frac {1}{F_{2^{k}}}}=3-{\\frac {F_{2^{N}-1}}{F_{2^{N}}}}.}"}] | — |
modifiedGCD divisibility property791ae0e75950
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Divisibility properties","snippet":"the Fibonacci sequence satisfies the stronger divisibility property"},{"type":"math_alttext","value":"{\\displaystyle \\gcd(F_{a},F_{b},F_{c},\\ldots )=F_{\\gcd(a,b,c,\\ldots )}\\,}"}] | — |
modifiedConsecutive Fibonacci numbers are coprime9ad3c0a50f3f
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Divisibility properties","snippet":"any three consecutive Fibonacci numbers are pairwise coprime"},{"type":"math_alttext","value":"{\\displaystyle \\gcd(F_{n},F_{n+1})=\\gcd(F_{n},F_{n+2})=\\gcd(F_{n+1},F_{n+2})=1}"}] | — |
modifiedFibonacci pseudoprimee2bdf3cb2738
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Primality testing","snippet":"If n is composite and satisfies the formula, then n is a Fibonacci pseudoprime"},{"type":"math_alttext","value":"{\\displaystyle n\\mid F_{n\\,-~\\!\\left({\\frac {5}{n}}\\right)},}"}] | — |
addedLucas numbersb3db1447c44e
addedPell numbers971ed297673b
addedFibonacci polynomials383df1848633
addedk-bonacci numbersf2988b891a71
modifiedFibonacci in Pascal's triangle5670c2018c5f
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Mathematics","snippet":"The Fibonacci numbers occur as the sums of binomial coefficients in the \"shallow\" diagonals of Pascal's triangle"},{"type":"math_alttext","value":"{\\displaystyle F_{n}=\\sum _{k=0}^{\\left\\lfloor {\\frac {n-1}{2}}\\right\\rfloor }{\\binom {n-k-1}{k}}.}"},{"type":"math_alttext","value":"{\\displaystyle {\\frac {x}{1-x-x^{2}}}=x+x^{2}(1+x)+x^{3}(1+x)^{2}+\\dots +x^{k+1}(1+x)^{k}+\\dots =\\sum \\limits _{n=0}^{\\infty }F_{n}x^{n}}"}] | — |
modifiedPythagorean triples from Fibonacci0463b744dda9
| Field | From #1217 | To #2187 |
|---|
| anchors | [{"section":"Mathematics","snippet":"every second Fibonacci number is the length of the hypotenuse of a right triangle with integer sides"},{"type":"math_alttext","value":"{\\displaystyle (F_{n}F_{n+3})^{2}+(2F_{n+1}F_{n+2})^{2}={F_{2n+3}}^{2}.}"}] | — |
modifiedWorst case of Euclid's algorithmcb59bcc51567
| Field | From #1217 | To #2187 |
|---|
| mathlib.decl | GenContFract.fib_le_of_continuantsAux_b | GenContFract.fib_le_of_contsAux_b |
| note | Mathlib bounds continued-fraction denominators below by `Nat.fib`, which underlies the worst-case analysis, but does not explicitly state the Lamé worst-case theorem for the Euclidean algorithm. | Mathlib bounds continued-fraction denominators below by `Nat.fib` (via `GenContFract.fib_le_of_contsAux_b`), which underlies the worst-case analysis, but does not explicitly state the Lamé worst-case theorem for the Euclidean algorithm. |