Lower bounds for smooth optimization

Fermat gives the genuine gradient at z equal to zero. Apply the existing strong-convexity first-order lower bound at z. The resulting alpha/2 factor is essential: the older midpoint-only alpha/4 bound would not give the prescribed halving constant. Assume the actual current point has distance at most r_k. Positivity of R and alpha makes r_k and delta_k=alpha*r_k²/8 positive, so the base solver contract applies. Its objective guarantee combined with quadratic growth yields squared distance at most r_k²/4. Nonnegative norms and r_k>0 then give radius r_k/2=r_(k+1). The initial radius is the supplied hypothesis. At every stage the prescribed radius appears in both the tolerance and the solver budget. Their ratio is exactly 8beta/alpha, so no monotonicity of phi is needed. The recursion adds the returned cost to the accumulated natural count. Induction gives c_N<=N phi(8beta/alpha). The chosen horizon gives r_N<=sqrt(epsilon/alpha). Pass that positive upper radius, together with tolerance epsilon, to the same solver at the actual state x_N. Its output has objective gap at most epsilon. The final budget argument simplifies exactly to beta/alpha. Add this final returned cost, including when 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 radius_accuracy_and_cost {f : E → ℝ} {α β R ε : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 < α) (hβ : 0 < β) (hR : 0 < R) (hε : 0 < ε)
    {z x₀ : E} (hmin : IsMinOn f univ z) (hx₀ : ‖x₀-z‖ ≤ R)
    (A : E → ℝ → ℝ → E × ℕ) (φ : ℝ → ℕ)
    (hA : ∀ y r δ, 0 < r → 0 < δ → ‖y-z‖ ≤ r →
      f (A y r δ).1 - f z ≤ δ ∧ (A y r δ).2 ≤ φ (β*r^2/δ))
    (N : ℕ) (hN : α * (R / (2:ℝ)^N)^2 ≤ ε) :
    let r := fun k : ℕ => R / (2:ℝ)^k
    let run : ℕ → E × ℕ := Nat.rec (x₀, 0) (fun k p =>
      let w := A p.1 (r k) (α*(r k)^2/8)
      (w.1, p.2 + w.2))
    let last := A (run N).1 (Real.sqrt (ε/α)) ε
    ‖(run N).1-z‖ ≤ r N ∧ (run N).2 ≤ N * φ (8*(β/α)) ∧
      f last.1 - f z ≤ ε ∧ (run N).2 + last.2 ≤ N * φ (8*(β/α)) + φ (β/α) := by
  let r := fun k : ℕ => R / (2:ℝ)^k
  let run : ℕ → E × ℕ := Nat.rec (x₀, 0) (fun k p =>
    let w := A p.1 (r k) (α*(r k)^2/8)
    (w.1, p.2 + w.2))
  change ‖(run N).1-z‖ ≤ r N ∧ (run N).2 ≤ N * φ (8*(β/α)) ∧ _
  have hr (k : ℕ) : 0 < r k := div_pos hR (pow_pos (by norm_num) _)
  have hgrad : gradient f z = 0 := by
    simp [gradient, (hmin.isLocalMin Filter.univ_mem).fderiv_eq_zero]
  have hqg (y : E) : α/2 * ‖y-z‖^2 ≤ f y - f z := by
    have h := StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn hsc
      (fun x _ => (hf.differentiable_one x).hasGradientAt) (mem_univ z) (mem_univ y)
    rw [hgrad, inner_zero_left] at h
    linarith
  have hind (k : ℕ) : ‖(run k).1-z‖ ≤ r k ∧ (run k).2 ≤ k * φ (8*(β/α)) := by
    induction k with
    | zero => simpa [run, r] using hx₀
    | succ k ih =>
      have hδ : 0 < α*(r k)^2/8 := by positivity
      have hw := hA (run k).1 (r k) (α*(r k)^2/8) (hr k) hδ ih.1
      have hid : β*(r k)^2 / (α*(r k)^2/8) = 8*(β/α) := by
        field_simp [ne_of_gt (hr k)]
      rw [hid] at hw
      have hs : r (k+1) = r k / 2 := by dsimp [r]; rw [pow_succ, div_mul_eq_div_div]
      constructor
      · change ‖(A (run k).1 (r k) (α*(r k)^2/8)).1-z‖ ≤ r (k+1)
        rw [hs]
        have hg := (hqg (A (run k).1 (r k) (α*(r k)^2/8)).1).trans hw.1
        have hsquare : ‖(A (run k).1 (r k) (α*(r k)^2/8)).1-z‖^2 ≤ (r k/2)^2 := by
          nlinarith
        nlinarith [norm_nonneg ((A (run k).1 (r k) (α*(r k)^2/8)).1-z), hr k]
      · change (run k).2 + (A (run k).1 (r k) (α*(r k)^2/8)).2 ≤ (k+1) * φ (8*(β/α))
        simpa only [Nat.add_mul, Nat.one_mul] using Nat.add_le_add ih.2 hw.2
  have hs : r N ≤ Real.sqrt (ε/α) := by
    apply Real.le_sqrt_of_sq_le
    exact (le_div_iff₀ hα).mpr (by nlinarith [hN])
  have hlast := hA (run N).1 (Real.sqrt (ε/α)) ε
    (Real.sqrt_pos.mpr (div_pos hε hα)) hε ((hind N).1.trans hs)
  have hid : β * (Real.sqrt (ε/α))^2 / ε = β/α := by
    rw [Real.sq_sqrt (div_nonneg hε.le hα.le)]
    field_simp
  rw [hid] at hlast
  exact ⟨(hind N).1, (hind N).2, hlast.1, Nat.add_le_add (hind N).2 hlast.2⟩
