A regularized minimizer exists and transfers approximation accuracy
AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationTransfer.exists_minimizer_radius_and_accuracy · theorem · Teaching coverage
Statement
E is a normed additive commutative group whose closed metric balls are compact (ProperSpace). The function f:E→R is continuous. A global minimizer z of f is supplied: f(z)<=f(x) for every x. The center x0 and positive real numbers R,epsilon satisfy ||z-x0||<=R. Set delta=epsilon/R² and W(x)=f(x)+delta||x-x0||²/2. The theorem constructs a global minimizer w of this same W; it does not assume a regularized minimizer, convexity or differentiability. There exists such a w with the radius bound below, and every epsilon/2-accurate regularized point is epsilon-accurate for f.
All objects and hypotheses
- E is a normed additive commutative group whose closed metric balls are compact (ProperSpace). The function f:E→R is continuous.
- A global minimizer z of f is supplied: f(z)<=f(x) for every x. The center x0 and positive real numbers R,epsilon satisfy ||z-x0||<=R.
- Set delta=epsilon/R² and W(x)=f(x)+delta||x-x0||²/2. The theorem constructs a global minimizer w of this same W; it does not assume a regularized minimizer, convexity or differentiability.
Mathematical proof
1. Minimize on a compact ball
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).
Corresponding Lean step
isCompact_closedBall; IsCompact.exists_isMinOn; continuity of distance and its square. Properness is used here.
2. Upgrade to a global minimum
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.
Corresponding Lean step
Membership split for closedBall, dist_eq_norm, positive scalar multiplication and the supplied IsMinOn f Set.univ z.
3. Compare the two minimizer radii
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.
Corresponding Lean step
The same compactly constructed w and W(w)<=W(z); positive-coefficient algebra and norm_nonneg.
4. Transfer an approximate regularized value
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.
Corresponding Lean step
Uniform all-x implication for the same witness w; δ=ε/R² and R>0 justify cancellation, with no totalized division assumption.
Lean statement · exists_minimizer_radius_and_accuracy
Existence of one actual W-minimizer, its sharp radius comparison and an all-points approximation implication.
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 ≤ εLean proof · exists_minimizer_radius_and_accuracy
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.QuadraticRegularizationTransferScope and omitted-condition boundaries
- This establishes the regularized-minimum existence, radius comparison and objective-accuracy transfer in Lemma4.2. It does not prove regularized strong convexity or smoothness, an optimizer implementation, query complexity or the complete class-level reduction.
- The proper normed-group formulation generalizes the source Euclidean geometry. Continuity suffices for this comparison component, so convexity and beta-smoothness are not formal assumptions here. Closed-ball compactness is explicit; no result for arbitrary complete infinite-dimensional Hilbert spaces is asserted.
- The original global minimizer is supplied; the regularized one is constructed. Uniqueness is not claimed in the broader continuous, possibly nonconvex setting. Positive R and epsilon ensure positive delta; the literal R=0 branch is outside this declaration.
- The approximation implication is a value-transfer interface, not a claim that every numerical method satisfies its input gap. Tests use an actual gradient step on a quadratic regularized objective to supply that gap without giving the algorithm the constructed minimizer.
- Existing C2/Hessian QuadraticRegularization and the stronger SPHMC proximal constructor were searched. They do not supply this weaker-assumption interface and are not claimed as invoked dependencies. Future curvature/smoothness and oracle-cost work must preserve the source regularity and budget conventions.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- IsCompact.exists_isMinOn
- isCompact_closedBall
- Metric.mem_closedBall
- dist_eq_norm
- Continuous.dist
- norm_nonneg
Mathematical sources
- Chewi Lemma4.2 proof — Regularized objective, minimizer-radius comparison and two half-error terms; full reduction remains separate.
- Actual one-step gradient consumer — Quadratic regularized gradient step with arbitrary positive epsilon; output does not receive the minimizer witness.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.