Revision #2805 → #3276 · back to history
modifiedNewton's method (root-finding algorithm)9a74de0aa035
| Field | From #2805 | To #3276 |
|---|
| note | Mathlib defines the Newton iteration `x ↦ x - P(x)/P'(x)` only for polynomials over a commutative ring, not for arbitrary differentiable real functions. | Mathlib defines the Newton iteration `x ↦ x - P(x)/P'(x)` only for polynomials over a commutative ring (via `Ring.inverse`), not for arbitrary differentiable real functions. |
modifiedTangent-line linear approximation1820464b3a14
| Field | From #2805 | To #3276 |
|---|
| note | Mathlib provides the Fréchet derivative formalism as best linear approximation, but no statement specifically frames it as Newton's tangent-line approximation. | Mathlib's `HasFDerivAt` formalizes the Fréchet derivative as best linear approximation, but nothing specifically frames it as Newton's tangent-line approximation. |
modifiedUndefined iterate for f(x)=x^2-1 at 059c8f6a36f9c
| Field | From #2805 | To #3276 |
|---|
| note | Not formalized in Mathlib (Mathlib's polynomial `newtonMap` uses a junk value when derivative is not a unit). | Not formalized in Mathlib (Mathlib's `Polynomial.newtonMap_apply_of_not_isUnit` uses the junk value `x` when the derivative is not a unit). |
modifiedNewton–Kantorovich theoreme35f11fb6557
| Field | From #2805 | To #3276 |
|---|
| note | The Newton–Kantorovich theorem is not in Mathlib (no `Kantorovich` matches). | The Newton–Kantorovich theorem is not in Mathlib (grep finds no `Kantorovich`). |
modifiedHensel's lemma — p-adic Newton recursion80a73b9f444c
| Field | From #2805 | To #3276 |
|---|
| note | Mathlib formalizes Hensel's lemma over ℤ_p, whose proof is built on Newton-iteration construction. | Mathlib formalizes Hensel's lemma over ℤ_p (`hensels_lemma` in `Mathlib.NumberTheory.Padics.Hensel`), whose proof is built on Newton-iteration construction. |
modifiedHouseholder's methodsa9da70e7de88
| Field | From #2805 | To #3276 |
|---|
| note | Householder's family of higher-order root-finding methods is not formalized in Mathlib (loogle finds no `Householder`). | Householder's family of higher-order root-finding methods is not formalized in Mathlib (grep finds no `Householder`). |
modifiedFréchet derivative9f64ef3e5e4c
| Field | From #2805 | To #3276 |
|---|
| mathlib.module | Mathlib.Analysis.Calculus.FDeriv.Basic | Mathlib.Analysis.Calculus.FDeriv.Defs |
| note | Mathlib defines the Fréchet derivative `fderiv` between normed spaces, matching the usage in the Banach-space formulation of Newton's method. | Mathlib defines the Fréchet derivative as `fderiv 𝕜 f x` (irreducible_def in `Mathlib.Analysis.Calculus.FDeriv.Defs`), matching the Banach-space formulation of Newton's method. |
addedDoubling of correct digits per step8873164e0d68
addedNewton iteration well-defined when f'(x_n) ≠ 08f0d3a55e516
addedBabylonian square-root approximation953f5989cae8
addedHeron's method for square rootsf1b163dd1022
addedAl-Kāshī's iteration for x^P = Nb33d40624a29
addedBasin of attraction59147db913dd
addedFractal boundaries of basins of attractionbe2405269aa9
addedMultivariate Newton via linear system solve869b407af827
addedPositive-definite Hessian implies local minimum0cda91936be2
addedNewton–Raphson iteration for reciprocal x_{n+1} = x_n(2 − a·x_n)1b2c81f92338