Quadratics attain the constant-step worst-case distance bound

Let M_h be the larger of the two endpoint magnitudes. Choose mu=alpha or beta attaining this maximum. Then alpha<=mu<=beta and mu>0. This choice does not depend on N. Set f(x)=mu x²/2. Differentiate to get the actual gradient mu x. Subtracting mu‖x‖²/2 leaves the zero convex function; lowering the strong-convexity modulus gives alpha. The exact quadratic remainder is mu(y−x)²/2, which is bounded above by beta(y−x)²/2. Positivity makes0 a global minimizer. Apply the compiled eigenmode identity to H=mu I and x0=1. Its norm is |1−hmu|^N=M_h^N. The compiled optimal-step theorem applied to this certified objective gives q<=M_h. Since q>=0, raising to N preserves the inequality. At hstar=2/(alpha+beta), the two endpoint update scalars are q and−q. Either selected mu therefore gives absolute factor q, and the same exact trajectory yields q^N for every N. Together with the previously compiled uniform one-step upper bound, this witnesses its class-level sharpness.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

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
    have hr := (quadratic_eigenmode (μ • (1 : ℝ →L[ℝ] ℝ)) hs heig t N).2.1
    have heq : (fun z : ℝ => inner ℝ z ((μ • (1 : ℝ →L[ℝ] ℝ)) z) / 2) = f := by
      funext z; simp [f]; ring
    simpa only [heq, smul_eq_mul, norm_one, mul_one] using hr
  have hβ : 0 < β := hα.trans_le hαβ
  have hD : 0 < α + β := add_pos hα hβ
  have hq : 0 ≤ (β - α) / (α + β) := div_nonneg (sub_nonneg.mpr hαβ) hD.le
  have hlow := (optimal_gradient_step hf hc hα.le hβ hαβ hu 0 1).2 h
  have hbal : |1 - 2 / (α + β) * μ| = (β - α) / (α + β) := by
    rcases hm with hma | hmb
    · rw [hma]
      have ha : 1 - 2 / (α + β) * α = (β - α) / (α + β) := by field_simp; ring
      rw [ha, abs_of_nonneg hq]
    · rw [hmb]
      have hb : 1 - 2 / (α + β) * β = -((β - α) / (α + β)) := by field_simp; ring
      rw [hb, abs_neg, abs_of_nonneg hq]
  refine ⟨μ, hm, hmpos, hf, hc, hu, hmin, ?_⟩
  intro N
  rw [hn h N, hn (2 / (α + β)) N, he, hbal]
  exact ⟨rfl, pow_le_pow_left₀ hq hlow N, rfl⟩

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentSharpness

Exact module and namespace context