SubgradientMethod

Main results

This file mainly concentrates on the subgradient algorithm for unconstrained nonsmooth optimization problems.

We prove the convergence rate with different kinds of step size.

Convergence of Subgradient method

theorem bounded_subgradient_to_Lipschitz {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {G : NNReal} (hf : ConvexOn ℝ Set.univ f) (hc : ContinuousOn f Set.univ) (h : ∀ ⦃x g : E⦄, g ∈ SubderivAt f x → ‖g‖ ≤ ↑G) : LipschitzWith G f

theorem Lipschitz_to_bounded_subgradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {G : NNReal} (h : LipschitzWith G f) ⦃x : E⦄ ⦃g : E⦄ : g ∈ SubderivAt f x → ‖g‖ ≤ ↑G

theorem bounded_subgradient_iff_Lipschitz {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {G : NNReal} (hf : ConvexOn ℝ Set.univ f) (hc : ContinuousOn f Set.univ) : (∀ ⦃x g : E⦄, g ∈ SubderivAt f x → ‖g‖ ≤ ↑G) ↔ LipschitzWith G f

class subgradient_method {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (x₀ : E) : Type u_1

• x : ℕ → E
• g : ℕ → E
• a : ℕ → ℝ
• ha : ∀ (n : ℕ), subgradient_method.a f x₀ n > 0
• G : NNReal
• lipschitz : LipschitzWith (subgradient_method.G f x₀) f
• initial : subgradient_method.x f x₀ 0 = x₀
• update : ∀ (k : ℕ), subgradient_method.x f x₀ (k + 1) = subgradient_method.x f x₀ k - subgradient_method.a f x₀ k • subgradient_method.g f x₀ k
• hg : ∀ (n : ℕ), subgradient_method.g f x₀ n ∈ SubderivAt f (subgradient_method.x f x₀ n)

theorem subgradient_method.ha {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x₀ : E} [self : subgradient_method f x₀] (n : ℕ) : subgradient_method.a f x₀ n > 0

theorem subgradient_method.lipschitz {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x₀ : E} [self : subgradient_method f x₀] : LipschitzWith (subgradient_method.G f x₀) f

theorem subgradient_method.initial {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x₀ : E} [self : subgradient_method f x₀] : subgradient_method.x f x₀ 0 = x₀

theorem subgradient_method.update {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x₀ : E} [self : subgradient_method f x₀] (k : ℕ) : subgradient_method.x f x₀ (k + 1) = subgradient_method.x f x₀ k - subgradient_method.a f x₀ k • subgradient_method.g f x₀ k

theorem subgradient_method.hg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x₀ : E} [self : subgradient_method f x₀] (n : ℕ) : subgradient_method.g f x₀ n ∈ SubderivAt f (subgradient_method.x f x₀ n)

theorem subgradient_method_converge {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} (xm : E) (x₀ : E) {alg : subgradient_method f x₀} (k : ℕ) : 2 * (Finset.range (k + 1)).sum (subgradient_method.a f x₀) * (sInf {x : ℝ | ∃ i ∈ Finset.range (k + 1), f (subgradient_method.x f x₀ i) = x} - f xm) ≤ ‖x₀ - xm‖ ^ 2 + ↑(subgradient_method.G f x₀) ^ 2 * ∑ i ∈ Finset.range (k + 1), subgradient_method.a f x₀ i ^ 2

theorem subgradient_method_fix_step_size {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} (xm : E) (x₀ : E) {alg : subgradient_method f x₀} {t : ℝ} (ha' : ∀ (n : ℕ), subgradient_method.a f x₀ n = t) (k : ℕ) : sInf {x : ℝ | ∃ i ∈ Finset.range (k + 1), f (subgradient_method.x f x₀ i) = x} - f xm ≤ ‖x₀ - xm‖ ^ 2 / (2 * (↑k + 1) * t) + ↑(subgradient_method.G f x₀) ^ 2 * t / 2

convergence with fixed step size -

theorem subgradient_method_fixed_distance {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} (xm : E) (x₀ : E) (hm : IsMinOn f Set.univ xm) {alg : subgradient_method f x₀} {s : ℝ} (ha' : ∀ (n : ℕ), subgradient_method.a f x₀ n * ‖subgradient_method.g f x₀ n‖ = s) (hs : s > 0) (k : ℕ) : sInf {x : ℝ | ∃ i ∈ Finset.range (k + 1), f (subgradient_method.x f x₀ i) = x} - f xm ≤ ↑(subgradient_method.G f x₀) * ‖x₀ - xm‖ ^ 2 / (2 * (↑k + 1) * s) + ↑(subgradient_method.G f x₀) * s / 2

convergence with fixed $‖x^{i+1}-x^{i}‖$ -

theorem subgradient_method_diminishing_step_size {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} (xm : E) (x₀ : E) (hm : IsMinOn f Set.univ xm) {alg : subgradient_method f x₀} (ha' : Filter.Tendsto (subgradient_method.a f x₀) Filter.atTop (nhds 0)) (ha'' : Filter.Tendsto (fun (k : ℕ) => (Finset.range (k + 1)).sum (subgradient_method.a f x₀)) Filter.atTop Filter.atTop) : Filter.Tendsto (fun (k : ℕ) => sInf {x : ℝ | ∃ i ∈ Finset.range (k + 1), f (subgradient_method.x f x₀ i) = x}) Filter.atTop (nhds (f xm))

convergence with diminishing step size -