AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentSharpness

- Every fixed step has a positive scalar quadratic attaining the endpoint max-envelope at every iteration count; the balanced step attains its minimax factor on the same witness. The curvature parameters are class bounds.

theorem exists_quadratic_worst_case {α β : ℝ} (hα : 0 < α) (hαβ : α ≤ β) (h : ℝ) :
    ∃ μ : ℝ, (μ = α ∨ μ = β) ∧ 0 < μ ∧
      let f : ℝ → ℝ := fun x => μ * x ^ 2 / 2
      ContDiff ℝ 2 f ∧ StrongConvexOn univ α f ∧
      (∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2) ∧
      IsMinOn f univ 0 ∧
      ∀ N : ℕ,
        ‖(fun x => x - h * gradient f x)^[N] 1‖ = (max |1 - h * α| |1 - h * β|) ^ N ∧
        ((β - α) / (α + β)) ^ N ≤ ‖(fun x => x - h * gradient f x)^[N] 1‖ ∧
        ‖(fun x => x - (2 / (α + β)) * gradient f x)^[N] 1‖ =
          ((β - α) / (α + β)) ^ N := by
  obtain ⟨μ, hm, he⟩ : ∃ μ : ℝ, (μ = α ∨ μ = β) ∧
      |1 - h * μ| = max |1 - h * α| |1 - h * β| := by
    by_cases hc : |1 - h * α| ≤ |1 - h * β|
    · exact ⟨β, Or.inr rfl, (max_eq_right hc).symm⟩
    · exact ⟨α, Or.inl rfl, (max_eq_left (le_of_not_ge hc)).symm⟩
  have ham : α ≤ μ := by rcases hm with rfl | rfl <;> order
  have hmb : μ ≤ β := by rcases hm with rfl | rfl <;> order
  have hmpos : 0 < μ := hα.trans_le ham
  let f : ℝ → ℝ := fun x => μ * x ^ 2 / 2
  have hf : ContDiff ℝ 2 f := (contDiff_const.mul (contDiff_id.pow 2)).div_const 2
  have hg (x : ℝ) : gradient f x = μ * x := by
    have hd : HasDerivAt f (μ * x) x := by
      convert (((hasDerivAt_id x).pow 2).const_mul μ).div_const (2 : ℝ) using 1 <;> first | rfl | (simp only [id_eq]; ring)
    exact hd.hasGradientAt.gradient
  have hc : StrongConvexOn univ α f := by
    apply StrongConvexOn.mono ham
    rw [strongConvexOn_iff_convex]
    have hz : (fun x : ℝ => f x - μ / 2 * ‖x‖ ^ 2) = fun _ => 0 := by
      funext x; simp [f, Real.norm_eq_abs, sq_abs]; ring
    rw [hz]; exact convexOn_const _ convex_univ
  have hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2 := by
    intro x y
    rw [hg]; simp only [f, Real.inner_apply, Real.norm_eq_abs, sq_abs]
    nlinarith [mul_nonneg (sub_nonneg.mpr hmb) (sq_nonneg (y-x))]
  have hmin : IsMinOn f univ 0 := by
    intro x _
    change μ * (0 : ℝ) ^ 2 / 2 ≤ μ * x ^ 2 / 2
    simpa using div_nonneg (mul_nonneg hmpos.le (sq_nonneg x)) (by norm_num : (0 : ℝ) ≤ 2)
  have hn (t : ℝ) (N : ℕ) :
      ‖(fun x => x - t * gradient f x)^[N] 1‖ = |1 - t * μ| ^ N := by
    have hs : (μ • (1 : ℝ →L[ℝ] ℝ)).IsSymmetric := by
      intro x y; simp [mul_comm, mul_left_comm]
    have heig : (μ • (1 : ℝ →L[ℝ] ℝ)) 1 = μ • (1 : ℝ) := by simp
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Analysis/GradientDescentSharpness.lean:23published source at 0e31a3cda412Open detailed card

Excerpt truncated; the exact source link is authoritative.