Revision #1899 → #3388 · back to history
modifiedGradient (informal)bc18bd92cc37
| Field | From #1899 | To #3388 |
|---|
| note | `gradient f x` is the Mathlib definition of the gradient of a scalar-valued differentiable function on a Hilbert space. | `gradient f x := (InnerProductSpace.toDual 𝕜 F).symm (fderiv 𝕜 f x)` is Mathlib's gradient of a scalar-valued differentiable function on a Hilbert space. |
modifiedDirection of fastest increase6ba656b983d8
| Field | From #1899 | To #3388 |
|---|
| note | No `steepest`/`fastest` ascent characterization of the gradient is stated in Mathlib's `Gradient` API. | No steepest/fastest-ascent characterization of the gradient is stated in Mathlib's Gradient API. |
modifiedStationary point870b9f03f2ce
| Field | From #1899 | To #3388 |
|---|
| note | Mathlib has no `IsCritical`/`StationaryPt`/`CriticalPt` definition for zeros of the gradient. | Mathlib has no `StationaryPt`/`CriticalPt` definition for zeros of the gradient. |
modifiedGradient via partial derivativesb97d9c0f3ff8
| Field | From #1899 | To #3388 |
|---|
| mathlib.match_kind | — | generalization |
| provenance | ai | ai-moderated |
modifiedLinear approximation via gradient8fffc70978fe
| Field | From #1899 | To #3388 |
|---|
| note | `hasGradientAt_iff_isLittleO` states `f x' = f x + ⟪f', x' - x⟫ + o(x' - x)`, the gradient linear approximation. | `hasGradientAt_iff_isLittleO` states `f x' - f x - ⟪f', x' - x⟫ = o(x' - x)`, the gradient linear-approximation identity. |
modifiedGradient is steepest ascent direction996bd94a379e
| Field | From #1899 | To #3388 |
|---|
| note | No `steepest`/`fastest` ascent theorem about the gradient is present in Mathlib. | No steepest/fastest-ascent theorem about the gradient is present in Mathlib. |
modifiedGradient on Riemannian manifoldcd2153cd50f3
| Field | From #1899 | To #3388 |
|---|
| note | Mathlib's Riemannian-manifold development (`Mathlib.Geometry.Manifold.Riemannian.*`) does not yet contain a gradient definition for smooth scalar functions. | Mathlib's Riemannian-manifold development does not yet contain a gradient definition for smooth scalar functions. |
addedDirectional derivative (definition used)3474740343de
addedCauchy–Schwarz bound on directional derivative814b544b8836