end AutoSamplingTheory.TechnicalLemmas.Analysis.RestartReduction

Exact module and namespace context

All logarithm arguments are positive. Natural ceiling gives L<=N. Multiply by the positive log4 and use monotonicity of log together with log(4^N)=N log4 to obtain q<=4^N. Since (2^N)²=4^N, this is exactly the horizon condition required by the finite restart theorem. For L>=0, the natural ceiling is less than L+1. For L<0, it equals zero. Thus N<=max(0,L)+1 globally. More precisely, N=0 iff L<=0 iff q<=1 iff alpha R²<=epsilon. This certifies only that no halving stage is needed; the final solver call remains. Apply the existing radius_accuracy_and_cost theorem at this N using the horizon just proved. Its Nat.rec is exactly the recursion below. It supplies the actual state radius, final output error, and the natural sum of all certified call costs. The new theorem does not assume a radius invariant or an adequate iteration count. Cast the natural cost inequality to real numbers. Both phi values are nonnegative, so replacing N by its upper bound preserves the inequality. This global logarithmic bound uses no comparison between the two phi values. Under the additional condition phi(kappa)<=phi(8kappa), the final cost can be absorbed with the displayed universal factor. The result is (max(0,L)+2)phi(8kappa). If additionally q>=4, then L>=1, so L+2<=3L. This gives the explicit constant3/log4 in front of phi(8kappa)logq. These are conditional consequences; no monotonicity of phi or all-accuracy logarithmic bound is silently asserted.

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 logarithmic_accuracy_and_cost {f : E → ℝ} {α β R ε : ℝ}
    (hf : ContDiff ℝ 1 f) (hsc : StrongConvexOn univ α f)
    (hα : 0 < α) (hβ : 0 < β) (hR : 0 < R) (hε : 0 < ε)
    {z x₀ : E} (hmin : IsMinOn f univ z) (hx₀ : ‖x₀-z‖ ≤ R)
    (A : E → ℝ → ℝ → E × ℕ) (φ : ℝ → ℕ)
    (hA : ∀ y r δ, 0 < r → 0 < δ → ‖y-z‖ ≤ r →
      f (A y r δ).1 - f z ≤ δ ∧ (A y r δ).2 ≤ φ (β*r^2/δ)) :
    let L := Real.log (α*R^2/ε) / Real.log 4
    let N := ⌈L⌉₊
    let r := fun k : ℕ => R / (2:ℝ)^k
    let run : ℕ → E × ℕ := Nat.rec (x₀, 0) (fun k p =>
      let w := A p.1 (r k) (α*(r k)^2/8)
      (w.1, p.2 + w.2))
    let last := A (run N).1 (Real.sqrt (ε/α)) ε
    let C := (run N).2 + last.2
    (N : ℝ) ≤ max 0 L + 1 ∧ (N = 0 ↔ α*R^2 ≤ ε) ∧
      ‖(run N).1-z‖ ≤ r N ∧ f last.1 - f z ≤ ε ∧
      C ≤ N * φ (8*(β/α)) + φ (β/α) ∧
      (C : ℝ) ≤ (max 0 L + 1) * φ (8*(β/α)) + φ (β/α) ∧
      (φ (β/α) ≤ φ (8*(β/α)) →
        (C : ℝ) ≤ (max 0 L + 2) * φ (8*(β/α)) ∧
        (4 ≤ α*R^2/ε → (C : ℝ) ≤ 3*L*φ (8*(β/α)))) := by
  let L := Real.log (α*R^2/ε) / Real.log 4
  let N := ⌈L⌉₊
  have hlog : 0 < Real.log 4 := Real.log_pos (by norm_num)
  have hq : 0 < α*R^2/ε := by positivity
  have hround : (N : ℝ) ≤ max 0 L + 1 := by
    by_cases hL : 0 ≤ L
    · exact (Nat.ceil_lt_add_one hL).le.trans (by rw [max_eq_right hL])
    · have hz : N = 0 := Nat.ceil_eq_zero.mpr (le_of_not_ge hL)
      rw [hz, Nat.cast_zero, max_eq_left (le_of_not_ge hL)]
      norm_num
  have hzero : N = 0 ↔ α*R^2 ≤ ε := by
    change ⌈Real.log (α*R^2/ε) / Real.log 4⌉₊ = 0 ↔ _
    rw [Nat.ceil_eq_zero, div_le_iff₀ hlog, zero_mul]
    rw [← Real.log_one, Real.log_le_log_iff hq (by norm_num)]
    exact (div_le_iff₀ hε).trans (by simp)
  have hpow : α*R^2/ε ≤ (4:ℝ)^N := by
    apply (Real.log_le_log_iff hq (by positivity)).mp
    rw [Real.log_pow]
    exact (div_le_iff₀ hlog).mp (Nat.le_ceil L)
  have hid : ((2:ℝ)^N)^2 = (4:ℝ)^N := by
    rw [← pow_mul, Nat.mul_comm N 2, pow_mul]
    norm_num
  have hN : α*(R/(2:ℝ)^N)^2 ≤ ε := by
    rw [div_pow, ← mul_div_assoc, hid]
    apply (div_le_iff₀ (by positivity : 0 < (4:ℝ)^N)).mpr
    have h := (div_le_iff₀ hε).mp hpow
    nlinarith
  have hb := RestartReduction.radius_accuracy_and_cost hf hsc hα hβ hR hε
    hmin hx₀ A φ hA N hN
  let r := fun k : ℕ => R / (2:ℝ)^k
  let run : ℕ → E × ℕ := Nat.rec (x₀, 0) (fun k p =>
    let w := A p.1 (r k) (α*(r k)^2/8)
    (w.1, p.2 + w.2))
  let last := A (run N).1 (Real.sqrt (ε/α)) ε
  let C := (run N).2 + last.2
  have hcast : (C : ℝ) ≤ (N : ℝ) * φ (8*(β/α)) + φ (β/α) := by
    have hc : C ≤ N * φ (8*(β/α)) + φ (β/α) := hb.2.2.2
    simpa only [Nat.cast_add, Nat.cast_mul] using ((Nat.cast_le (α := ℝ)).mpr hc)
  have hm : (N : ℝ) * φ (8*(β/α)) ≤
      (max 0 L + 1) * φ (8*(β/α)) :=
    mul_le_mul_of_nonneg_right hround (Nat.cast_nonneg _)
  have hreal : (C : ℝ) ≤ (max 0 L + 1) * φ (8*(β/α)) + φ (β/α) := by
    linarith
  refine ⟨hround, hzero, hb.1, hb.2.2.1, hb.2.2.2, hreal, ?_⟩
  intro hφ
  have hp : (φ (β/α) : ℝ) ≤ φ (8*(β/α)) := by exact_mod_cast hφ
  have ha : (C : ℝ) ≤ (max 0 L + 2) * φ (8*(β/α)) := by nlinarith
  refine ⟨ha, ?_⟩
  intro hsmall
  have hL : 1 ≤ L := by
    apply (le_div_iff₀ hlog).mpr
    simpa using (Real.log_le_log (by norm_num : (0:ℝ)<4) hsmall)
  rw [max_eq_right (by linarith : 0 ≤ L)] at ha
  have hfactor : L+2 ≤ 3*L := by linarith
  exact ha.trans (mul_le_mul_of_nonneg_right hfactor (Nat.cast_nonneg _))

