def
DescentDirection
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{f : E → ℝ}
{f' : E → E}
(d : E)
(x : E)
:
HasGradientAt f (f' x) x → Prop
Equations
- DescentDirection d x✝ x = (⟪f' x✝, d⟫_ℝ < 0)
Instances For
theorem
optimal_no_descent_direction
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{xm : E}
{f : E → ℝ}
{f' : E → E}
(hf : ∀ (x : E), HasGradientAt f (f' x) x)
(min : IsMinOn f Set.univ xm)
(hfc : ContinuousOn f' Set.univ)
(d : E)
:
¬DescentDirection d xm ⋯
theorem
first_order_unconstrained
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{xm : E}
{f : E → ℝ}
{f' : E → E}
(hf : ∀ (x : E), HasGradientAt f (f' x) x)
(min : IsMinOn f Set.univ xm)
(hfc : ContinuousOn f' Set.univ)
:
f' xm = 0
theorem
first_order_convex
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{xm : E}
{f : E → ℝ}
{f' : E → E}
(hf : ∀ (x : E), HasGradientAt f (f' x) x)
(hcon : ConvexOn ℝ Set.univ f)
(hfm : f' xm = 0)
:
IsMinOn f Set.univ xm
theorem
first_order_convex_iff
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{xm : E}
{f : E → ℝ}
{f' : E → E}
(hf : ∀ (x : E), HasGradientAt f (f' x) x)
(hcon : ConvexOn ℝ Set.univ f)
(hfc : ContinuousOn f' Set.univ)
: