Gradient descent: smooth case

Fix x,y and write d=∇f(y)−∇f(x), z=y−d/β. Convexity and the actual gradient give the supporting-plane lower bound at x. This says f minus its tangent plane at x is minimized at x. The positive β makes the trial step meaningful. Apply the original upper model from y to z. Insert z−y=−d/β and z−x=(y−x)−d/β in the two models. Combining the inequalities eliminates f(z). The difference of the two linear terms is ⟨d,d⟩/β. Multiplication by 2β gives the shared division-free statement. The Lean proof carries out the same field arithmetic with β≠0 and positive reciprocal. The source reciprocal form is only recovered for β>0.

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 gradient_gap_sq_le_bregman {f : E → ℝ} {β : ℝ}
    (hf : ContDiff ℝ 1 f) (hc : ConvexOn ℝ univ f) (hβ : 0 < β)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖gradient f y - gradient f x‖ ^ 2 ≤
      2 * β * (f y - f x - inner ℝ (gradient f x) (y - x)) := by
  let d := gradient f y - gradient f x
  let z := y - β⁻¹ • d
  have hl := StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn
    (strongConvexOn_zero.mpr hc)
    (fun w _ => (hf.differentiable_one w).hasGradientAt) (mem_univ x) (mem_univ z)
  simp only [zero_div, zero_mul, add_zero] at hl
  have hh := hu y z
  have hzx : z - x = (y - x) - β⁻¹ • d := by dsimp [z]; abel
  rw [hzx, inner_sub_right, inner_smul_right] at hl
  have hzy : z - y = -(β⁻¹ • d) := by dsimp [z]; abel
  rw [hzy, inner_neg_right, inner_smul_right, norm_neg, norm_smul,
    Real.norm_eq_abs, mul_pow, sq_abs] at hh
  have hd : inner ℝ (gradient f y) d - inner ℝ (gradient f x) d = ‖d‖ ^ 2 := by
    rw [← inner_sub_left]
    exact real_inner_self_eq_norm_sq d
  have h := le_trans hl hh
  have hb : β ≠ 0 := ne_of_gt hβ
  apply (mul_le_mul_iff_right₀ (inv_pos.mpr hβ)).mp
  field_simp [hb] at h ⊢
  nlinarith

/-- Convex gradients are cocoercive in the division-free normalization.
The zero-modulus case follows by relaxing the upper model to `β + ε` and
letting positive `ε` tend to zero, without assigning meaning to a zero denominator. -/

Exact module and namespace context

Fix x,y and set d=∇f(y)−∇f(x). For ε>0, the β upper model implies the (β+ε) model because squared norm is nonnegative. Thus the positive-modulus Bregman bound applies even when β=0. The values f(x),f(y) cancel. The two Bregman gaps sum to the gradient-displacement pairing, while reversing the gradient difference preserves its squared norm. Let ε decrease to zero. The right side is affine and continuous in ε, and order is closed in ℝ. This proves the scaled bound for all β≥0. At β=0 the norm square must be zero, so the gradient is constant; no inverse at zero is used.

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 gradient_cocoercive {f : E → ℝ} {β : ℝ}
    (hf : ContDiff ℝ 1 f) (hc : ConvexOn ℝ univ f) (hβ : 0 ≤ β)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖gradient f y - gradient f x‖ ^ 2 ≤
      β * inner ℝ (gradient f y - gradient f x) (y - x) := by
  have he (ε : ℝ) (hε : 0 < ε) :
      ‖gradient f y - gradient f x‖ ^ 2 ≤
        (β + ε) * inner ℝ (gradient f y - gradient f x) (y - x) := by
    have hu' (a b : E) : f b ≤ f a + inner ℝ (gradient f a) (b - a) +
        (β + ε) / 2 * ‖b - a‖ ^ 2 := by
      have := hu a b
      nlinarith [sq_nonneg ‖b - a‖]
    have hxy := gradient_gap_sq_le_bregman hf hc (add_pos_of_nonneg_of_pos hβ hε) hu' x y
    have hyx := gradient_gap_sq_le_bregman hf hc (add_pos_of_nonneg_of_pos hβ hε) hu' y x
    rw [norm_sub_rev (gradient f x), show x - y = -(y - x) by abel, inner_neg_right] at hyx
    rw [inner_sub_left]
    nlinarith
  have ht : Tendsto (fun ε : ℝ => (β + ε) *
      inner ℝ (gradient f y - gradient f x) (y - x)) (𝓝[>] 0)
      (𝓝 (β * inner ℝ (gradient f y - gradient f x) (y - x))) := by
    simpa using (tendsto_const_nhds.add (tendsto_id.mono_left nhdsWithin_le_nhds :
      Tendsto (fun ε : ℝ => ε) (𝓝[>] 0) (𝓝 0))).mul tendsto_const_nhds
  apply ge_of_tendsto ht
  filter_upwards [self_mem_nhdsWithin] with ε hε
  exact he ε hε

/-- A C¹ convex function with the global quadratic upper model has a
`β`-Lipschitz gradient, including `β = 0`. -/

Exact module and namespace context

Write d=∇f(y)−∇f(x), v=y−x. Multiply the inner-product upper bound by the nonnegative β and combine it with cocoercivity. If ‖d‖=0, the desired inequality is immediate. Otherwise ‖d‖>0 and cancellation yields the Lipschitz estimate. This does not divide by β and therefore includes β=0.

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 gradient_lipschitz {f : E → ℝ} {β : NNReal}
    (hf : ContDiff ℝ 1 f) (hc : ConvexOn ℝ univ f)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + (β : ℝ) / 2 * ‖y - x‖ ^ 2) :
    LipschitzWith β (gradient f) := by
  rw [lipschitzWith_iff_norm_sub_le]
  intro x y
  have h := gradient_cocoercive hf hc β.coe_nonneg hu y x
  have hs := mul_le_mul_of_nonneg_left
    (real_inner_le_norm (gradient f x - gradient f y) (x - y)) β.coe_nonneg
  by_cases hz : ‖gradient f x - gradient f y‖ = 0
  · rw [hz]
    positivity
  · apply (mul_le_mul_iff_left₀ (lt_of_le_of_ne (norm_nonneg _) (Ne.symm hz))).mp
    nlinarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSmoothGradient

Exact module and namespace context

