Lipschitz growth bounds every supplied subgradient
AutoSamplingTheory.TechnicalLemmas.Analysis.SubgradientMethod.norm_le_of_supportsAt · theorem · Teaching coverage
Mathematical statement
For any globally G-Lipschitz real-valued function on a real inner-product space, every global supporting vector v at x satisfies ‖v‖≤G.
Lean statement · norm_le_of_supportsAt
A supplied global supporting vector of a globally G-Lipschitz objective has norm at most G.
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 norm_le_of_supportsAt {f : E → ℝ} {G : ℝ≥0} {x g : E}
(hf : LipschitzWith G f) (hs : SupportsAt f x g) : ‖g‖ ≤ (G : ℝ)Proof roadmap
- 1Probe in the supporting direction
Evaluate the global supporting inequality at z=x+v. The pairing is exactly ‖v‖², with no derivative or inverse norm needed.
- 2Use the actual Lipschitz bound
The function increment is at most its absolute value, and global Lipschitz continuity bounds that absolute value by G‖v‖.
- 3Keep the zero vector separate
If v=0 the result is nonnegativity of G. Otherwise ‖v‖>0, so the quadratic inequality implies ‖v‖≤G. This is the same bound as the upstream normalized-direction argument, with a division-free proof.
Full assumptions and notation
All objects and hypotheses
- E is a real inner-product space with its associated norm. No completeness or finite-dimensionality assumption is imposed.
- G is a nonnegative real Lipschitz constant and f:E→ℝ is globally G-Lipschitz.
- SupportsAt f x v means f(x)+⟨v,z−x⟩≤f(z) for every z∈E. It supplies a genuine global supporting vector; no differentiability or totalized gradient is used.
Mathematical proof
1. Probe in the supporting direction
Evaluate the global supporting inequality at z=x+v. The pairing is exactly ‖v‖², with no derivative or inverse norm needed.
Corresponding Lean step
SupportsAt evaluated at x+g; real_inner_self_eq_norm_sq.
2. Use the actual Lipschitz bound
The function increment is at most its absolute value, and global Lipschitz continuity bounds that absolute value by G‖v‖.
Corresponding Lean step
LipschitzWith.dist_le_mul; Real.dist_eq; le_abs_self.
3. Keep the zero vector separate
If v=0 the result is nonnegativity of G. Otherwise ‖v‖>0, so the quadratic inequality implies ‖v‖≤G. This is the same bound as the upstream normalized-direction argument, with a division-free proof.
Corresponding Lean step
norm_nonneg; zero/nonzero split; nlinarith.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · norm_le_of_supportsAt
Probe at x+v, compare the quadratic lower growth with Lipschitz upper growth, and separate the zero-norm case.
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 norm_le_of_supportsAt {f : E → ℝ} {G : ℝ≥0} {x g : E}
(hf : LipschitzWith G f) (hs : SupportsAt f x g) : ‖g‖ ≤ (G : ℝ) := by
have hs' := hs (x + g)
change f x + inner ℝ g (x + g - x) ≤ f (x + g) at hs'
rw [add_sub_cancel_left, real_inner_self_eq_norm_sq] at hs'
have hl : f (x + g) - f x ≤ (G : ℝ) * ‖g‖ := by
calc
f (x + g) - f x ≤ |f (x + g) - f x| := le_abs_self _
_ ≤ (G : ℝ) * ‖g‖ := by
simpa [Real.dist_eq, dist_eq_norm] using hf.dist_le_mul (x + g) x
by_cases hg : ‖g‖ = 0
· simp [hg]
· have hp : 0 < ‖g‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hg)
nlinarithScope and omitted-condition boundaries
- No existence or measurable selection of supporting vectors is claimed. The theorem does not require convexity once a global supporting vector is supplied, just as the corresponding upstream direction.
- This is a native local port of the norm bound, not a bulk import of Optlib or a sampling convergence result.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- LipschitzWith.dist_le_mul
- real_inner_self_eq_norm_sq
- Real.dist_eq
- norm_nonneg
Mathematical sources
- Optlib Lipschitz_to_bounded_subgradient — Apache-2.0 source norm bound; native proof rewritten over Samplinglib SupportsAt.
- Nonsmooth absolute-value iteration and endpoint tests — Focused consumers of the actual new theorems.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.