IsLocalMaxOn.fderivWithin_eq_zero
theorem IsLocalMaxOn.fderivWithin_eq_zero :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E} {s : Set E},
IsLocalMaxOn f s a →
∀ {y : E}, y ∈ posTangentConeAt s a → -y ∈ posTangentConeAt s a → (fderivWithin ℝ f s a) y = 0
The theorem `IsLocalMaxOn.fderivWithin_eq_zero` states that if a real-valued function `f` has a local maximum on a set `s` at a point `a`, and both a vector `y` and its negation `-y` belong to the positive tangent cone of the set `s` at the point `a`, then the directional derivative of `f` at the point `a` in the direction of `y` is zero. In other words, if `f` has a local maximum at `a` and `y` is a direction in which `s` is locally flat at `a`, then `f` does not change in the direction of `y` near `a`. This theorem is a fundamental result in calculus and differential geometry, and is commonly used to analyze the behavior of functions near their local maxima.
More concisely: If a real-valued function has a local maximum at a point in a set and the point's positive tangent cone contains the direction vector, then the directional derivative of the function in that direction is zero.
|
IsLocalMin.hasFDerivAt_eq_zero
theorem IsLocalMin.hasFDerivAt_eq_zero :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E} {f' : E →L[ℝ] ℝ},
IsLocalMin f a → HasFDerivAt f f' a → f' = 0
**Fermat's Theorem** states that for a function `f` that maps from a normed additive commutative group `E` (with a normed real number space) to the real numbers, if `f` has a local minimum at a point `a`, and if `f` has a derivative `f'` at this point `a`, then the derivative `f'` at this point `a` is zero. In mathematical terms, if `f` is locally minimized at `a` and `f'(a)` exists, then `f'(a) = 0`. This is a fundamental result of calculus that characterizes critical points of functions.
More concisely: If a real-valued function `f` on a normed additive commutative group `E` has a local minimum at `a` and a derivate `f'` at `a`, then `f'(a) = 0`.
|
IsLocalMax.fderiv_eq_zero
theorem IsLocalMax.fderiv_eq_zero :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E},
IsLocalMax f a → fderiv ℝ f a = 0
**Fermat's Theorem**: This theorem states that for a given function `f`, which maps from a type `E` (representing a normed additive commutative group with a normed space over the real numbers) to the real numbers, if there exists a local maximum at a point `a` in `E` (as denoted by `IsLocalMax f a`), then the derivative of the function `f` at the point `a` (represented by `fderiv ℝ f a`) is equal to zero. In mathematical terms, if `f(x)` has a local maximum at `x=a`, then `f'(a) = 0`, where `f'(a)` is the derivative of `f` at `a`.
More concisely: If `f : E → ℝ` has a local maximum at `a ∈ E` in the normed additive commutative group `E` over the real numbers, then `f'(a) = 0`.
|
IsLocalMax.deriv_eq_zero
theorem IsLocalMax.deriv_eq_zero : ∀ {f : ℝ → ℝ} {a : ℝ}, IsLocalMax f a → deriv f a = 0
**Fermat's Theorem**: The theorem states that for any real-valued function `f` and a real number `a`, if `a` is a local maximum of the function `f`, then the derivative of `f` at the point `a` equals zero. In other words, at the peak of a local maximum, the slope of the function `f` becomes flat. This theorem is a fundamental result in calculus and plays a crucial role in the analysis of the critical points of functions.
More concisely: If `f` is a real-valued function and `a` is a local maximum, then `df/da (a) = 0`.
|
IsLocalMaxOn.hasFDerivWithinAt_eq_zero
theorem IsLocalMaxOn.hasFDerivWithinAt_eq_zero :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E} {f' : E →L[ℝ] ℝ}
{s : Set E},
IsLocalMaxOn f s a →
HasFDerivWithinAt f f' s a → ∀ {y : E}, y ∈ posTangentConeAt s a → -y ∈ posTangentConeAt s a → f' y = 0
This theorem states that if a function `f`, from a normed additively commutative group `E` (with a normed space structure over real numbers) to real numbers, has a local maximum at a point `a` within a set `s`, and `f'` is a derivative of `f` at `a` within the set `s`. If both a vector `y` and its negation `-y` are in the positive tangent cone of the set `s` at the point `a`, then the derivative `f'` of the function `f` at the vector `y` equals zero.
In simpler terms, it says that at a local maximum point of a function, if a direction and its opposite are both directions of non-decreasing, then the derivative of the function in that direction is zero.
More concisely: If a differentiable real-valued function on a normed additively commutative group has a local maximum at a point with both the vector and its negation in the positive tangent cone, then the derivative of the function in that direction is zero.
|
IsLocalExtr.hasFDerivAt_eq_zero
theorem IsLocalExtr.hasFDerivAt_eq_zero :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E} {f' : E →L[ℝ] ℝ},
IsLocalExtr f a → HasFDerivAt f f' a → f' = 0
**Fermat's Theorem**: This theorem states that for any function `f` mapping from a normed additive commutative group `E` into real numbers `ℝ`, if `f` has a local extremum at a point `a` in `E` and the function `f` has a derivative `f'` at the point `a`, then the derivative `f'` at the point `a` is zero. In other words, if a function has a local maximum or minimum at a point, then its derivative at that point is zero. This is a formal statement of Fermat's theorem in calculus.
More concisely: If a real-valued function `f` defined on a normed additive commutative group `E` has a local extremum at a point `a` where it is differentiable, then its derivative `f'` at `a` is zero.
|
IsLocalMinOn.fderivWithin_eq_zero
theorem IsLocalMinOn.fderivWithin_eq_zero :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E} {s : Set E},
IsLocalMinOn f s a →
∀ {y : E}, y ∈ posTangentConeAt s a → -y ∈ posTangentConeAt s a → (fderivWithin ℝ f s a) y = 0
The theorem `IsLocalMinOn.fderivWithin_eq_zero` states that for a function `f`, a point `a`, and a set `s`, if `f` has a local minimum on `s` at `a` and both a vector `y` and its negative `-y` belong to the positive tangent cone of `s` at `a`, then the derivative of `f` at `a` (within `s`) in the direction of `y` is `0`. This essentially means that if `f` is at a local minimum and `y` is a direction such that moving both ways along `y` stays within `s`, then `f` is not changing in the direction of `y`.
More concisely: If a function `f` has a local minimum at `a` in the set `s` and `y` is a vector in the positive tangent cone of `s` at `a`, then the derivative of `f` at `a` in the direction of `y` is equal to 0.
|
IsLocalExtr.hasDerivAt_eq_zero
theorem IsLocalExtr.hasDerivAt_eq_zero : ∀ {f : ℝ → ℝ} {f' a : ℝ}, IsLocalExtr f a → HasDerivAt f f' a → f' = 0 := by
sorry
**Fermat's Theorem**: This theorem states that if a function `f` from the real numbers to the real numbers has a local extremum at a point `a`, and if the function `f` has a derivative `f'` at this same point `a`, then the value of the derivative `f'` at the point of local extremum is zero. Remember, a local extremum is a point where the function takes a minimum or maximum value within some neighborhood of that point. This theorem is a mathematical formalization of the intuitive concept that at the top of a hill (a local maximum) or the bottom of a valley (a local minimum), the slope of the hill or valley is horizontally flat, i.e., has zero slope.
More concisely: If `f` is a real-valued function with a local extremum at `a` and `f'` exists at `a`, then `f'(a) = 0`.
|
IsLocalMin.hasDerivAt_eq_zero
theorem IsLocalMin.hasDerivAt_eq_zero : ∀ {f : ℝ → ℝ} {f' a : ℝ}, IsLocalMin f a → HasDerivAt f f' a → f' = 0 := by
sorry
**Fermat's Theorem**: This theorem states that for any real-valued function `f`, real numbers `f'` and `a`, if `a` is a local minimum of the function `f` (that is, `f(a)` is less than or equal to `f(x)` for all `x` in some neighborhood of `a`), and if the derivative of the function `f` at the point `a` exists and is equal to `f'`, then the derivative `f'` must be zero. In other words, the slope of the tangent line to the function `f` at a local minimum is zero.
More concisely: If `f` is a real-valued function with local minimum `a` where the derivative `f'` exists, then `f'(a) = 0`.
|
IsLocalMaxOn.fderivWithin_nonpos
theorem IsLocalMaxOn.fderivWithin_nonpos :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E} {s : Set E},
IsLocalMaxOn f s a → ∀ {y : E}, y ∈ posTangentConeAt s a → (fderivWithin ℝ f s a) y ≤ 0
The theorem `IsLocalMaxOn.fderivWithin_nonpos` states that if a function `f` has a local maximum at a point `a` within a set `s`, and if a vector `y` is in the positive tangent cone of `s` at `a`, then the directional derivative of the function `f` at the point `a` in the direction of `y`, calculated within the set `s`, is less than or equal to zero. This is a generalization of the fact that the derivative of a function at a local maximum is zero, to the case where the domain of the function is a subset of a normed vector space and the derivative is replaced by a directional derivative.
More concisely: If a function has a local maximum at a point within a set, and the vector is in the positive tangent cone of that point in the set, then the directional derivative of the function at that point in the direction of the vector is less than or equal to zero.
|
IsLocalExtr.fderiv_eq_zero
theorem IsLocalExtr.fderiv_eq_zero :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E},
IsLocalExtr f a → fderiv ℝ f a = 0
**Fermat's Theorem**: The theorem states that for any function `f` from a normed additive commutative group `E` to real numbers, if there's a local extremum at a point `a` in `E` (which means the function `f` has a local minimum or a maximum at `a`), then the derivative of `f` at this point `a`, computed via `fderiv ℝ f a`, equals zero. This theorem is a key result in calculus, encapsulating a fundamental characteristic of local extrema.
More concisely: If `f` is a real-valued function on a normed additive commutative group `E` and has a local extremum at `a` in `E`, then `f'(a) = 0`, where `f'` denotes the derivative of `f`.
|
IsLocalExtr.deriv_eq_zero
theorem IsLocalExtr.deriv_eq_zero : ∀ {f : ℝ → ℝ} {a : ℝ}, IsLocalExtr f a → deriv f a = 0
**Fermat's Theorem**: For any real-valued function `f` and any real number `a`, if `a` is a local extremum of function `f` (that is, `f(a)` is either a local minimum or maximum), then the derivative of `f` at the point `a` is equal to zero. This implies that at the points of local extrema, the rate of change of the function is zero.
More concisely: If `f` is a real-valued function and `a` is a local extrema point, then `f'.(a) = 0`. (The derivative of a real-valued function `f` at a point `a` is equal to zero.)
|
IsLocalMax.hasFDerivAt_eq_zero
theorem IsLocalMax.hasFDerivAt_eq_zero :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E} {f' : E →L[ℝ] ℝ},
IsLocalMax f a → HasFDerivAt f f' a → f' = 0
**Fermat's Theorem**: This theorem states that for any function `f` mapping from a normed additive commutative group `E` (with real numbers as the scalar field) to real numbers, if `f` has a local maximum at a point `a` and if the function `f` has a derivative `f'` at the point `a`, then the derivative `f'` at the point `a` is zero. In mathematical terms, this can be written as if $f'(a)$ exists and $a$ is a local maximum, then $f'(a) = 0$.
More concisely: If a real-valued function `f` on a normed additive commutative group `E` has a local maximum at `a` and a derivative `f'` at `a`, then `f'(a)` equals zero.
|
IsLocalMin.deriv_eq_zero
theorem IsLocalMin.deriv_eq_zero : ∀ {f : ℝ → ℝ} {a : ℝ}, IsLocalMin f a → deriv f a = 0
**Fermat's Theorem**: This theorem states that for a real-valued function `f` defined on the real numbers, if there exists a local minimum at a point `a`, then the derivative of `f` at point `a` is zero. In other words, if the value of `f` at `a` is less than or equal to the values of `f` at nearby points, then the rate of change of `f` at `a` is zero. This result is a key principle in calculus and optimization.
More concisely: If `f` is a real-valued function with a local minimum at `a`, then `f'(a) = 0`.
|
IsLocalMin.fderiv_eq_zero
theorem IsLocalMin.fderiv_eq_zero :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E},
IsLocalMin f a → fderiv ℝ f a = 0
**Fermat's Theorem**: This theorem states that for any real-valued function `f` with a local minimum at a point `a` in a normed additive commutative group `E` over the real numbers, the derivative of the function `f` at the point `a` is equal to zero. This is one of the key results in calculus that help us understand the behavior of functions at their extremal points.
More concisely: If `f` is a real-valued function with a local minimum at `a` in a normed additive commutative group `E` over the real numbers, then `df/da = 0`.
|
IsLocalMax.hasDerivAt_eq_zero
theorem IsLocalMax.hasDerivAt_eq_zero : ∀ {f : ℝ → ℝ} {f' a : ℝ}, IsLocalMax f a → HasDerivAt f f' a → f' = 0 := by
sorry
**Fermat's Theorem**: This theorem states that if a function `f` has a local maximum at a point `a`, then the derivative of `f` at `a` is equal to zero. In other words, for any real-valued function `f`, if `f` has a local maximum at `a` (i.e., `f(x) ≤ f(a)` for all `x` in a neighborhood of `a`), and if `f` has a derivative `f'` at `a` (in the sense that `f(x') = f(x) + (x' - x) * f' + o(x' - x)` for `x'` converging to `x`), then `f'` must be `0`.
More concisely: If `f` is a real-valued function with a local maximum at `a` and is differentiable at `a`, then `f'(a) = 0`.
|
IsLocalMaxOn.hasFDerivWithinAt_nonpos
theorem IsLocalMaxOn.hasFDerivWithinAt_nonpos :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E} {f' : E →L[ℝ] ℝ}
{s : Set E}, IsLocalMaxOn f s a → HasFDerivWithinAt f f' s a → ∀ {y : E}, y ∈ posTangentConeAt s a → f' y ≤ 0
The theorem `IsLocalMaxOn.hasFDerivWithinAt_nonpos` states that if a real-valued function `f` has a local maximum at a point `a` within a set `s`, and `f'` is the derivative of `f` with respect to `a` within `s`, then for any point `y` that belongs to the positive tangent cone of `s` at `a`, the derivative of `f` at `y` is less than or equal to zero. In other words, if `f` reaches a local peak at `a`, then any direction within `s` that is in the positive tangent cone at `a` leads to a decrease in `f` or at least, `f` does not increase in those directions. This theorem is a part of the theory of local extrema in analysis and is applicable in a normed add-commutative group `E` that is a normed space over the reals.
More concisely: If a real-valued function `f` has a local maximum at `a` within a set `s`, then for any `y` in the positive tangent cone of `s` at `a`, `f'(y)` is less than or equal to 0.
|
IsLocalMinOn.hasFDerivWithinAt_nonneg
theorem IsLocalMinOn.hasFDerivWithinAt_nonneg :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E} {f' : E →L[ℝ] ℝ}
{s : Set E}, IsLocalMinOn f s a → HasFDerivWithinAt f f' s a → ∀ {y : E}, y ∈ posTangentConeAt s a → 0 ≤ f' y
The theorem `IsLocalMinOn.hasFDerivWithinAt_nonneg` states that for a function `f` from a normed additive commutative group `E` to real numbers, if `f` has a local minimum on a set `s` at a point `a`, and `f'` is the derivative of `f` at `a` within `s`, then for any `y` that belongs to the positive tangent cone of `s` at `a`, the derivative `f'` at `y` is greater than or equal to zero. In simple terms, this theorem tells us that at a local minimum of a function, the derivative in the direction of any point in the positive tangent cone is non-negative.
More concisely: If a function has a local minimum at a point in a normed additive commutative group, then its derivative in the positive tangent cone at that point is non-negative.
|
IsLocalMinOn.fderivWithin_nonneg
theorem IsLocalMinOn.fderivWithin_nonneg :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E} {s : Set E},
IsLocalMinOn f s a → ∀ {y : E}, y ∈ posTangentConeAt s a → 0 ≤ (fderivWithin ℝ f s a) y
The theorem `IsLocalMinOn.fderivWithin_nonneg` states that if a function `f` has a local minimum at a point `a` within a set `s`, and if a vector `y` belongs to the positive tangent cone of `s` at `a`, then the directional derivative of `f` at `a` in the direction of `y` is nonnegative. This is to say, moving along the direction `y` from point `a` does not decrease the value of the function `f`, which is expected as `a` is a local minimum within the set `s`.
More concisely: If a function has a local minimum at a point in a set and the directional derivative in the positive tangent cone direction is non-negative at that point, then the function does not decrease in that direction.
|
IsLocalMinOn.hasFDerivWithinAt_eq_zero
theorem IsLocalMinOn.hasFDerivWithinAt_eq_zero :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {a : E} {f' : E →L[ℝ] ℝ}
{s : Set E},
IsLocalMinOn f s a →
HasFDerivWithinAt f f' s a → ∀ {y : E}, y ∈ posTangentConeAt s a → -y ∈ posTangentConeAt s a → f' y = 0
This theorem states that if a function `f` has a local minimum within a set `s` at a point `a`, and `f'` is a derivative of `f` at `a` within `s`, then for any element `y` that both belongs to and has its negation in the positive tangent cone of `s` at `a`, the value of `f'` at `y` is zero. In simpler words, if we have a function that reaches a local minimum at a certain point, and we have a direction in which both the direction and its opposite are 'uphill' from this point, then the derivative of the function in that direction is zero. This is a mathematical condition expressing a certain symmetry property of the function at points where it reaches a local minimum.
More concisely: If a differentiable function `f` has a local minimum at `a` in the set `s`, then the derivative `f'` evaluates to zero at any point `y` in the positive tangent cone of `s` at `a`.
|