end AutoSamplingTheory.TechnicalLemmas.Analysis.RestartLogComplexity

Exact module and namespace context

Delta is positive because epsilon and R are positive. The squared distance to x0 is continuous, so W is continuous. The closed ball of radius R centered at x0 is compact and contains z. The extreme value theorem gives w in that ball minimizing W there; in particular W(w)<=W(z). Inside the ball the comparison is already proved. Outside it, ||x-x0||>R>=||z-x0||. The original global minimality gives f(z)<=f(x), and the nonnegative quadratic coefficient gives the same order for the two penalties. Therefore W(z)<=W(x), and W(w)<=W(z)<=W(x). This constructs actual global minimality, not just constrained minimality. Combine W(w)<=W(z) with f(z)<=f(w). Subtract the objective terms, then cancel the positive delta/2. The squared distance of w from x0 is no larger than that of z. Both norms are nonnegative, so their order follows. No uniqueness or convexity is used. For any x whose W-gap above W(w) is at most epsilon/2, nonnegativity of the penalty gives f(x)<=W(x). The minimizer comparison bounds W(w) by W(z). The radius certificate gives delta||z-x0||²/2<=delta R²/2=epsilon/2. Adding the two half-error terms yields f(x)-f(z)<=epsilon.

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_minimizer_radius_and_accuracy
    {E : Type*} [NormedAddCommGroup E] [ProperSpace E]
    {f : E → ℝ} (hf : Continuous f) {z x₀ : E} (hz : IsMinOn f univ z)
    {R ε : ℝ} (hR : 0 < R) (hε : 0 < ε) (hx : ‖z-x₀‖ ≤ R) :
    let δ := ε/R^2
    let W := fun x => f x + δ/2*‖x-x₀‖^2
    ∃ w, IsMinOn W univ w ∧ ‖w-x₀‖ ≤ ‖z-x₀‖ ∧
      ∀ x, W x - W w ≤ ε/2 → f x - f z ≤ ε := by
  let δ := ε/R^2
  let W := fun x => f x + δ/2*‖x-x₀‖^2
  have hδ : 0 < δ := div_pos hε (sq_pos_of_pos hR)
  have hn : Continuous (fun x : E => ‖x-x₀‖^2) :=
    ((continuous_id.sub continuous_const).norm).pow 2
  have hW : Continuous W := hf.add (continuous_const.mul hn)
  have hzball : z ∈ closedBall x₀ R := by simpa [mem_closedBall, dist_eq_norm] using hx
  obtain ⟨w, _, hw⟩ := (isCompact_closedBall x₀ R).exists_isMinOn ⟨z,hzball⟩ hW.continuousOn
  have hwz : W w ≤ W z := hw hzball
  have hglobal : IsMinOn W univ w := by
    intro x _
    by_cases hb : x ∈ closedBall x₀ R
    · exact hw hb
    · have hr : R < ‖x-x₀‖ := by simpa [mem_closedBall, dist_eq_norm] using hb
      have hs : ‖z-x₀‖^2 ≤ ‖x-x₀‖^2 := by
        nlinarith [norm_nonneg (z-x₀), norm_nonneg (x-x₀)]
      have hzfx : f z ≤ f x := hz (mem_univ x)
      have hquad := mul_le_mul_of_nonneg_left hs (le_of_lt (div_pos hδ (by norm_num : (0:ℝ)<2)))
      have hzW : W z ≤ W x := by dsimp [W]; linarith
      exact hwz.trans hzW
  have hradius : ‖w-x₀‖ ≤ ‖z-x₀‖ := by
    have hzw : f z ≤ f w := hz (mem_univ w)
    have hs : ‖w-x₀‖^2 ≤ ‖z-x₀‖^2 := by
      dsimp [W] at hwz
      nlinarith
    nlinarith [norm_nonneg (w-x₀), norm_nonneg (z-x₀)]
  refine ⟨w,hglobal,hradius,?_⟩
  intro x he
  have hbase : f x ≤ W x := by
    dsimp [W]
    exact le_add_of_nonneg_right (mul_nonneg (div_nonneg hδ.le (by norm_num)) (sq_nonneg _))
  have hs : ‖z-x₀‖^2 ≤ R^2 := by nlinarith [norm_nonneg (z-x₀)]
  have hquad := mul_le_mul_of_nonneg_left hs (le_of_lt (div_pos hδ (by norm_num : (0:ℝ)<2)))
  have hid : δ/2*R^2 = ε/2 := by dsimp [δ]; field_simp
  rw [hid] at hquad
  dsimp [W] at hwz
  change W x - W w ≤ ε/2 at he
  have : W w ≤ f z + ε/2 := by dsimp [W]; linarith
  linarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationTransfer

