Actual terminal reference by gradient descent

Mathematical statement

The derived a,c are positive and k≥1. The exact gradient is grad F(x)=grad U(x)+(x-u)/A. Both N and x_plus are measurable. For every v, the output satisfies norm(grad F(x_plus(v)))^2≤d/A and the exact center-residual identity norm(u-A*grad U(x_plus(v))-x_plus(v))=A*norm(grad F(x_plus(v)))≤sqrt(d*A). All j<N(v) strictly fail the stopping test. N(v)≤ceil(k*log(1+A*norm(grad F(v))^2/d)), and N(v)+1≤k*log(1+A*norm(grad F(v))^2/d)+2. Under the additional starting-law moment hypotheses, N+1 is genuinely integrable and its expectation is at most 2+k*log(1+A*M/d).

theorem terminal_reference_gradient_descent [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E] {U : E → ℝ} {m b : ℝ≥0}
    (hU : ContDiff ℝ 2 U)
    (hH : ∀ x v : E, (m:ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ U) x v) v ∧
      (fderiv ℝ (fderiv ℝ U) x v) v ≤ (b:ℝ)*‖v‖^2)
    (hmb : m ≤ b) {A d : ℝ} (hA : 0 < A) (hd : 0 < d)
    (_hdim : d = Module.finrank ℝ E) (u : E) :
    let F := fun x => U x+A⁻¹/2*‖x-u‖^2
    let a := (m:ℝ)+A⁻¹
    let c := (b:ℝ)+A⁻¹
    let k := c/a
    let T := fun x => x-c⁻¹ • gradient F x
    let N := firstIndex T F (d/A)
    let xp := fun v => T^[N v] v
    0 < a ∧ 0 < c ∧ 1 ≤ k ∧
    (∀ x, gradient F x=gradient U x+A⁻¹ • (x-u)) ∧
    Measurable N ∧ Measurable xp ∧
    (∀ v, ‖gradient F (xp v)‖^2 ≤ d/A ∧
      ‖u-A • gradient U (xp v)-xp v‖=A*‖gradient F (xp v)‖ ∧
      ‖u-A • gradient U (xp v)-xp v‖ ≤ Real.sqrt (d*A) ∧
      (∀ j < N v, d/A < ‖gradient F (T^[j] v)‖^2) ∧
      N v ≤ Nat.ceil (k*Real.log (1+A*‖gradient F v‖^2/d)) ∧
      (N v:ℝ)+1 ≤ k*Real.log (1+A*‖gradient F v‖^2/d)+2) ∧
    (∀ (μ : Measure E), IsProbabilityMeasure μ → ∀ M : ℝ,
      Integrable (fun v => ‖gradient F v‖^2) μ →
      (∫ v, ‖gradient F v‖^2 ∂μ) ≤ M →
      Integrable (fun v => (N v:ℝ)+1) μ ∧
      (∫ v, (N v:ℝ)+1 ∂μ) ≤ 2+k*Real.log (1+A*M/d))

Proof roadmap

1. 1Derive the actual regularized gradient and curvature

   The quadratic term has derivative A^{-1}<x-u, .>. Adding it to the derivative of U gives the exact gradient formula. Reuse QuadraticRegularization for strong convexity and gradient Lipschitz continuity. To obtain the quadratic upper model, apply the Hessian-to-strong-convexity theorem to -U with modulus -b, then the first-order lower bound and reverse its signs. Add the exact quadratic expansion. Since A>0 and 0≤m≤b, a,c>0 and k≥1. No model inequality or gradient field is supplied as an assumption.

2. 2Control gradients through adjacent actual iterates

   Apply the existing one-step contraction to x and T(x). Their distance is c^{-1} times the norm of grad F(x); the next distance is c^{-1} times the norm of grad F(T(x)). Cancel the positive step and iterate this inequality. Bound sqrt(1-a/c) by exp(-a/(2c)), then square the resulting norm bound. This uses the source gradient-descent map and needs no supplied minimizer. It is a stronger local proof than the source display with an extra k prefactor, rather than a literal replay of that display.

3. 3Give a finite stopping certificate including degenerate gradients

   Put s=d/A>0 and z=norm(grad F(v))^2≥0. The natural ceiling n=ceil(k log(1+z/s)) satisfies n≥k log(1+z/s). Therefore exp(-n/k)z≤z/(1+z/s)≤s. This constructs a finite successful index before Nat.find is used. The argument covers z=0 and k=1 without taking log(1-1/k). The ceiling bound and ceil(t)<t+1 for t≥0 later give the extra two units in the real count bound.

4. 4Prove the first-hit index and stopped output are measurable

   The C1 gradient is continuous, hence T and each finite iterate are continuous. Each event where the nth gradient square is at most s is Borel measurable. The finite-attainment certificate identifies N with Nat.find of this event family. measurable_find proves N measurable, and Measurable.find proves measurability of v mapped to T^N(v)(v). Nat.find_spec gives success and Nat.find_min gives strict failure for every earlier index. Pointwise termination is not used as a substitute for measurability.

5. 5Convert the stopping test into the required terminal residual

   At every x, the exact gradient formula gives u-A grad U(x)-x=-A grad F(x). Because A>0, its norm is A times norm(grad F(x)). At the stopped point, multiply the proved gradient-square threshold by A squared; the result is at most dA. Taking the nonnegative square root yields the center residual used by the terminal sampler. This proves the residual of the constructed point rather than receiving it as input.

6. 6Establish integrability before the expected-count bound

   For g(v)=norm(grad F(v))^2, the given nonnegative integrable g and Eg≤M imply M≥0. First use 0≤log(1+g/s)≤g/s to prove logarithmic integrability. The log-ratio inequality gives the displayed tangent bound; both sides are integrable before integrating. Its remainder has nonpositive expectation by Eg≤M. Finally, measurability and the pointwise count bound imply N+1 is integrable, and integral monotonicity gives the expected count. This is a direct logarithmic tangent proof, not a call to a Jensen API or a presumption of cost integrability.

7. 7Assemble the actual fixed-parameter reference and counting contract

   Instantiate the stopping and expectation lemmas with the genuine F, its proved a,c and threshold d/A. The pointwise conclusions hold for every starting point; the expected-cost clause is then quantified over any probability starting law satisfying the actual gradient moment hypotheses. At an initially successful point N=0 and one gradient check is charged. Each visit needs one U-gradient evaluation because the regularization term is algebraic, and the computed gradient is reused for the next update. The final gradient is charged; no unproved saving is deducted when later combining this construction with a sampler.