For arbitrary x,y define v=y−x, d=∇f(y)−∇f(x) and p=⟨d,v⟩. Strong convexity with α≥0 supplies convexity and the lower pairing bound. Cocoercivity supplies the upper gradient-square bound. Since h≥0 and βh≤1, multiplying the cocoercivity bound by h² gives h²‖d‖²≤h²βp≤hp. Insert this into the exact squared-norm expansion, then use hp≥αh‖v‖². The squared norm is nonnegative. Taking square roots and factoring the nonnegative factor ‖v‖² yields the asserted distance bound. If 1−αh is negative and v≠0, the squared estimate is impossible; hence no nontrivial negative-coefficient case is hidden.

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 gradient_step_contraction {f : E → ℝ} {α β h : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 ≤ α) (hβ : 0 ≤ β) (hh : 0 ≤ h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖(y - h • gradient f y) - (x - h • gradient f x)‖ ≤
      Real.sqrt (1 - α * h) * ‖y - x‖ := by
  have hc : ConvexOn ℝ univ f := hsc.convexOn (by intro r; positivity)
  have hm := StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn
    hsc (fun z _ => (hf.differentiable_one z).hasGradientAt) (mem_univ x) (mem_univ y)
  have hg := ConvexSmoothGradient.gradient_cocoercive hf hc hβ hu x y
  have hp : 0 ≤ inner ℝ (gradient f y - gradient f x) (y - x) :=
    le_trans (mul_nonneg hα (sq_nonneg _)) hm
  have hg' := mul_le_mul_of_nonneg_left hg (sq_nonneg h)
  have hs := mul_le_mul_of_nonneg_left hstep (mul_nonneg hh hp)
  have hm' := mul_le_mul_of_nonneg_left hm hh
  have hv : (y - h • gradient f y) - (x - h • gradient f x) =
      (y - x) - h • (gradient f y - gradient f x) := by rw [smul_sub]; abel
  have hb : ‖(y - h • gradient f y) - (x - h • gradient f x)‖ ^ 2 ≤
      (1 - α * h) * ‖y - x‖ ^ 2 := by
    rw [hv, norm_sub_sq_real, inner_smul_right,
      real_inner_comm (gradient f y - gradient f x), norm_smul,
      Real.norm_eq_abs, mul_pow, sq_abs]
    nlinarith
  simpa only [Real.sqrt_mul' _ (sq_nonneg _), Real.sqrt_sq (norm_nonneg _)] using
    Real.le_sqrt_of_sq_le hb

/-- The actual Nth gradient-descent iterate has geometric, then exponential,
distance control about a supplied global minimizer. -/

Exact module and namespace context

Write x⋆ for the supplied global minimizer, x₀ for the initial point, N∈ℕ for the iteration count, R=‖x₀−x⋆‖, T(x)=x−h∇f(x), and r=√(1−αh). A global minimum on the whole space is a local minimum. Fermat’s theorem sets its Fréchet derivative to zero, so the Riesz gradient vanishes. The single-step result means T is r-Lipschitz. Its Nth iterate is r^N-Lipschitz, and x⋆ stays fixed under every iterate. Apply the iterated bound to x₀ and x⋆. N=0 is included. The real inequality 1−a≤e^(−a), applied with a=αh, implies r≤e^(−αh/2). Both sides are nonnegative, so taking natural powers and multiplying by R≥0 preserves order. The exponential product identity gives the final formula.

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 gradient_descent_distance_bound {f : E → ℝ} {α β h : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 ≤ α) (hβ : 0 ≤ β) (hh : 0 ≤ h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    {xstar : E} (hmin : IsMinOn f univ xstar) (x₀ : E) (N : ℕ) :
    ‖(fun x => x - h • gradient f x)^[N] x₀ - xstar‖ ≤
        Real.sqrt (1 - α * h) ^ N * ‖x₀ - xstar‖ ∧
      Real.sqrt (1 - α * h) ^ N * ‖x₀ - xstar‖ ≤
        Real.exp (-(α * h * N) / 2) * ‖x₀ - xstar‖ := by
  let T : E → E := fun x => x - h • gradient f x
  have hg : gradient f xstar = 0 := by
    simp [gradient, (hmin.isLocalMin Filter.univ_mem).fderiv_eq_zero]
  have hfix : Function.IsFixedPt T xstar := by simp [Function.IsFixedPt, T, hg]
  have hl : LipschitzWith (Real.toNNReal (Real.sqrt (1 - α * h))) T := by
    rw [lipschitzWith_iff_norm_sub_le]
    intro x y
    simpa only [Real.coe_toNNReal _ (Real.sqrt_nonneg _)] using
      gradient_step_contraction hf hsc hα hβ hh hstep hu y x
  constructor
  · have hi := (hl.iterate N).dist_le_mul x₀ xstar
    simpa only [dist_eq_norm, (hfix.iterate N).eq, NNReal.coe_pow, Real.coe_toNNReal _ (Real.sqrt_nonneg _), T] using hi
  · have he : Real.sqrt (1 - α * h) ≤ Real.exp (-(α * h) / 2) := by
      apply (Real.sqrt_le_left (Real.exp_nonneg _)).mpr
      have hx := Real.add_one_le_exp (-(α * h))
      rw [pow_two, ← Real.exp_add, show -(α * h) / 2 + -(α * h) / 2 = -(α * h) by ring]
      simpa only [sub_eq_add_neg, add_comm] using hx
    have hp := pow_le_pow_left₀ (Real.sqrt_nonneg _) he N
    have hr := mul_le_mul_of_nonneg_right hp (norm_nonneg (x₀ - xstar))
    rw [← Real.exp_nat_mul, show (N : ℝ) * (-(α * h) / 2) =
      -(α * h * N) / 2 by ring] at hr
    exact hr

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentContraction

Exact module and namespace context

Apply the existing distance theorem at the positive step h=1/beta. Its first conclusion bounds the actual iterate by the geometric factor; compose it with the second conclusion to obtain the exponential bound. If R=0, the exponential bound has zero right-hand side. Thus every iterate has zero distance and meets any positive tolerance. This branch uses neither a real logarithm at zero nor a positive iteration count. For R>0, the ratio R/epsilon is positive. Multiply the threshold by alpha/beta>0 and divide by two. The log comparison gives R/epsilon<=exp(alpha N/(2beta)). Multiply by exp(-alpha N/(2beta)) and then by epsilon>0; the two exponential factors cancel. Combining with the first step proves the accuracy bound.

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 distance_le_of_log_bound {f : E → ℝ} {α β ε : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 < α) (hβ : 0 < β) (hε : 0 < ε)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y-x) + β/2*‖y-x‖^2)
    {xstar : E} (hmin : IsMinOn f univ xstar) (x₀ : E) (N : ℕ)
    (hN : 0 < ‖x₀-xstar‖ → 2 * (β / α) * Real.log (‖x₀-xstar‖ / ε) ≤ (N : ℝ)) :
    ‖(fun x => x - β⁻¹ • gradient f x)^[N] x₀ - xstar‖ ≤ ε := by
  have hi := GradientDescentContraction.gradient_descent_distance_bound hf hsc
    hα.le hβ.le (inv_nonneg.mpr hβ.le) (by simp [ne_of_gt hβ]) hu hmin x₀ N
  have he := hi.1.trans hi.2
  by_cases hR : ‖x₀-xstar‖ = 0
  · simpa [hR] using he.trans (by simpa [hR] using hε.le)
  · have hRp : 0 < ‖x₀-xstar‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hR)
    have ht := mul_le_mul_of_nonneg_left (hN hRp) (div_nonneg hα.le hβ.le)
    have hc : (α / β) * (2 * (β / α) * Real.log (‖x₀-xstar‖ / ε)) =
        2 * Real.log (‖x₀-xstar‖ / ε) := by field_simp
    rw [hc] at ht
    have hl : Real.log (‖x₀-xstar‖ / ε) ≤ α * β⁻¹ * N / 2 := by
      rw [div_eq_mul_inv α β] at ht
      nlinarith [ht]
    have hex := (Real.log_le_iff_le_exp (div_pos hRp hε)).mp hl
    have hb : Real.exp (-(α * β⁻¹ * N) / 2) * ‖x₀-xstar‖ ≤ ε := by
      have hm := mul_le_mul_of_nonneg_left hex (le_of_lt (Real.exp_pos (-(α * β⁻¹ * N) / 2)))
      have hid : Real.exp (-(α * β⁻¹ * N) / 2) * Real.exp (α * β⁻¹ * N / 2) = 1 := by
        rw [← Real.exp_add]; ring_nf; exact Real.exp_zero
      rw [hid] at hm
      have hh := (div_le_iff₀ hε).mp (show (Real.exp (-(α * β⁻¹ * N) / 2) * ‖x₀-xstar‖) / ε ≤ 1 by simpa [mul_div_assoc] using hm)
      simpa using hh
    exact he.trans hb

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentComplexity

Exact module and namespace context

Put g=∇f(x) and s=T(x)=x−hg. Apply the upper model at x,s. Since h≥0 and βh≤1, βh²‖g‖²≤h‖g‖². This proves the source Lemma3.1 descent estimate using the canonical shared descent interface. The compiled first-order support theorem follows from the source chord definition and the genuine gradient, supplied by C¹ differentiability. Set v=x−z and g=∇f(x). No minimum condition on z enters. Multiply each function inequality by 2h≥0 and insert the exact squared-distance expansion. The h²‖g‖² terms cancel. This gives the stated one-step energy inequality even when the comparator gap is negative.

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 gradient_step_energy_bound {f : E → ℝ} {α β h : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hh : 0 ≤ h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x z : E) :
    ‖x - h • gradient f x - z‖ ^ 2 + 2 * h * (f (x - h • gradient f x) - f z) ≤
      (1 - α * h) * ‖x - z‖ ^ 2 := by
  have hl := StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn
    hsc (fun w _ => (hf.differentiable_one w).hasGradientAt) (mem_univ x) (mem_univ z)
  have hd := GradientDescentBasic.gradient_step_descent_of_quadratic_upper_bound hh hstep hu x
  have hn : z - x = -(x - z) := by abel
  rw [hn, inner_neg_right, norm_neg] at hl
  have hl' := mul_le_mul_of_nonneg_left hl (by positivity : 0 ≤ 2 * h)
  have hd' := mul_le_mul_of_nonneg_left hd (by positivity : 0 ≤ 2 * h)
  rw [show x - h • gradient f x - z = (x - z) - h • gradient f x by abel,
    norm_sub_sq_real, inner_smul_right, real_inner_comm (gradient f x),
    norm_smul, Real.norm_eq_abs, mul_pow, sq_abs]
  nlinarith

/-- Weighted final function gap for actual gradient-descent iterates. The
coefficient domain is explicit and includes both zero and one. -/

Exact module and namespace context

Define x_n=T^n(x₀), u_n=‖x_n−z‖², g_n=f(x_n)−f(z), and q=1−αh≥0. The one-step energy inequality gives the recurrence, and shared descent gives g_(n+1)≤g_n. The gaps themselves need not be nonnegative. Apply Mathlib’s recurrence theorem with constant coefficient q and forcing −2h g_(n+1). This theorem permits signed forcing. Constant products become powers; no inverse of q is introduced, so q=0 is admitted. For k<N, monotonicity gives g_N≤g_(k+1). Multiply by the nonpositive coefficient −2h and then the nonnegative weight q^(N−1−k). Sum, discard u_N≥0, and reverse the finite index. Write S_N=Σ_(k=0)^(N−1)q^k and R=‖x₀−z‖. This proves the final bound also for N=0.

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 gradient_descent_weighted_value_bound {f : E → ℝ} {α β h : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hh : 0 ≤ h) (hstep : β * h ≤ 1) (hcoeff : α * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x₀ z : E) (N : ℕ) :
    2 * h * (∑ k ∈ range N, (1 - α * h) ^ k) *
        (f ((fun x => x - h • gradient f x)^[N] x₀) - f z) ≤
      (1 - α * h) ^ N * ‖x₀ - z‖ ^ 2 := by
  let T : E → E := fun x => x - h • gradient f x
  let X : ℕ → E := fun n => T^[n] x₀
  let q : ℝ := 1 - α * h
  have hq : 0 ≤ q := sub_nonneg.mpr hcoeff
  have hX (n : ℕ) : X (n + 1) = T (X n) := Function.iterate_succ_apply' _ _ _
  have hm : Antitone (fun n => f (X n)) := by
    apply antitone_nat_of_succ_le
    intro n
    have hd := GradientDescentBasic.gradient_step_descent_of_quadratic_upper_bound hh hstep hu (X n)
    rw [hX]
    dsimp [T]
    have : 0 ≤ h / 2 * ‖gradient f (X n)‖ ^ 2 := by positivity
    linarith
  have hr (n : ℕ) (_ : 0 ≤ n) :
      ‖X (n + 1) - z‖ ^ 2 ≤ q * ‖X n - z‖ ^ 2 + (-2 * h * (f (X (n + 1)) - f z)) := by
    have he := gradient_step_energy_bound hf hsc hh hstep hu (X n) z
    rw [hX]
    dsimp [T, q]
    linarith
  have hg := discrete_gronwall_prod_general (u := fun n => ‖X n - z‖ ^ 2)
    (b := fun n => -2 * h * (f (X (n + 1)) - f z)) (c := fun _ => q) hr (fun _ _ => hq) (Nat.zero_le N)
  simp only [Finset.prod_const, Nat.card_Ico, Nat.Ico_zero_eq_range, Finset.card_range] at hg
  have hs : ∑ k ∈ range N, (-2 * h * (f (X (k + 1)) - f z)) * q ^ (N - (k + 1)) ≤
      ∑ k ∈ range N, (-2 * h * (f (X N) - f z)) * q ^ (N - (k + 1)) := by
    apply sum_le_sum
    intro k hk
    have hm' := hm (by have := mem_range.mp hk; omega : k + 1 ≤ N)
    apply mul_le_mul_of_nonneg_right _ (pow_nonneg hq _)
    have hh' : 0 ≤ 2 * h := by positivity
    nlinarith
  have hsum : (∑ k ∈ range N, q ^ (N - (k + 1))) = ∑ k ∈ range N, q ^ k := by
    rw [← sum_range_reflect (fun k => q ^ k) N]
    apply sum_congr rfl
    intro k _
    congr 1
    omega
  rw [← mul_sum, hsum] at hs
  have hu0 : X 0 = x₀ := rfl
  rw [hu0] at hg
  have huN := sq_nonneg ‖X N - z‖
  change 2 * h * (∑ k ∈ range N, q ^ k) * (f (X N) - f z) ≤ q ^ N * ‖x₀ - z‖ ^ 2
  nlinarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentValue

Exact module and namespace context

Write q=1-alpha h, R=||x0-z|| and e_N=f(X_N)-f(z). The existing weighted theorem already derives objective descent and the forced recurrence for the actual gradient iterates. Invoke it directly; its conclusion also allows negative comparator gaps. For a convex objective set alpha=0, hence q=1. Every summand equals one and there are exactly N summands. Thus the weighted estimate becomes 2hN e_N<=R². Since h>0 and N>0, the coefficient 2hN is positive. Dividing preserves the inequality. With beta>0, substituting h=1/beta gives exactly beta R²/(2N), the source prescribed-step convex rate. This substitution is exercised by a compiled consumer test.

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 convex_value_le {f : E → ℝ} {β h : ℝ} (hf : ContDiff ℝ 1 f)
    (hc : ConvexOn ℝ univ f) (hh : 0 < h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x₀ z : E) {N : ℕ} (hN : 0 < N) :
    f ((fun x => x - h • gradient f x)^[N] x₀) - f z ≤ ‖x₀ - z‖ ^ 2 / (2 * h * N) := by
  have he := gradient_descent_weighted_value_bound hf
    (strongConvexOn_zero.mpr hc) hh.le hstep (by norm_num : (0 : ℝ) * h ≤ 1) hu x₀ z N
  simp only [zero_mul, sub_zero, one_pow, sum_const, card_range, nsmul_eq_mul,
    mul_one, one_mul] at he
  apply (le_div_iff₀ (by positivity : 0 < 2 * h * (N : ℝ))).mpr
  nlinarith [he]

/-- Strongly convex rational rate, and exact inverse-power form on its positive-base domain. -/

Exact module and namespace context

Write q=1-alpha h, R=||x0-z|| and e_N=f(X_N)-f(z). The existing weighted theorem already derives objective descent and the forced recurrence for the actual gradient iterates. Invoke it directly; its conclusion also allows negative comparator gaps. Positive alpha and h with alpha h<=1 give 0<=q<1. For N>0, q^N<1. The finite geometric identity, multiplied by 2, yields 2alpha h sum(q^k)=2(1-q^N). Multiply the weighted estimate by positive alpha and divide by positive 2(1-q^N). This rational form remains valid at q=0. Under the additional strict inequality alpha h<1, q>0 and q^N>0. Integer negative powers equal inverse positive powers. Multiplying numerator and denominator by q^N proves the exact displayed equality. At q=0 only the preceding rational conclusion applies; the negative-power formula is undefined in ordinary real arithmetic.

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 strongly_convex_value_le {f : E → ℝ} {α β h : ℝ} (hf : ContDiff ℝ 1 f)
    (hsc : StrongConvexOn univ α f) (hα : 0 < α) (hh : 0 < h) (hstep : β * h ≤ 1)
    (hcoeff : α * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x₀ z : E) {N : ℕ} (hN : 0 < N) :
    f ((fun x => x - h • gradient f x)^[N] x₀) - f z ≤
      α * (1 - α * h) ^ N * ‖x₀ - z‖ ^ 2 / (2 * (1 - (1 - α * h) ^ N)) ∧
    (α * h < 1 → f ((fun x => x - h • gradient f x)^[N] x₀) - f z ≤
      α / (2 * ((1 - α * h) ^ (-(N : ℤ)) - 1)) * ‖x₀ - z‖ ^ 2) := by
  have hq : 0 ≤ 1 - α * h := by linarith
  have hqlt : 1 - α * h < 1 := by nlinarith
  have he := gradient_descent_weighted_value_bound hf hsc hh.le hstep (by linarith) hu x₀ z N
  have hs := geom_sum_mul_neg (1 - α * h) N
  have hp : (1 - α * h) ^ N < 1 := pow_lt_one₀ hq hqlt (Nat.ne_of_gt hN)
  have hr : f ((fun x => x - h • gradient f x)^[N] x₀) - f z ≤
      α * (1 - α * h) ^ N * ‖x₀ - z‖ ^ 2 / (2 * (1 - (1 - α * h) ^ N)) := by
    apply (le_div_iff₀ (by positivity : 0 < 2 * (1 - (1 - α * h) ^ N))).mpr
    have hem := mul_le_mul_of_nonneg_left he hα.le
    have hid : α * (2 * h * ∑ k ∈ range N, (1 - α * h) ^ k) =
        2 * (1 - (1 - α * h) ^ N) := by nlinarith [hs]
    rw [← mul_assoc, hid] at hem
    nlinarith [hem]
  refine ⟨hr, ?_⟩
  intro hstrict
  have hqp : 0 < (1 - α * h) ^ N := pow_pos (by linarith) N
  have heq : α * (1 - α * h) ^ N * ‖x₀ - z‖ ^ 2 /
      (2 * (1 - (1 - α * h) ^ N)) =
      α / (2 * ((1 - α * h) ^ (-(N : ℤ)) - 1)) * ‖x₀ - z‖ ^ 2 := by
    rw [zpow_neg, zpow_natCast]
    field_simp
  rwa [heq] at hr

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentRates

Exact module and namespace context