Exact module and namespace context

Subtract delta||x||²/2 from W. Expanding the squared distance leaves f plus a linear functional and a constant. This is convex because f is convex. The Mathlib characterization therefore proves delta-strong convexity, with the delta/2 chord convention. Differentiate the squared norm composed with x↦x-u, multiply by delta/2 and add the derivative of f. The factors two and one-half cancel. This gives the genuine Frechet derivative of W and hence its differentiability. Apply the inverse Riesz isometry to the derivative just computed. Linearity preserves addition and scalar multiplication, while the inverse of the functional v↦⟨x-u,v⟩ is x-u. Thus the claimed gradient is computed from W, not supplied as an assumption. Subtract the gradient identity at y from the one at x; the center cancels. The triangle inequality, the given beta-Lipschitz estimate for the true gradient of f, and nonnegativity of delta bound the two terms. Add the bounds to obtain beta+delta.

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 curvature_gradient_and_smoothness
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    {f : E → ℝ} (hd : Differentiable ℝ f) (hc : ConvexOn ℝ univ f)
    {β δ : ℝ≥0} (hL : LipschitzWith β (gradient f)) (u : E) :
    let W := fun x => f x + (δ : ℝ)/2*‖x-u‖^2
    Differentiable ℝ W ∧ StrongConvexOn univ (δ : ℝ) W ∧
      (∀ x, gradient W x = gradient f x + (δ : ℝ) • (x-u)) ∧
      LipschitzWith (β+δ) (gradient W) := by
  let W := fun x => f x + (δ : ℝ)/2*‖x-u‖^2
  have hq (x : E) : HasFDerivAt (fun z => (δ : ℝ)/2*‖z-u‖^2)
      ((δ : ℝ) • innerSL ℝ (x-u)) x := by
    convert (((hasFDerivAt_id x).sub_const u).norm_sq).const_mul ((δ : ℝ)/2)
      using 1 <;> first | rfl | (ext v; simp; ring)
  have hWd : Differentiable ℝ W := fun x => ((hd x).hasFDerivAt.add (hq x)).differentiableAt
  have hgrad (x : E) : gradient W x = gradient f x + (δ : ℝ) • (x-u) := by
    have hfd : fderiv ℝ W x = fderiv ℝ f x + (δ : ℝ) • innerSL ℝ (x-u) :=
      ((hd x).hasFDerivAt.add (hq x)).fderiv
    rw [gradient, hfd, map_add, map_smul]
    congr 1
    exact congrArg (fun v : E => (δ : ℝ) • v) ((toDual ℝ E).symm_apply_apply (x-u))
  have hstrong : StrongConvexOn univ (δ : ℝ) W := by
    apply strongConvexOn_iff_convex.mpr
    have ha := (hc.add (((-(δ : ℝ)) • (innerSL ℝ u).toLinearMap).convexOn convex_univ)).add_const
      ((δ : ℝ)/2*‖u‖^2)
    convert! ha using 1
    ext x
    simp [W, norm_sub_sq_real, real_inner_comm]
    ring
  refine ⟨hWd,hstrong,hgrad,?_⟩
  apply LipschitzWith.of_dist_le_mul
  intro x y
  rw [dist_eq_norm, hgrad, hgrad]
  have he : gradient f x + (δ : ℝ) • (x-u) -
      (gradient f y + (δ : ℝ) • (y-u)) =
      (gradient f x-gradient f y) + (δ : ℝ) • (x-y) := by
    simp only [smul_sub]
    abel
  rw [he]
  have hb := hL.dist_le_mul x y
  rw [dist_eq_norm, dist_eq_norm] at hb
  calc
    _ ≤ ‖gradient f x-gradient f y‖ + ‖(δ : ℝ) • (x-y)‖ := norm_add_le _ _
    _ ≤ (β : ℝ)*‖x-y‖ + (δ : ℝ)*‖x-y‖ := by
      rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg δ.coe_nonneg]
      linarith
    _ = ((β+δ : ℝ≥0) : ℝ)*dist x y := by rw [dist_eq_norm]; simp; ring
end AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationFirstOrder

Exact module and namespace context

If next(s) halts with x, return the current state, some x, and zero queries, even when n=0. If it asks q with n=0, return state s, none, and zero queries. For a query q with positive fuel, obtain the single answer a=O(q), update to s′, and recurse with one fewer query. Preserve the final state and halt/exhaustion outcome; increment only the returned counter.

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.

def run {S Q A X : Type*} (next : S → Sum X Q) (update : S → Q → A → S)
    (oracle : Q → A) : ℕ → S → (S × Option X) × ℕ
  | fuel, s => match next s with
    | .inl x => ((s, some x), 0)
    | .inr q => match fuel with
      | 0 => ((s, none), 0)
      | n+1 =>
        let answer := oracle q
        let tail := run next update oracle n (update s q answer)
        (tail.1, tail.2+1)

set_option backward.isDefEq.respectTransparency false in
/-- Correct each original value/gradient reply using known quadratic data.
For every adaptive program and fuel, this preserves the actual regularized
execution, including its state, halt/exhaustion outcome and query count. -/

Exact module and namespace context

The compiled first-order regularization theorem computes the genuine gradient of W. Its value is W by definition. Therefore adding the known quadratic value and gradient correction to one O_f reply produces exactly O_W(x). Convexity and gradient Lipschitzness are inherited source-class premises of the reused parent; no Hessian or second derivative is needed. Induct on query allowance, for every state. Both runs inspect the same next(s). A halt or zero-fuel exhaustion returns the same result without querying. In the positive-fuel query branch, corrected and true replies update to exactly the same state. Apply the induction hypothesis there; this handles reply-dependent future queries and stopping. In the only querying branch both interpreters make one interaction and add one to the equal recursive counters. The inductive bound c≤n gives c+1≤n+1. Halt/exhaustion branches have zero cost. No externally supplied cost label or objective minimizer enters the execution.

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 simulate_regularized
    {E S X : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    (next : S → Sum X E) (update : S → E → (ℝ × E) → S)
    {f : E → ℝ} (hd : Differentiable ℝ f) (hc : ConvexOn ℝ univ f)
    {β δ : ℝ≥0} (hL : LipschitzWith β (gradient f)) (u : E) (fuel : ℕ) (s : S) :
    let W := fun x => f x + (δ : ℝ)/2*‖x-u‖^2
    let corrected := fun s x (a : ℝ × E) =>
      update s x (a.1 + (δ : ℝ)/2*‖x-u‖^2, a.2 + (δ : ℝ) • (x-u))
    let base := run next corrected (fun x => (f x, gradient f x)) fuel s
    let target := run next update (fun x => (W x, gradient W x)) fuel s
    base = target ∧ base.2 ≤ fuel := by
  dsimp only
  have hg := (QuadraticRegularizationFirstOrder.curvature_gradient_and_smoothness
    hd hc hL (δ := δ) u).2.2.1
  induction fuel generalizing s with
  | zero => cases h : next s <;> simp [run, h]
  | succ n ih =>
    cases h : next s with
    | inl x => simp [run, h]
    | inr x =>
      have step (upd : S → E → (ℝ × E) → S) (O : E → ℝ × E) :
          run next upd O (n+1) s =
            let tail := run next upd O n (upd s x (O x))
            (tail.1, tail.2+1) := by rw [run, h]
      simp only [step, hg]
      obtain ⟨he, hn⟩ := ih (update s x
        (f x + (δ : ℝ)/2*‖x-u‖^2, gradient f x + (δ : ℝ) • (x-u)))
      refine ⟨?_, Nat.succ_le_succ hn⟩
      simpa only [hg] using congrArg (fun r => (r.1, r.2+1)) he
end AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationOracle

Exact module and namespace context

The chosen positive regularization satisfies delta<=beta. The existing first-order theorem proves the actual W=f+delta||x-u||²/2 is differentiable, delta-strongly convex and has (beta+delta)-Lipschitz gradient. Weaken that Lipschitz constant to 2beta and invoke the solver with that declared parameter. This avoids replacing Phi at unequal arguments. Apply the existing compact-ball comparison theorem to continuous f and its supplied original minimizer z. It constructs a global minimizer w of the actual W, proves the original radius bound also holds for w, and provides the half-error-to-full-error implication. Do not assume that W already has a minimizer. All premises of the uniform strongly convex solver contract now hold. Its execution against the actual value/gradient oracle of W halts with some x and the required half-error. The program and its initial state were fixed before the function was quantified, so this instantiation cannot choose a new solver using W or w. Correct each original reply by the known quadratic value and gradient terms. The previous oracle simulation gives identical final state, successful output and query count, with c<=N. Apply the previously obtained value-transfer implication to this actual halted output. Exhaustion never counts as successful optimization. Positive R and epsilon justify cancellation in both budget arguments. The logarithmic ratio is exactly two; the condition-number parameter is exactly 2beta R²/epsilon. Finally log2<=1 and the nonnegative natural value Phi(q) give ceil_nat(Phi(q)log2)<=Phi(q). Thus the actual query count obeys both bounds.

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 uniform_accuracy_and_query_bound
    {E S : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [ProperSpace E]
    (β : ℝ≥0) (u : E) {R ε : ℝ} (hR : 0 < R) (hε : 0 < ε)
    (hsmall : ε ≤ (β : ℝ)*R^2) (φ : ℝ → ℕ)
    (next : S → Sum E E) (update : S → E → (ℝ × E) → S) (s₀ : S) :
    let δ : ℝ≥0 := NNReal.mk (ε/R^2) (div_pos hε (sq_pos_of_pos hR)).le
    let N := ⌈(φ ((2*(β : ℝ))/(δ : ℝ)) : ℝ) *
      Real.log ((δ : ℝ)*R^2/(ε/2))⌉₊
    (∀ g : E → ℝ, Differentiable ℝ g → StrongConvexOn univ (δ : ℝ) g →
      LipschitzWith (2*β) (gradient g) → ∀ w : E,
      IsMinOn g univ w → ‖w-u‖ ≤ R →
      ∃ t x c, run next update (fun y => (g y, gradient g y)) N s₀ =
        ((t, some x), c) ∧ g x-g w ≤ ε/2) →
    let corrected := fun s y (a : ℝ × E) =>
      update s y (a.1+(δ : ℝ)/2*‖y-u‖^2, a.2+(δ : ℝ) • (y-u))
    ∀ f : E → ℝ, Differentiable ℝ f → ConvexOn ℝ univ f →
      LipschitzWith β (gradient f) → ∀ z : E,
      IsMinOn f univ z → ‖z-u‖ ≤ R →
      ∃ t x c, run next corrected (fun y => (f y, gradient f y)) N s₀ =
        ((t, some x), c) ∧ f x-f z ≤ ε ∧
        c ≤ ⌈(φ (2*(β : ℝ)*R^2/ε) : ℝ)*Real.log 2⌉₊ ∧
        c ≤ φ (2*(β : ℝ)*R^2/ε) := by
  dsimp only
  let δ : ℝ≥0 := NNReal.mk (ε/R^2) (div_pos hε (sq_pos_of_pos hR)).le
  let N := ⌈(φ ((2*(β : ℝ))/(δ : ℝ)) : ℝ)*
    Real.log ((δ : ℝ)*R^2/(ε/2))⌉₊
  intro hs f hd hc hL z hz hr
  let W := fun x => f x+(δ : ℝ)/2*‖x-u‖^2
  have hδβ : (δ : ℝ) ≤ β := (div_le_iff₀ (sq_pos_of_pos hR)).mpr hsmall
  obtain ⟨hWd,hsc,_,hWL⟩ :=
    QuadraticRegularizationFirstOrder.curvature_gradient_and_smoothness hd hc hL (δ := δ) u
  have hWL' : LipschitzWith (2*β) (gradient W) := by
    apply LipschitzWith.of_dist_le_mul
    intro x y
    calc
      dist (gradient W x) (gradient W y) ≤ ((β+δ : ℝ≥0) : ℝ)*dist x y :=
        hWL.dist_le_mul x y
      _ ≤ ((2*β : ℝ≥0) : ℝ)*dist x y := by
        apply mul_le_mul_of_nonneg_right _ dist_nonneg
        norm_num only [NNReal.coe_add, NNReal.coe_mul, NNReal.coe_ofNat]
        linarith
  obtain ⟨w,hw,hwR,haccuracy⟩ :=
    QuadraticRegularizationTransfer.exists_minimizer_radius_and_accuracy hd.continuous hz hR hε hr
  obtain ⟨t,x,c,hex,hgap⟩ := hs W hWd hsc hWL' w hw (hwR.trans hr)
  obtain ⟨heq,hcount⟩ :=
    QuadraticRegularizationOracle.simulate_regularized next update hd hc hL (δ := δ) u N s₀
  have hout : run next
      (fun s y (a : ℝ × E) => update s y
        (a.1+(δ : ℝ)/2*‖y-u‖^2,a.2+(δ : ℝ) • (y-u)))
      (fun y => (f y,gradient f y)) N s₀ = ((t,some x),c) := heq.trans hex
  have hcN : c ≤ N := by simpa only [hout] using hcount
  have hratio : 2*(β : ℝ)/(δ : ℝ) = 2*(β : ℝ)*R^2/ε := by
    change 2*(β : ℝ)/(ε/R^2) = 2*(β : ℝ)*R^2/ε
    field_simp [ne_of_gt hε, ne_of_gt hR]
  have hlog : (δ : ℝ)*R^2/(ε/2) = 2 := by
    change ε/R^2*R^2/(ε/2) = 2
    field_simp [ne_of_gt hε, ne_of_gt hR]
  have hN : N = ⌈(φ (2*(β : ℝ)*R^2/ε) : ℝ)*Real.log 2⌉₊ := by
    simp only [N, hratio, hlog]
  have hceil : N ≤ φ (2*(β : ℝ)*R^2/ε) := by
    rw [hN, Nat.ceil_le]
    have hl : Real.log 2 ≤ 1 := by
      have := Real.log_le_sub_one_of_pos (by norm_num : (0:ℝ)<2)
      linarith
    simpa using mul_le_mul_of_nonneg_left hl
      (Nat.cast_nonneg (φ (2*(β : ℝ)*R^2/ε)) : (0:ℝ) ≤ _)
  exact ⟨t,x,c,hout,haccuracy x hgap,by simpa only [← hN] using hcN,hcN.trans hceil⟩
end AutoSamplingTheory.TechnicalLemmas.Analysis.UniformRegularization

Exact module and namespace context