ConvexFunction #
Main results #
This file mainly concentrates on the differentiable convex function and its properties.
The main theorem is given as:
Let f be a smooth function defined on a convex set s. Then the following statement is equivalent
(a) f is convex on s.
(b) (first order condition) f(y) ≥ f(x) + ∇ f(x)^T (y-x) ∀ x, y ∈ s.
(c) (monotonic of gradient) (∇ f(x) - ∇ f(y))^T (x-y) ≥ 0 ∀ x, y ∈ s.
Besides we also proof the corresponding properties for strict convex function.
theorem
Convex_first_order_condition
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : E → ℝ}
{f' : E → E →L[ℝ] ℝ}
{x : E}
{s : Set E}
(h : HasFDerivAt f (f' x) x)
(hf : ConvexOn ℝ s f)
(xs : x ∈ s)
(y : E)
:
theorem
Convex_first_order_condition_inverse
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : E → ℝ}
{f' : E → E →L[ℝ] ℝ}
{s : Set E}
(h : ∀ x ∈ s, HasFDerivAt f (f' x) x)
(h₁ : Convex ℝ s)
(h₂ : ∀ x ∈ s, ∀ y ∈ s, f x + (f' x) (y - x) ≤ f y)
:
theorem
Convex_monotone_gradient
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{f : E → ℝ}
{f' : E → E →L[ℝ] ℝ}
{s : Set E}
(hfun : ConvexOn ℝ s f)
(h : ∀ x ∈ s, HasFDerivAt f (f' x) x)
(x : E)
:
theorem
Convex_first_order_condition'
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{f : E → ℝ}
{f' : E → E}
{s : Set E}
{x : E}
(h : HasGradientAt f (f' x) x)
(hf : ConvexOn ℝ s f)
(xs : x ∈ s)
(y : E)
:
theorem
Convex_first_order_condition_inverse'
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{f : E → ℝ}
{f' : E → E}
{s : Set E}
(h : ∀ x ∈ s, HasGradientAt f (f' x) x)
(h₁ : Convex ℝ s)
(h₂ : ∀ x ∈ s, ∀ y ∈ s, f x + ⟪f' x, y - x⟫_ℝ ≤ f y)
:
theorem
Convex_first_order_condition_iff'
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{f : E → ℝ}
{f' : E → E}
{s : Set E}
(h₁ : Convex ℝ s)
(h : ∀ x ∈ s, HasGradientAt f (f' x) x)
:
theorem
Convex_monotone_gradient'
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{f : E → ℝ}
{f' : E → E}
{s : Set E}
(hfun : ConvexOn ℝ s f)
(h : ∀ x ∈ s, HasGradientAt f (f' x) x)
(x : E)
:
theorem
monotone_gradient_convex'
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{f : E → ℝ}
{f' : E → E}
{s : Set E}
(h₁ : Convex ℝ s)
(hf : ∀ x ∈ s, HasGradientAt f (f' x) x)
(mono : ∀ x ∈ s, ∀ y ∈ s, ⟪f' x - f' y, x - y⟫_ℝ ≥ 0)
:
theorem
monotone_gradient_iff_convex'
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{f : E → ℝ}
{f' : E → E}
{s : Set E}
(h₁ : Convex ℝ s)
(hf : ∀ x ∈ s, HasGradientAt f (f' x) x)
:
theorem
monotone_gradient_convex
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{f : E → ℝ}
{s : Set E}
{f' : E → E →L[ℝ] ℝ}
(h₁ : Convex ℝ s)
(hf : ∀ x ∈ s, HasFDerivAt f (f' x) x)
(mono : ∀ x ∈ s, ∀ y ∈ s, (f' x - f' y) (x - y) ≥ 0)
:
theorem
montone_gradient_iff_convex
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{f : E → ℝ}
{s : Set E}
{f' : E → E →L[ℝ] ℝ}
(h₁ : Convex ℝ s)
(hf : ∀ x ∈ s, HasFDerivAt f (f' x) x)
:
theorem
monotone_gradient_strict_convex
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{f : E → ℝ}
{f' : E → E}
{s : Set E}
(hs : Convex ℝ s)
(hf : ∀ x ∈ s, HasGradientAt f (f' x) x)
(mono : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → ⟪f' x - f' y, x - y⟫_ℝ > 0)
:
StrictConvexOn ℝ s f
theorem
strict_convex_monotone_gradient
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{f : E → ℝ}
{f' : E → E}
{s : Set E}
(hf : ∀ x ∈ s, HasGradientAt f (f' x) x)
(h₁ : StrictConvexOn ℝ s f)
(x : E)
:
theorem
strict_convex_iff_monotone_gradient
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
{f : E → ℝ}
{f' : E → E}
{s : Set E}
(hs : Convex ℝ s)
(h : ∀ x ∈ s, HasGradientAt f (f' x) x)
: