/- 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.