IsLocalExtrOn.range_ne_top_of_hasStrictFDerivAt
theorem IsLocalExtrOn.range_ne_top_of_hasStrictFDerivAt :
∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E]
[inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : CompleteSpace F] {f : E → F} {φ : E → ℝ}
{x₀ : E} {f' : E →L[ℝ] F} {φ' : E →L[ℝ] ℝ},
IsLocalExtrOn φ {x | f x = f x₀} x₀ →
HasStrictFDerivAt f f' x₀ → HasStrictFDerivAt φ φ' x₀ → LinearMap.range (f'.prod φ') ≠ ⊤
The theorem `IsLocalExtrOn.range_ne_top_of_hasStrictFDerivAt` can be described as follows:
This is the Lagrange multipliers theorem. It states that if a function `φ : E → ℝ` has a local extremum at a point `x₀` on the set `{x | f x = f x₀}`, where both `f : E → F` and `φ` are strictly differentiable at `x₀`, and the codomain of `f` is a complete space, then the linear map defined by `x ↦ (f' x, φ' x)` is not surjective. In other words, there exists at least one point in the codomain that is not the image of any point in the domain under the linear map. This theorem is a fundamental result in optimization and differential calculus, and is crucial for problems involving constraints.
More concisely: If a strictly differentiable function φ and its derivative function f with respect to some variable x, both defined on a complete space E, have a local extremum at x\_0 such that f(x\_0) is not the image of any point in E under the linear map x ↦ (f' x, φ' x), then the function φ does not attain its local minimum or maximum on the set {x | f x = f x\_0}.
|
IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d
theorem IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt_1d :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {φ : E → ℝ}
{x₀ : E} {φ' : E →L[ℝ] ℝ} {f : E → ℝ} {f' : E →L[ℝ] ℝ},
IsLocalExtrOn φ {x | f x = f x₀} x₀ →
HasStrictFDerivAt f f' x₀ → HasStrictFDerivAt φ φ' x₀ → ∃ a b, (a, b) ≠ 0 ∧ a • f' + b • φ' = 0
This theorem is a version of the Lagrange multipliers theorem. It states that if a function `φ : E → ℝ` has a local extremum at a point `x₀` on the set of points where `f x = f x₀`, and both `f` and `φ` are strictly differentiable at `x₀`, then there exist two real numbers `a` and `b`, not both zero, such that the weighted sum of the derivatives of `f` and `φ` at `x₀` equals zero, with weights `a` and `b` respectively. Here, `E` is a normed add commutative group, also a normed space over the reals and complete. The derivatives of `f` and `φ` are denoted `f'` and `φ'` respectively.
More concisely: If a real-valued function `φ` has a local extremum at `x₀` on the level set of another function `f` (i.e., `f(x₀) = f(x)` for all `x` near `x₀`) under the assumptions of both functions being strictly differentiable at `x₀`, then there exist non-zero scalars `a` and `b` such that the derivatives `f'(x₀)` and `φ'(x₀)` satisfy `a * f'(x₀) + b * φ'(x₀) = ∫01 (df/dt)(t) dt = 0`, where `df/dt` is the derivative of the function `f` along a curve connecting `x₀` to a point on the level set.
|
IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt
theorem IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {φ : E → ℝ}
{x₀ : E} {φ' : E →L[ℝ] ℝ} {ι : Type u_3} [inst_3 : Fintype ι] {f : ι → E → ℝ} {f' : ι → E →L[ℝ] ℝ},
IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀ →
(∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀) →
HasStrictFDerivAt φ φ' x₀ → ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ (Finset.univ.sum fun i => Λ i • f' i) + Λ₀ • φ' = 0
The theorem `IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt` is a one-dimensional version of the Lagrange multipliers theorem. It states that for a finite family of functions `f : ι → E → ℝ`, if another function `φ : E → ℝ` has a local extremum at `x₀` on the set of points `x` where `f i x` equals `f i x₀` for all `i`, and if both `φ` and all functions `f i` are strictly differentiable at `x₀`, then the derivatives `f' i : E → L[ℝ] ℝ` and `φ' : E →L[ℝ] ℝ` are linearly dependent. In other words, there exist real numbers `Λ : ι → ℝ` and `Λ₀ : ℝ`, not both zero, such that the weighted sum over all `i` of `Λ i` times `f' i`, plus `Λ₀` times `φ'`, equals zero. This theorem is a key result in the method of Lagrange multipliers, which is a strategy for finding the local maxima and minima of a function subject to equality constraints.
More concisely: If a finite family of strictly differentiable real-valued functions `f i` on a real vector space `E` has a local extremum `x₀` where they all equal a constant, then the derivatives of the functions and the derivative of a real-valued function `φ` having a local extremum at `x₀` on the same set are linearly dependent.
|
IsLocalExtrOn.linear_dependent_of_hasStrictFDerivAt
theorem IsLocalExtrOn.linear_dependent_of_hasStrictFDerivAt :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {φ : E → ℝ}
{x₀ : E} {φ' : E →L[ℝ] ℝ} {ι : Type u_3} [inst_3 : Finite ι] {f : ι → E → ℝ} {f' : ι → E →L[ℝ] ℝ},
IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀ →
(∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀) →
HasStrictFDerivAt φ φ' x₀ → ¬LinearIndependent ℝ (Option.elim' φ' f')
This is the Lagrange multipliers theorem. It applies to a function `φ : E → ℝ` that has a local extremum at a point `x₀` on the set `{x | ∀ i, f i x = f i x₀}`, where `f : ι → E → ℝ` is a finite family of functions. The theorem assumes that function `φ` and all functions `f i` are strictly differentiable at `x₀`. The theorem then concludes that the derivatives `f' i : E → L[ℝ] ℝ` of each function in the family `f` and the derivative `φ' : E →L[ℝ] ℝ` of function `φ` are not linearly independent over ℝ. In other words, they are linearly dependent. The function `Option.elim' φ' f'` is used to combine the derivative of `φ` and the derivatives of `f i` into a single family of vectors for the purpose of checking linear independence.
More concisely: The Lagrange multipliers theorem states that at a local extremum of a strictly differentiable function φ on a constrained set {x | ∀ i, f i(x) = f i(x₀)}, the derivatives of φ and the constraint functions f i are linearly dependent.
|
IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt
theorem IsLocalExtrOn.exists_linear_map_of_hasStrictFDerivAt :
∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E]
[inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : CompleteSpace F] {f : E → F} {φ : E → ℝ}
{x₀ : E} {f' : E →L[ℝ] F} {φ' : E →L[ℝ] ℝ},
IsLocalExtrOn φ {x | f x = f x₀} x₀ →
HasStrictFDerivAt f f' x₀ →
HasStrictFDerivAt φ φ' x₀ → ∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
The Lagrange multipliers theorem states that if a function `φ : E → ℝ` has a local extremum at `x₀` on the set of points where another function `f : E → F` equals `f x₀`, and both `f` and `φ` are strictly differentiable at `x₀`, and the codomain of `f` is a complete space. Then there exist two real number vectors `Λ : dual ℝ F` and `Λ₀ : ℝ` such that `(Λ, Λ₀) ≠ 0` and for all `x`, their linear combination `Λ (f' x) + Λ₀ • φ' x` equals zero. The theorem asserts the existence of these multiplier vectors under the given conditions.
More concisely: Given a strictly differentiable real-valued function `φ` with a local extremum at `x₀` on the set where another function `f` equals `f(x₀)`, and `f` and `φ` have codomains in a complete space, there exist non-zero multiplier vectors `Λ` in the dual of the codomain of `f` and `Λ₀` in `ℝ` such that the linear combination `Λ(f' (x)) + Λ₀ * φ' (x)` equals zero for all `x`.
|