Lsmooth #

Main results #

This file mainly concentrates on the properties of the L smooth function.

The main theorem is given as:

We prove the second order upper bound theorem, i.e.

Let f be a Lipschitz smooth function defined on a convex set s. f is l-Lipschitz smooth on s.

f(y) ≤ f(x) + ∇ f(x)^T (y-x) + 1 / 2 * ‖y - x‖ ^ 2 ∀ x, y ∈ s.
We prove the properties of a convex l-Lipschitz smooth function

Let f be a differentiable convex function defined on ℝ^n, then the following statement is equivalent

(a) f is l - Lipschitz smooth on ℝ^n.

(b) g(x) = 1 / 2 * ‖x‖ ^ 2 - f(x) is convex .

(c) (∇ f(x) - ∇ f(y)) ^ T(x- y) ≥ 1 / l * ‖∇ f(x) - ∇ f(y)‖ ^ 2 ∀ x, y ∈ ℝ^n.
Some relative lemmas are also contained

theorem lipschitz_continuous_upper_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {f' : E → E →L[ℝ ] ℝ} {l : NNReal} (h₁ : ∀ (x₁ : E), HasFDerivAt f (f' x₁) x₁) (h₂ : LipschitzWith l f') (x : E) (y : E) :

f y ≤ f x + (f' x) (y - x) + ↑l / 2 * ‖y - x‖ ^ 2

theorem lipschitz_continuos_upper_bound' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {f' : E → E} {l : NNReal} (h₁ : ∀ (x₁ : E), HasGradientAt f (f' x₁) x₁) (h₂ : LipschitzWith l f') (x : E) (y : E) :

f y ≤ f x + ⟪f' x, y - x⟫_ℝ + ↑l / 2 * ‖y - x‖ ^ 2

theorem lipschitz_minima_lower_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {f' : E → E} {xm : E} {l : NNReal} (h₁ : ∀ (x : E), HasGradientAt f (f' x) x) (h₂ : LipschitzWith l f') (min : IsMinOn f Set.univ xm) (hl : l > 0) (x : E) :

1 / (2 * ↑l) * ‖f' x‖ ^ 2 ≤ f x - f xm

theorem lipschitz_to_lnorm_sub_convex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {f' : E → E} {s : Set E} {l : NNReal} (hs : Convex ℝ s) (h₁ : ∀ x ∈ s, HasGradientAt f (f' x) x) (h₂ : LipschitzOnWith l f' s) (hl : l > 0) :

ConvexOn ℝ s fun (x : E) => ↑l / 2 * ‖x‖ ^ 2 - f x

theorem convex_to_lower {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {f' : E → E} {l : ℝ} (h₁ : ∀ (x : E), HasGradientAt f (f' x) x) (h₂ : ConvexOn ℝ Set.univ fun (x : E) => l / 2 * ‖x‖ ^ 2 - f x) (lp : l > 0) (hfun : ConvexOn ℝ Set.univ f) (x : E) (y : E) :

⟪f' x - f' y, x - y⟫_ℝ ≥ 1 / l * ‖f' x - f' y‖ ^ 2

theorem lipschitz_to_lower {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {f' : E → E} {l : NNReal} (h₁ : ∀ (x : E), HasGradientAt f (f' x) x) (h₂ : LipschitzWith l f') (hfun : ConvexOn ℝ Set.univ f) (hl : l > 0) (x : E) (y : E) :

⟪f' x - f' y, x - y⟫_ℝ ≥ 1 / ↑l * ‖f' x - f' y‖ ^ 2

theorem lower_to_lipschitz {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f' : E → E} {l : NNReal} (h₂ : ∀ (x y : E), ⟪f' x - f' y, x - y⟫_ℝ ≥ 1 / ↑l * ‖f' x - f' y‖ ^ 2) (hl : l > 0) :

theorem lower_iff_lipschitz {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {f' : E → E} {l : NNReal} (h₁ : ∀ (x : E), HasGradientAt f (f' x) x) (hfun : ConvexOn ℝ Set.univ f) (hl : l > 0) :

LipschitzWith l f' ↔ ∀ (x y : E), ⟪f' x - f' y, x - y⟫_ℝ ≥ 1 / ↑l * ‖f' x - f' y‖ ^ 2

theorem lipshictz_iff_lnorm_sub_convex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {f' : E → E} {l : NNReal} (h₁ : ∀ (x : E), HasGradientAt f (f' x) x) (hfun : ConvexOn ℝ Set.univ f) (hl : l > 0) :

LipschitzWith l f' ↔ ConvexOn ℝ Set.univ fun (x : E) => ↑l / 2 * ‖x‖ ^ 2 - f x

theorem lower_iff_lnorm_sub_convex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {f' : E → E} {l : NNReal} (h₁ : ∀ (x : E), HasGradientAt f (f' x) x) (hfun : ConvexOn ℝ Set.univ f) (hl : l > 0) :

(ConvexOn ℝ Set.univ fun (x : E) => ↑l / 2 * ‖x‖ ^ 2 - f x) ↔ ∀ (x y : E), ⟪f' x - f' y, x - y⟫_ℝ ≥ 1 / ↑l * ‖f' x - f' y‖ ^ 2