the properties of strongly convex function and gradient descent method for strongly convex function
theorem
Strongly_Convex_Bound
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{s : Set E}
{f : E → ℝ}
(m : ℝ)
(strongly_convex : StrongConvexOn s m f)
⦃x : E⦄
:
theorem
stronglyConvexOn_def
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{s : Set E}
{f : E → ℝ}
{m : ℝ}
(hs : Convex ℝ s)
(hfun : ∀ ⦃x : E⦄,
x ∈ s →
∀ ⦃y : E⦄,
y ∈ s →
∀ ⦃a : ℝ⦄,
0 ≤ a → ∀ ⦃b : ℝ⦄, 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ a * f x + b * f y - m / 2 * a * b * ‖x - y‖ ^ 2)
:
StrongConvexOn s m f
theorem
Strongly_Convex_Unique_Minima
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{s : Set E}
{f : E → ℝ}
{m : ℝ}
{xm : E}
{xm' : E}
{mp : m > 0}
(hsc : StrongConvexOn s m f)
(min : IsMinOn f s xm)
(min' : IsMinOn f s xm')
(hxm : xm ∈ s)
(hxm' : xm' ∈ s)
:
xm = xm'
theorem
Strong_Convex_lower
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{s : Set E}
{f : E → ℝ}
{m : ℝ}
{f' : E → E}
(hsc : StrongConvexOn s m f)
(hf : ∀ x ∈ s, HasGradientAt f (f' x) x)
(x : E)
:
theorem
Lower_Strong_Convex
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{s : Set E}
{f : E → ℝ}
{m : ℝ}
{f' : E → E}
(hf : ∀ x ∈ s, HasGradientAt f (f' x) x)
(hs : Convex ℝ s)
(h : ∀ x ∈ s, ∀ y ∈ s, ⟪f' x - f' y, x - y⟫_ℝ ≥ m * ‖x - y‖ ^ 2)
:
StrongConvexOn s m f
theorem
Strong_Convex_iff_lower
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{s : Set E}
{f : E → ℝ}
{m : ℝ}
{f' : E → E}
(hf : ∀ x ∈ s, HasGradientAt f (f' x) x)
(hs : Convex ℝ s)
:
theorem
Strong_Convex_second_lower
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{s : Set E}
{f : E → ℝ}
{m : ℝ}
{f' : E → E}
(hsc : StrongConvexOn s m f)
(hf : ∀ x ∈ s, HasGradientAt f (f' x) x)
(x : E)
: