Why a global Lipschitz function bounds its supporting vectors

1. Because the support relation is global, its test point may be \(y=x+g\). Thus \[\|g\|^2=\langle g,g\rangle\le f(x+g)-f(x).\] This tests the supplied relation; it does not use a theorem constructing subgradients.

2. Global Lipschitz growth and the absolute-value bound give \[f(x+g)-f(x)\le|f(x+g)-f(x)|\le G\|g\|.\] Combining the inequalities yields \(\|g\|^2\le G\|g\|\).

3. If \(g=0\) the conclusion is immediate from \(G\ge 0\). Otherwise \(\|g\|>0\), so division by this strictly positive number gives \(\|g\|\le G\). No completeness, differentiability or finite-dimensional compactness is used.

4. For constrained support take \(E=\mathbb{R}\), f≡0, \(G=0\), C=[0,∞), \(x=0\) and \(g=-1\). Then \[f(0)+g(y-0)=-y\le0=f(y)\qquad(y\in C),\] but \(\|g\|=1>0=G\). The chosen point \(x+g=-1\) is outside C. This refutes the constrained variant, not the globally quantified theorem.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSubgradient
import Mathlib.Topology.MetricSpace.Lipschitz
import Mathlib.Data.Finset.Max
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring

/- Copyright (c) 2024 Hongjia Chen, Chenyi Li, Wanyi He, Zaiwen Wen.
Released under Apache 2.0; retain LICENSE and NOTICE.
Upstream Optlib 5da27c5f95aa6a8a45b8c14b968ade4c13ff18c3,
Optlib/Algorithm/SubgradientMethod.lean:80–118,137–232.
Modified for Samplinglib: native Lean 4.33.0, global SupportsAt and unbundled inputs. -/
open AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSubgradient
open scoped NNReal RealInnerProductSpace
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

example {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)
    nlinarith

1. Uses the globally admissible point \(y=x+g\) to obtain the exact squared-norm lower bound without assuming subgradient existence. (1 point)
2. Applies global Lipschitz growth to bound the same increment by G times the norm. (1 point)
3. Separates the zero case before dividing, retaining only the stated inner-product-space hypotheses. (1 point)
4. Gives any valid constrained-support counterexample with globally Lipschitz f, checks its support and failed norm bound, and explains the unavailable global test point; the reference half-line example is sufficient, not required. (1 point)

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSubgradient
import Mathlib.Topology.MetricSpace.Lipschitz
import Mathlib.Data.Finset.Max
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring

/- Copyright (c) 2024 Hongjia Chen, Chenyi Li, Wanyi He, Zaiwen Wen.
Released under Apache 2.0; retain LICENSE and NOTICE.
Upstream Optlib 5da27c5f95aa6a8a45b8c14b968ade4c13ff18c3,
Optlib/Algorithm/SubgradientMethod.lean:80–118,137–232.
Modified for Samplinglib: native Lean 4.33.0, global SupportsAt and unbundled inputs. -/
open AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSubgradient
open scoped NNReal RealInnerProductSpace
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

example {f : E → ℝ} {G : ℝ≥0} {x g : E}
    (hf : LipschitzWith G f) (hs : SupportsAt f x g) : ‖g‖ ≤ (G : ℝ) := by
  -- Replace this comment with your proof.

Download task template

The reference tests hs at x+g, rewrites the inner product with itself as a squared norm, and obtains the upper increment bound with hf.dist_le_mul. It splits on a zero norm before the final ordered-field inference. SupportsAt is the existing global relation from ConvexSubgradient, not a new predicate. The source module is not imported into the task, and its norm theorem is not supplied as a premise. The Lean conclusion covers the norm bound only; the constrained counterexample is the separate prose audit.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSubgradient
import Mathlib.Topology.MetricSpace.Lipschitz
import Mathlib.Data.Finset.Max
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity
import Mathlib.Tactic.Ring

/- Copyright (c) 2024 Hongjia Chen, Chenyi Li, Wanyi He, Zaiwen Wen.
Released under Apache 2.0; retain LICENSE and NOTICE.
Upstream Optlib 5da27c5f95aa6a8a45b8c14b968ade4c13ff18c3,
Optlib/Algorithm/SubgradientMethod.lean:80–118,137–232.
Modified for Samplinglib: native Lean 4.33.0, global SupportsAt and unbundled inputs. -/
open AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSubgradient
open scoped NNReal RealInnerProductSpace
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

example {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)
    nlinarith

Download runnable reference