Write g=∇f(x), T(x)=x−hg. The displacement is −hg; inner-product and norm identities evaluate the model exactly. Multiply βh≤1 by h‖g‖²≥0. Substituting the result leaves half of the linear decrease.

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 gradient_step_descent_of_quadratic_upper_bound {f : E → ℝ} {β h : ℝ}
    (hh : 0 ≤ h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x : E) : f (x - h • gradient f x) - f x ≤ -(h / 2) * ‖gradient f x‖ ^ 2 := by
  have hu' := hu x (x - h • gradient f x)
  have he : x - h • gradient f x - x = -(h • gradient f x) := by abel
  rw [he, inner_neg_right, inner_smul_right, real_inner_self_eq_norm_sq,
    norm_neg, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs] at hu'
  have hs := mul_le_mul_of_nonneg_right hstep (mul_nonneg hh (sq_nonneg ‖gradient f x‖))
  nlinarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic

Exact module and namespace context

Let z be the supplied global minimizer, G(x)=f(x)−f(z)≥0 and q=1−αh. Multiply 2αG(x)≤‖∇f(x)‖² by h/2≥0 and combine with the shared descent bound. If q≥0, set u_n=G(Tⁿx₀). The actual iterate successor identity gives u_(n+1)≤q u_n. Apply the existing scalar geometric bound; no convexity enters. If q<0, nonnegative gaps and the one-step bound force G(x)=0 for every x. Both sides of the claimed rate are zero for every natural N, including odd N.

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 gradient_descent_pl_value_bound {f : E → ℝ} {α β h : ℝ} {z : E}
    (hz : IsMinOn f univ z) (hh : 0 ≤ h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (hpl : ∀ x, 2 * α * (f x - f z) ≤ ‖gradient f x‖ ^ 2)
    (x₀ : E) (N : ℕ) :
    f ((fun x => x - h • gradient f x)^[N] x₀) - f z ≤
      (1 - α * h) ^ N * (f x₀ - f z) := by
  let T : E → E := fun x => x - h • gradient f x
  let q : ℝ := 1 - α * h
  have hnonneg (x : E) : 0 ≤ f x - f z := sub_nonneg.mpr (hz (mem_univ x))
  have hrec (x : E) : f (T x) - f z ≤ q * (f x - f z) := by
    have hd := GradientDescentBasic.gradient_step_descent_of_quadratic_upper_bound hh hstep hu x
    have hp := mul_le_mul_of_nonneg_left (hpl x) (show 0 ≤ h / 2 by positivity)
    dsimp [T, q]
    nlinarith
  by_cases hq : 0 ≤ q
  · have hr := le_geom (u := fun n => f (T^[n] x₀) - f z) hq N (by
      intro k _
      rw [Function.iterate_succ_apply']
      exact hrec _)
    exact hr
  · have hzero (x : E) : f x - f z = 0 := by
      have hc : q * (f x - f z) ≥ 0 := (hnonneg (T x)).trans (hrec x)
      have hneg : q < 0 := lt_of_not_ge hq
      have hx := hnonneg x
      nlinarith
    change f (T^[N] x₀) - f z ≤ q ^ N * (f x₀ - f z)
    rw [hzero, hzero, mul_zero]

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentPL

Exact module and namespace context

The existing shared descent theorem controls the gradient norm at x_k by the decrease from x_k to x_(k+1). The successor identity connects the abstract iterate to the actual update. Distribute h/2 over the finite sum, sum the pointwise inequalities, then cancel adjacent objective values with Mathlib’s reversed telescoping identity. No lower bound is needed.

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 gradient_descent_sum_sq_bound {f : E → ℝ} {β h : ℝ}
    (hh : 0 ≤ h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x₀ : E) (N : ℕ) :
    h / 2 * ∑ k ∈ Finset.range N, ‖gradient f ((fun x => x - h • gradient f x)^[k] x₀)‖ ^ 2 ≤
      f x₀ - f ((fun x => x - h • gradient f x)^[N] x₀) := by
  let T : E → E := fun x => x - h • gradient f x
  calc
    h / 2 * ∑ k ∈ Finset.range N, ‖gradient f (T^[k] x₀)‖ ^ 2 =
        ∑ k ∈ Finset.range N, h / 2 * ‖gradient f (T^[k] x₀)‖ ^ 2 := Finset.mul_sum _ _ _
    _ ≤ ∑ k ∈ Finset.range N, (f (T^[k] x₀) - f (T^[k + 1] x₀)) := by
      apply Finset.sum_le_sum
      intro k _
      rw [Function.iterate_succ_apply']
      have hd := GradientDescentBasic.gradient_step_descent_of_quadratic_upper_bound
        hh hstep hu (T^[k] x₀)
      change h / 2 * ‖gradient f (T^[k] x₀)‖ ^ 2 ≤ f (T^[k] x₀) - f (T (T^[k] x₀))
      dsimp [T] at *
      linarith
    _ = f x₀ - f (T^[N] x₀) := by
      simpa using Finset.sum_range_sub' (fun k => f (T^[k] x₀)) N

/-- Among the first `N` actual gradient iterates, one has small gradient norm.
This is a best-iterate guarantee, not a last-iterate or global optimality guarantee. -/

Exact module and namespace context

The supplied global minimizer z gives f(z)≤f(x_N). Apply accumulated descent to replace the final objective value by f(z). Let B=2(f(x₀)−f(z))/(Nh). Since h>0 and N>0, multiplication by h/2 preserves and reflects order; (h/2)NB is exactly the initial gap. Hence the sum is at most NB. A nonempty finite sum bounded by the sum of the constant B has a term at most B. Convert that squared-norm bound to a norm bound with Mathlib’s square-root lemma. The witness is one of x₀,…,x_(N−1).

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_gradient_descent_norm_le {f : E → ℝ} {β h : ℝ} {z : E}
    (hz : IsMinOn f univ z) (hh : 0 < h) (hstep : β * h ≤ 1)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x₀ : E) {N : ℕ} (hN : 0 < N) :
    ∃ k ∈ Finset.range N,
      ‖gradient f ((fun x => x - h • gradient f x)^[k] x₀)‖ ≤
        Real.sqrt (2 * (f x₀ - f z) / ((N : ℝ) * h)) := by
  let T : E → E := fun x => x - h • gradient f x
  let B : ℝ := 2 * (f x₀ - f z) / ((N : ℝ) * h)
  have hNr : 0 < (N : ℝ) := by exact_mod_cast hN
  have hd := gradient_descent_sum_sq_bound hh.le hstep hu x₀ N
  have hzN : f z ≤ f (T^[N] x₀) := hz (mem_univ _)
  have hsum : (∑ k ∈ Finset.range N, ‖gradient f (T^[k] x₀)‖ ^ 2) ≤
      ∑ _k ∈ Finset.range N, B := by
    have hb : h / 2 * ((N : ℝ) * B) = f x₀ - f z := by
      dsimp [B]
      field_simp
    simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
    apply (mul_le_mul_iff_right₀ (show 0 < h / 2 by positivity)).mp
    change h / 2 * (∑ k ∈ Finset.range N, ‖gradient f (T^[k] x₀)‖ ^ 2) ≤
      h / 2 * ((N : ℝ) * B)
    rw [hb]
    change h / 2 * (∑ k ∈ Finset.range N, ‖gradient f (T^[k] x₀)‖ ^ 2) ≤
      f x₀ - f (T^[N] x₀) at hd
    linarith
  obtain ⟨k, hk, hkle⟩ := Finset.exists_le_of_sum_le ⟨0, Finset.mem_range.mpr hN⟩ hsum
  refine ⟨k, hk, ?_⟩
  exact Real.le_sqrt_of_sq_le hkle

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarity

Exact module and namespace context

Apply the strong-convex first-order gradient monotonicity theorem and its C² Hessian equivalence. The upper-model equivalence gives the opposite inequality. The Riesz map turns D²f(z) into a continuous linear operator H_z with the displayed quadratic form. Differentiate T_h to obtain A_z=I−hH_z. C² symmetry makes A_z symmetric. Multiplying the Hessian inequalities by h≥0 puts the Rayleigh value of every nonzero vector in [1−hβ,1−hα]. Its absolute value is at most the maximum of the endpoint absolute values. Mathlib’s supremum formula bounds the operator norm; the zero vector is treated separately. In this supremum the Rayleigh quotient is assigned value zero at v=0, including when E is the zero space. Set v=y−x. The derivative of t↦T_h(x+tv) is A_(x+tv)v and is continuous. The vector fundamental theorem of calculus expresses the update difference as its integral over [0,1]. Bound the integral norm by the uniform derivative bound times the segment length.

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 gradient_step_endpoint_bound {f : E → ℝ} {α β h : ℝ}
    (hf : ContDiff ℝ 2 f) (hsc : StrongConvexOn univ α f) (hh : 0 ≤ h)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖(y - h • gradient f y) - (x - h • gradient f x)‖ ≤
      max |1 - h * α| |1 - h * β| * ‖y - x‖ := by
  let M := max |1 - h * α| |1 - h * β|
  have hM : 0 ≤ M := (abs_nonneg _).trans (le_max_left _ _)
  have hlo := (ConvexityC2.gradient_mono_iff_fderiv2_lower hf).mp (fun a b =>
    StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn hsc
      (fun z _ => ((hf.of_le (by norm_num) : ContDiff ℝ 1 f).differentiable_one z).hasGradientAt)
      (mem_univ a) (mem_univ b))
  have hup := (SmoothnessEquivalences.upper_model_iff_fderiv2_upper hf).mp hu
  let R : (E →L[ℝ] ℝ) →L[ℝ] E :=
    { toFun := (toDual ℝ E).symm
      map_add' := (toDual ℝ E).symm.map_add
      map_smul' := by intros; simp
      cont := (toDual ℝ E).symm.continuous }
  let H (z : E) : E →L[ℝ] E := R.comp (fderiv ℝ (fderiv ℝ f) z)
  let A (z : E) : E →L[ℝ] E := ContinuousLinearMap.id ℝ E - h • H z
  let T : E → E := fun z => z - h • gradient f z
  have hfd : ContDiff ℝ 1 (fderiv ℝ f) := hf.fderiv_right (by norm_num)
  have hgrad (z : E) : HasFDerivAt (gradient f) (H z) z :=
    R.hasFDerivAt.comp z (hfd.differentiable_one z).hasFDerivAt
  have hTd (z : E) : HasFDerivAt T (A z) z :=
    (hasFDerivAt_id z).sub ((hgrad z).const_smul h)
  have hT : ContDiff ℝ 1 T := contDiff_id.sub ((R.contDiff.comp hfd).const_smul h)
  have hinner (z v w : E) : inner ℝ (H z v) w = (fderiv ℝ (fderiv ℝ f) z v) w :=
    toDual_symm_apply
  have hsym (z : E) : (A z).IsSymmetric := by
    intro v w
    change inner ℝ (v - h • H z v) w = inner ℝ v (w - h • H z w)
    rw [inner_sub_left, inner_sub_right, real_inner_smul_left, inner_smul_right]
    have hr : inner ℝ v (H z w) = (fderiv ℝ (fderiv ℝ f) z w) v :=
      (real_inner_comm v (H z w)).symm.trans (hinner z w v)
    rw [hinner, hr]
    rw [hf.contDiffAt.isSymmSndFDerivAt (by norm_num) v w]
  have hnorm (z : E) : ‖A z‖ ≤ M := by
    rw [(A z).norm_eq_iSup_rayleighQuotient (hsym z)]
    apply ciSup_le
    intro v
    change |inner ℝ (A z v) v / ‖v‖ ^ 2| ≤ M
    by_cases hv : v = 0
    · simp [hv]
      exact hM
    · simp only [abs_div, abs_pow, abs_norm]
      apply (div_le_iff₀ (sq_pos_of_pos (norm_pos_iff.mpr hv))).mpr
      change |inner ℝ (v - h • H z v) v| ≤ M * ‖v‖ ^ 2
      rw [inner_sub_left, real_inner_smul_left, real_inner_self_eq_norm_sq, hinner]
      have hl := mul_le_mul_of_nonneg_left (hlo z v) hh
      have hu' := mul_le_mul_of_nonneg_left (hup z v) hh
      have hleft : 1 - h * α ≤ M := (le_abs_self _).trans (le_max_left _ _)
      have hright : -(1 - h * β) ≤ M := (neg_le_abs _).trans (le_max_right _ _)
      have hleft' := mul_le_mul_of_nonneg_right hleft (sq_nonneg ‖v‖)
      have hright' := mul_le_mul_of_nonneg_right hright (sq_nonneg ‖v‖)
      exact abs_le.mpr ⟨by nlinarith, by nlinarith⟩
  let v := y - x
  have hpath (t : ℝ) : HasDerivAt (fun s : ℝ => T (x + s • v)) (A (x + t • v) v) t := by
    convert (hTd (x + t • v)).comp_hasDerivAt t
      (((hasDerivAt_id t).smul_const v).const_add x) using 1 <;> simp [Function.comp_def]
  have hc : Continuous (fun t : ℝ => A (x + t • v) v) := by
    have hA : A = fderiv ℝ T := funext (fun z => (hTd z).fderiv.symm)
    rw [hA]
    exact ((hT.continuous_fderiv (by norm_num)).comp
      (continuous_const.add (continuous_id.smul continuous_const))).clm_apply continuous_const
  have hFTC : (∫ t : ℝ in 0..1, A (x + t • v) v) = T y - T x := by
    simpa [v] using intervalIntegral.integral_eq_sub_of_hasDerivAt
      (fun t _ => hpath t) (hc.intervalIntegrable 0 1)
  change ‖T y - T x‖ ≤ M * ‖v‖
  rw [← hFTC]
  simpa using intervalIntegral.norm_integral_le_of_norm_le_const (a := (0 : ℝ)) (b := 1)
    (fun t _ => ((A (x + t • v)).le_opNorm v).trans
      (mul_le_mul_of_nonneg_right (hnorm _) (norm_nonneg v)))

/-- The step `2/(α+β)` gives the sharp uniform curvature-envelope contraction.
Its factor minimizes the endpoint max-envelope over every real step.
The `α=0` boundary is nonexpansive, and `α=β` is retained. -/

Exact module and namespace context

Let D=α+β>0 and q=(β−α)/D≥0. At h★=2/D the endpoint values are q and −q. Their maximum absolute value is q, so the preceding actual-gradient bound gives the stated two-point inequality. For any real h, M_h≥1−hα and M_h≥hβ−1. Multiply these inequalities by β≥0 and α≥0 respectively and add. The h terms cancel. Dividing by α+β>0 yields M_h≥q, including negative h. This is envelope minimization, not an objective-by-objective optimal-step theorem.

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 optimal_gradient_step {f : E → ℝ} {α β : ℝ}
    (hf : ContDiff ℝ 2 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 ≤ α) (hβ : 0 < β) (hαβ : α ≤ β)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖(y - (2 / (α + β)) • gradient f y) - (x - (2 / (α + β)) • gradient f x)‖ ≤
        ((β - α) / (α + β)) * ‖y - x‖ ∧
      ∀ h : ℝ, (β - α) / (α + β) ≤ max |1 - h * α| |1 - h * β| := by
  have hD : 0 < α + β := add_pos_of_nonneg_of_pos hα hβ
  have hq : 0 ≤ (β - α) / (α + β) := div_nonneg (sub_nonneg.mpr hαβ) hD.le
  have ha : 1 - 2 / (α + β) * α = (β - α) / (α + β) := by field_simp; ring
  have hb : 1 - 2 / (α + β) * β = -((β - α) / (α + β)) := by field_simp; ring
  constructor
  · have hc := gradient_step_endpoint_bound hf hsc (show 0 ≤ 2 / (α + β) by positivity) hu x y
    simpa only [ha, hb, abs_neg, abs_of_nonneg hq, max_self] using hc
  · intro h
    let M := max |1 - h * α| |1 - h * β|
    have ha' : 1 - h * α ≤ M := (le_abs_self _).trans (le_max_left _ _)
    have hb' : -(1 - h * β) ≤ M := (neg_le_abs _).trans (le_max_right _ _)
    apply (div_le_iff₀ hD).mpr
    have h1 := mul_le_mul_of_nonneg_left ha' hβ.le
    have h2 := mul_le_mul_of_nonneg_left hb' hα
    nlinarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStep

Exact module and namespace context

The product rule for the inner product gives half the sum of two linear terms. Symmetry moves H between arguments, and real inner-product symmetry identifies both terms. This is the continuous linear functional represented by Hx, so uniqueness of the Riesz gradient yields ∇f(x)=Hx. Substitute the computed gradient into T_h. The update is the continuous linear endomorphism I−hH. Reuse Mathlib’s identity equating endomorphism powers with function iteration; the zero-th power is the identity.

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 quadratic_gradient_iterate (H : E →L[ℝ] E) (hH : H.IsSymmetric)
    (h : ℝ) (N : ℕ) (x : E) :
    let f := fun z : E => inner ℝ z (H z) / 2
    (fun z => z - h • gradient f z)^[N] x = ((1 - h • H) ^ N) x := by
  let f := fun z : E => inner ℝ z (H z) / 2
  have hg (z : E) : gradient f z = H z := by
    have hraw := ((hasFDerivAt_id z).inner ℝ H.hasFDerivAt).const_mul (1 / 2 : ℝ)
    have hlin : (1 / 2 : ℝ) •
        ((fderivInnerCLM ℝ (z, H z)).comp ((ContinuousLinearMap.id ℝ E).prod H)) =
        toDual ℝ E (H z) := by
      ext v
      change (1 / 2 : ℝ) * (inner ℝ z (H v) + inner ℝ v (H z)) = inner ℝ (H z) v
      rw [← hH.apply_clm z v, (real_inner_comm v (H z)).symm]
      ring
    have hd : HasFDerivAt f (toDual ℝ E (H z)) z := by
      convert hraw using 1 <;> first | rfl | exact hlin.symm | (ext v; simp only [f, id_eq]; ring)
    exact (hasGradientAt_iff_hasFDerivAt.mpr hd).gradient
  change (fun z => z - h • gradient f z)^[N] x = _
  simp_rw [hg]
  exact congrFun (FunLike.coe_pow_eq_iterate (1 - h • H) N).symm x

/-- A supplied eigenmode gives exact iterates, distances to zero and quadratic values.
No existence of an eigenvector or stability of the chosen step is assumed. -/

Exact module and namespace context

The given relation Hx=μx implies (I−hH)x=(1−hμ)x. If x=0, every power identity is immediate. Otherwise this is a genuine nonzero eigenvector of I−hH, so Mathlib’s eigenvector power theorem applies. No eigenvector is constructed. Take norms of the scalar multiple and use homogeneity. The quadratic is homogeneous of degree two, so its value is multiplied by the square of the trajectory scalar. The absolute value is essential when the update changes sign.

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 quadratic_eigenmode (H : E →L[ℝ] E) (hH : H.IsSymmetric)
    {μ : ℝ} {x : E} (hx : H x = μ • x) (h : ℝ) (N : ℕ) :
    let f := fun z : E => inner ℝ z (H z) / 2
    let z := (fun y => y - h • gradient f y)^[N] x
    z = (1 - h * μ) ^ N • x ∧
      ‖z‖ = |1 - h * μ| ^ N * ‖x‖ ∧
      f z = (1 - h * μ) ^ (2 * N) * f x := by
  let f := fun z : E => inner ℝ z (H z) / 2
  let A : E →L[ℝ] E := 1 - h • H
  have hAx : A x = (1 - h * μ) • x := by
    simp only [A, sub_apply, one_apply_eq_self,
      smul_apply, hx, smul_smul, sub_smul, one_smul]
  have hp : (A ^ N) x = (1 - h * μ) ^ N • x := by
    by_cases hz : x = 0
    · simp [hz]
    · have he : Module.End.HasEigenvector A.toLinearMap (1 - h * μ) x :=
        ⟨Module.End.mem_eigenspace_iff.mpr hAx, hz⟩
      have ht := congrArg (fun K : E →ₗ[ℝ] E => K x) (ContinuousLinearMap.toLinearMap_pow A N)
      convert ht.trans (he.pow_apply N) using 1; rfl
  have hi := (quadratic_gradient_iterate H hH h N x).trans hp
  change _ = _ ∧ _ = _ ∧ f _ = _ * f x
  rw [hi]
  refine ⟨rfl, ?_, ?_⟩
  · simp [norm_smul, Real.norm_eq_abs]
  · simp only [f, map_smul, inner_smul_left, inner_smul_right, RCLike.conj_to_real]
    rw [Nat.mul_comm 2 N, pow_mul]
    ring

end AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticGradientDescent

Exact module and namespace context

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

For beta>0 and N natural set D=N+1 and mu=beta/(2D). Then D>=1 and0<mu<=beta. Reuse the compiled scalar-quadratic witness with both curvature endpoints equal to mu. Equality of the endpoints forces that witness to be exactly f(x)=mu x²/2. It supplies C2 regularity, mu strong convexity, minimizer0 and the genuine gradient trajectory. At the prescribed step1/beta the scalar contraction is q=1−1/(2D), which is nonnegative. The existing norm identity gives norm(x_N)=q^N. Since the objective is mu times the squared norm divided by2 and f(0)=0, this is also an exact objective-gap formula. Enlarging the quadratic upper model from mu to beta verifies the advertised smoothness class. Apply Bernoulli to q and exponent N. The resulting affine lower bound is (D+1)/(2D), at least1/2. Thus even after N steps the selected small curvature leaves at least half of the initial distance. Squaring the nonnegative half-distance bound gives q^(2N)>=1/4. Multiply by the positive beta/(4D) in the exact objective identity. With the source upper rate for N>0, the resulting family obstructs any uniformly faster order at this prescribed step.

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 quadratic_gap_lower_bound {β : ℝ} (hβ : 0 < β) (N : ℕ) :
    let μ := β / (2 * ((N : ℝ) + 1))
    let f : ℝ → ℝ := fun x => μ * x ^ 2 / 2
    0 < μ ∧ 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 ∧
      let z := (fun x => x - (1 / β) * gradient f x)^[N] 1
      f z - f 0 = β / (4 * ((N : ℝ) + 1)) *
        (1 - 1 / (2 * ((N : ℝ) + 1))) ^ (2 * N) ∧
      β / (16 * ((N : ℝ) + 1)) ≤ f z - f 0 := by
  let D : ℝ := (N : ℝ) + 1
  have hD : 0 < D := by dsimp [D]; positivity
  have hD1 : 1 ≤ D := by dsimp [D]; exact le_add_of_nonneg_left (Nat.cast_nonneg N)
  let μ := β / (2 * D)
  have hμ : 0 < μ := div_pos hβ (by positivity)
  have hμβ : μ ≤ β := by
    apply (div_le_iff₀ (by positivity : 0 < 2 * D)).mpr
    nlinarith
  obtain ⟨ν, hν, _, hf, hc, hu, hm, hn⟩ :=
    exists_quadratic_worst_case hμ (le_refl μ) (1 / β)
  have hv : ν = μ := hν.elim id id
  subst ν
  let f : ℝ → ℝ := fun x => μ * x ^ 2 / 2
  let q : ℝ := 1 - 1 / (2 * D)
  have hq : 0 ≤ q := by
    have : 1 / (2 * D) ≤ 1 := (div_le_one (by positivity)).mpr (by linarith)
    dsimp [q]; linarith
  have he : 1 - 1 / β * μ = q := by
    dsimp [μ, q]; field_simp
  have hn' : ‖(fun x => x - (1 / β) * gradient f x)^[N] 1‖ = q ^ N := by
    simpa only [max_self, he, abs_of_nonneg hq] using (hn N).1
  have hpow : 1 / 2 ≤ q ^ N := by
    have hb := one_add_mul_sub_le_pow (by linarith : -1 ≤ q) N
    have heq : 1 + (N : ℝ) * (q - 1) = (D + 1) / (2 * D) := by
      dsimp [q, D]; field_simp; ring
    rw [heq] at hb
    have : (1 : ℝ) / 2 ≤ (D + 1) / (2 * D) := by
      apply (le_div_iff₀ (by positivity)).mpr
      linarith
    exact this.trans hb
  have huβ : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2 := by
    intro x y
    have hh : f y ≤ f x + inner ℝ (gradient f x) (y - x) + μ / 2 * ‖y - x‖ ^ 2 := hu x y
    nlinarith [mul_nonneg (sub_nonneg.mpr hμβ) (sq_nonneg ‖y - x‖)]
  change 0 < μ ∧ _ ∧ _ ∧ _ ∧ _ ∧ _
  refine ⟨hμ, hf, hc, huβ, hm, ?_⟩
  dsimp only
  have hvalue : f ((fun x => x - (1 / β) * gradient f x)^[N] 1) - f 0 =
      β / (4 * D) * (q ^ N) ^ 2 := by
    have hs : ((fun x => x - (1 / β) * gradient f x)^[N] 1) ^ 2 = (q ^ N) ^ 2 := by
      simpa only [Real.norm_eq_abs, abs_mul_abs_self, sq] using congrArg (fun r : ℝ => r * r) hn'
    change μ * _ ^ 2 / 2 - μ * 0 ^ 2 / 2 = _
    rw [hs]
    dsimp [μ]; field_simp; ring
  rw [hvalue]
  change β / (4 * D) * (q ^ N) ^ 2 = β / (4 * D) * q ^ (2 * N) ∧
    β / (16 * D) ≤ β / (4 * D) * (q ^ N) ^ 2
  constructor
  · rw [Nat.mul_comm 2 N, pow_mul]
  · have hs : (1 : ℝ) / 4 ≤ (q ^ N) ^ 2 := by nlinarith
    have := mul_le_mul_of_nonneg_left hs (by positivity : 0 ≤ β / (4 * D))
    convert this using 1 <;> first | rfl | (field_simp; ring)

end AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexGradientGapSharpness

Exact module and namespace context