PL descent: the sign of the contraction factor

1. Substitute the actual gradient step into the quadratic model. Using \(h\ge0\) and \(\beta h\le1\) yields \[f(x-h\nabla f(x))\le f(x)-\tfrac h2\|\nabla f(x)\|^2.\]

2. Multiply the PL bound by \(h/2\ge 0\). With \(g(x)=f(x)-f(z)\ge0\) and \(q=1-\alpha h\), obtain \(0\le g(x-h\nabla f(x))\le qg(x)\).

3. If \(q\ge 0\), multiplication preserves order. Induction along the actual iterates gives \(g(x_N)\le q^N g(x_0)\), including \(N=0\).

4. If \(q<0\), the same one-step inequality holds for every x and forces \(g(x)=0\): otherwise qg(x)<0 contradicts nonnegativity of the next gap. Hence every gap is zero and the displayed bound still holds. Nontrivial geometric decay requires \(0\le q<1\), rather than merely the existence of a real power \(q^N\).

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic
import Mathlib.Analysis.SpecificLimits.Basic

open Set
open scoped RealInnerProductSpace
open AutoSamplingTheory.TechnicalLemmas.Analysis
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]

example {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]

1. Derives the descent estimate from the actual update and the supplied quadratic model. (1 point)
2. Uses nonnegative h/2 to combine PL with descent and obtains a nonnegative gap recurrence. (1 point)
3. Proves the iteration bound for \(q\ge 0\) and handles \(q<0\) by showing every gap vanishes. (1 point)
4. Does not add convexity or a hidden sign premise; distinguishes a bound from strict geometric decay. (1 point)

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic
import Mathlib.Analysis.SpecificLimits.Basic

open Set
open scoped RealInnerProductSpace
open AutoSamplingTheory.TechnicalLemmas.Analysis
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]

example {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
  -- Replace this comment with your proof.

Download task template

IsMinOn f univ z supplies nonnegative gaps. Function.iterate describes actual gradient iterates. The proof calls the existing gradient-step bound, combines it with hpl using nlinarith, and splits on the sign of q before invoking le_geom. Completeness is retained from the existing Lean API; it is not asserted to be a sharp mathematical hypothesis.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasic
import Mathlib.Analysis.SpecificLimits.Basic

open Set
open scoped RealInnerProductSpace
open AutoSamplingTheory.TechnicalLemmas.Analysis
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]

example {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]

Download runnable reference