Revision #2150 → #2831 · back to history
modifiedRecurrence relation (informal)d13be601f487
| Field | From #2150 | To #2831 |
|---|
| note | Mathlib has no general recurrence-relation definition; only the linear case is formalized as `LinearRecurrence`. | Mathlib has no general recurrence-relation definition; only the linear constant-coefficient case is formalized as `LinearRecurrence`. |
modifiedOrder of a recurrence relation82c18607b853
| Field | From #2150 | To #2831 |
|---|
| note | The order is captured as a field of `LinearRecurrence`, but only for linear recurrences. | The order is captured as a field of `LinearRecurrence`; no general recurrence-order definition exists. |
modifiedLinear recurrence4d294e92c93f
| Field | From #2150 | To #2831 |
|---|
| note | `LinearRecurrence` formalizes linear recurrences (with constant coefficients) over a commutative semiring. | `LinearRecurrence` formalizes only the constant-coefficient case; variable-coefficient linear recurrences (e.g. polynomial coefficients) are not covered. |
| provenance | ai | ai-moderated |
| status | formalized | partial |
modifiedLinear recurrence with constant coefficientsa70883c5c8cb
| Field | From #2150 | To #2831 |
|---|
| note | `LinearRecurrence` is exactly the structure of a linear recurrence with constant coefficients. | `LinearRecurrence` is exactly the structure of a linear recurrence with constant coefficients (order + coefficient vector). |
modifiedSolving a recurrence relation2a051bd20e53
| Field | From #2150 | To #2831 |
|---|
| note | `mkSol` produces the unique solution from initial data inductively, but closed-form solutions are not formalized (see file docstring). | `mkSol` produces the unique solution from initial data inductively for linear recurrences, but closed-form solutions are not formalized. |
modifiedRecurrence relation (formal definition)2ac3dca8e0e8
| Field | From #2150 | To #2831 |
|---|
| label | First-order recurrence relation | Recurrence relation (formal definition) |
| note | Only linear first-order recurrences are covered (as `LinearRecurrence` with order = 1); general first-order recurrences are not defined. | Only linear recurrences are formalized (as `LinearRecurrence`); general recurrences defined by an arbitrary function of preceding terms are not defined in Mathlib. |
| provenance | ai | ai-moderated |
addedFirst-order recurrence relation7690d0a27851
addedInitial value of a recurrence856272295044
modifiedFactorial recurrencef62d6e99873b
| Field | From #2150 | To #2831 |
|---|
| note | `Nat.factorial` is defined by the recurrence and `factorial_succ` states `(n+1)! = (n+1) * n!`. | `Nat.factorial` is defined by the recurrence and `Nat.factorial_succ` states `(n+1)! = (n+1) * n!`. |
addedBinet's formula for Fibonacci numbers93dbddd241df
modifiedClosed-form formula for binomial coefficients0d45dbbf5e0d
| Field | From #2150 | To #2831 |
|---|
| note | `Nat.choose_eq_factorial_div_factorial` gives the closed-form `n.choose k = n! / (k! * (n-k)!)` (for `k ≤ n`). | `Nat.choose_eq_factorial_div_factorial` gives the closed-form `n.choose k = n! / (k! * (n-k)!)` for `k ≤ n`. |
modifiedSecond difference2654bb1357d4
| Field | From #2150 | To #2831 |
|---|
| note | The second difference is obtained by iterating `fwdDiff` twice (`fwdDiff h^[2]`); no dedicated name exists. | The second difference is obtained by iterating `fwdDiff` twice (`(fwdDiff h)^[2]`); no dedicated name exists. |
modifiedk-th differenceb96666c533ab
| Field | From #2150 | To #2831 |
|---|
| note | The k-th difference appears as `Function.iterate (fwdDiff h) k` (e.g. in `fwdDiff_iter_eq_sum_shift`) but is not separately defined. | The k-th difference appears as `Function.iterate (fwdDiff h) k` in lemmas but is not separately defined. |
modifiedCharacteristic equation of a linear recurrence12766bcdfecb
| Field | From #2150 | To #2831 |
|---|
| note | `LinearRecurrence.charPoly` defines the characteristic polynomial of a linear recurrence; its roots are the eigenvalues referenced in the stability criterion. | `LinearRecurrence.charPoly` defines the characteristic polynomial of a linear recurrence, whose roots are the characteristic roots. |