Samplinglib mathematical lesson

A nonlinear parametrization preserves a numerical PL bound

AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexPLPullback.exists_minimizer_and_pl · theorem · Teaching coverage

Read this first

Mathematical statement

Let E and F be complete real inner-product spaces, f:F→R and g:E→F be everywhere Frechet differentiable, alpha>0 and sigma≥0. Assume f is globally alpha-strongly convex, z is its global minimizer, g is surjective, and the derivative satisfies the following quadratic-form bound at every x and every v in F. Then there is a minimizing preimage xstar and the actual composite gradient satisfies the stated numerical PL inequality.

\[\begin{gathered}A_x=Dg(x),\qquad\langle v,A_xA_x^*v\rangle\ge\sigma\|v\|^2\quad(\forall x\in E,\ v\in F),\\\exists x_\star\in E:\quad g(x_\star)=z,\quad x_\star\in\arg\min(f\circ g),\\2\alpha\sigma\big((f\circ g)(x)-(f\circ g)(x_\star)\big)\le\|\nabla(f\circ g)(x)\|^2\quad(\forall x\in E).\end{gathered}\]

Lean statement · exists_minimizer_and_pl

Construct a preimage of the base minimizer and prove a global numerical gradient-gap inequality for the actual composition.

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.

Download module (.lean)

theorem exists_minimizer_and_pl {f : F → ℝ} {g : E → F} {α σ : ℝ} {z : F}
    (hα : 0 < α) (hσ : 0 ≤ σ) (hsc : StrongConvexOn univ α f)
    (hf : Differentiable ℝ f) (hg : Differentiable ℝ g)
    (hsurj : Function.Surjective g) (hz : IsMinOn f univ z)
    (hjac : ∀ x v, σ * ‖v‖ ^ 2 ≤
      inner ℝ v ((fderiv ℝ g x) ((fderiv ℝ g x).adjoint v))) :
    ∃ xstar, g xstar = z ∧ IsMinOn (f ∘ g) univ xstar ∧
      ∀ x, 2 * (α * σ) * ((f ∘ g) x - (f ∘ g) xstar) ≤
        ‖gradient (f ∘ g) x‖ ^ 2

Exact module and namespace context

Proof roadmap

1Lift the attained minimum
Let z be the supplied global minimizer of f. Surjectivity gives xstar with g(xstar)=z. Every g(x) lies in the objective space, so f(g(xstar))=f(z)≤f(g(x)); thus the same xstar minimizes the composite.
2Turn strong convexity into a gradient-gap bound
At y=g(x), the shared first-order strong-convexity bound at comparator z gives the gap at most <grad f(y),y-z> minus alpha times the squared distance divided by2. Cauchy-Schwarz bounds the inner product. The nonnegative square (norm grad f(y)−alpha norm(y−z))² yields the numerical PL bound for f.
3Identify the actual composite gradient
Put A_x=Dg(x). The Frechet chain rule gives D(f∘g)(x)[v]=<grad f(g(x)),A_x v>. The defining adjoint identity rewrites this as <A_x-adjoint grad f(g(x)),v>. Uniqueness of the Riesz representative identifies the actual composite gradient.
4Transport the coercivity constant
Apply the assumed operator lower bound to v=grad f(g(x)). Its quadratic form equals norm(A_x-adjoint v)² by the adjoint identity. Multiply the base gradient-gap bound by nonnegative sigma and combine. Finally use g(xstar)=z to express the same gap relative to the attained composite minimum.

Full assumptions and notation

All objects and hypotheses

E,F are real complete inner-product spaces. f:F→R and g:E→F are Frechet differentiable at every point; continuity of their derivatives is not assumed.
Alpha>0 and sigma≥0 are real constants. StrongConvexOn univ alpha f supplies the global strong convexity inequality.
A supplied z:F satisfies f(z)≤f(y) for all y:F. The map g is surjective.
For every x:E and v:F, sigma||v||²≤<v,Dg(x)(Dg(x)-adjoint v)>. This is a bound on the actual Frechet derivative, not on a supplied gradient of the composite.

Mathematical proof

1. Lift the attained minimum

Let z be the supplied global minimizer of f. Surjectivity gives xstar with g(xstar)=z. Every g(x) lies in the objective space, so f(g(xstar))=f(z)≤f(g(x)); thus the same xstar minimizes the composite.

\[g(x_\star)=z,\qquad (f\circ g)(x_\star)=f(z)\le f(g(x)).\]

Corresponding Lean step

Function.Surjective applied to z; IsMinOn transported pointwise.

2. Turn strong convexity into a gradient-gap bound

At y=g(x), the shared first-order strong-convexity bound at comparator z gives the gap at most <grad f(y),y-z> minus alpha times the squared distance divided by2. Cauchy-Schwarz bounds the inner product. The nonnegative square (norm grad f(y)−alpha norm(y−z))² yields the numerical PL bound for f.

\[\begin{gathered}f(y)-f(z)\le\langle\nabla f(y),y-z\rangle-\frac\alpha2\|y-z\|^2\\\le\|\nabla f(y)\|\|y-z\|-\frac\alpha2\|y-z\|^2,\\2\alpha(f(y)-f(z))\le\|\nabla f(y)\|^2.\end{gathered}\]

Corresponding Lean step

StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn, real_inner_le_norm, sq_nonneg and positive alpha.

3. Identify the actual composite gradient

Put A_x=Dg(x). The Frechet chain rule gives D(f∘g)(x)[v]=<grad f(g(x)),A_x v>. The defining adjoint identity rewrites this as <A_x-adjoint grad f(g(x)),v>. Uniqueness of the Riesz representative identifies the actual composite gradient.

\[\nabla(f\circ g)(x)=A_x^*\nabla f(g(x)),\qquad A_x=Dg(x).\]

Corresponding Lean step

HasFDerivAt.comp; hasGradientAt_iff_hasFDerivAt; InnerProductSpace.toDual_apply_apply; ContinuousLinearMap.adjoint_inner_left; HasGradientAt.gradient.

4. Transport the coercivity constant

Apply the assumed operator lower bound to v=grad f(g(x)). Its quadratic form equals norm(A_x-adjoint v)² by the adjoint identity. Multiply the base gradient-gap bound by nonnegative sigma and combine. Finally use g(xstar)=z to express the same gap relative to the attained composite minimum.

\[\begin{aligned}\|\nabla(f\circ g)(x)\|^2&=\langle v,A_xA_x^*v\rangle\ge\sigma\|v\|^2\\&\ge2\alpha\sigma\big((f\circ g)(x)-(f\circ g)(x_\star)\big).\end{aligned}\]

Corresponding Lean step

ContinuousLinearMap.adjoint_inner_left; real_inner_self_eq_norm_sq; mul_le_mul_of_nonneg_left.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · exists_minimizer_and_pl

Let z be the supplied global minimizer of f. Surjectivity gives xstar with g(xstar)=z. Every g(x) lies in the objective space, so f(g(xstar))=f(z)<=f(g(x)); thus the same xstar minimizes the composite. At y=g(x), the shared first-order strong-convexity bound at comparator z gives the gap at most <grad f(y),y-z> minus alpha times the squared distance divided by2. Cauchy-Schwarz bounds the inner product. The nonnegative square (norm grad f(y)−alpha norm(y−z))² yields the numerical PL bound for f. Put A_x=Dg(x). The Frechet chain rule gives D(f∘g)(x)[v]=<grad f(g(x)),A_x v>. The defining adjoint identity rewrites this as <A_x-adjoint grad f(g(x)),v>. Uniqueness of the Riesz representative identifies the actual composite gradient. Apply the assumed operator lower bound to v=grad f(g(x)). Its quadratic form equals norm(A_x-adjoint v)² by the adjoint identity. Multiply the base gradient-gap bound by nonnegative sigma and combine. Finally use g(xstar)=z to express the same gap relative to the attained composite minimum.

Download module (.lean)

theorem exists_minimizer_and_pl {f : F → ℝ} {g : E → F} {α σ : ℝ} {z : F}
    (hα : 0 < α) (hσ : 0 ≤ σ) (hsc : StrongConvexOn univ α f)
    (hf : Differentiable ℝ f) (hg : Differentiable ℝ g)
    (hsurj : Function.Surjective g) (hz : IsMinOn f univ z)
    (hjac : ∀ x v, σ * ‖v‖ ^ 2 ≤
      inner ℝ v ((fderiv ℝ g x) ((fderiv ℝ g x).adjoint v))) :
    ∃ xstar, g xstar = z ∧ IsMinOn (f ∘ g) univ xstar ∧
      ∀ x, 2 * (α * σ) * ((f ∘ g) x - (f ∘ g) xstar) ≤
        ‖gradient (f ∘ g) x‖ ^ 2 := by
  obtain ⟨xstar, hxstar⟩ := hsurj z
  refine ⟨xstar, hxstar, ?_, ?_⟩
  · intro x _
    simpa [Function.comp_def, hxstar] using hz (mem_univ (g x))
  · intro x
    have hfirst := StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn
      hsc (fun y _ => (hf y).hasGradientAt) (mem_univ (g x)) (mem_univ z)
    have hcs := real_inner_le_norm (gradient f (g x)) (g x - z)
    have hbase : 2 * α * (f (g x) - f z) ≤ ‖gradient f (g x)‖ ^ 2 := by
      rw [← neg_sub (g x) z, inner_neg_right, norm_neg] at hfirst
      nlinarith [sq_nonneg (‖gradient f (g x)‖ - α * ‖g x - z‖)]
    have hchain : HasGradientAt (f ∘ g)
        ((fderiv ℝ g x).adjoint (gradient f (g x))) x := by
      apply hasGradientAt_iff_hasFDerivAt.mpr
      have hc := (hf (g x)).hasGradientAt.hasFDerivAt.comp x (hg x).hasFDerivAt
      have heq : (InnerProductSpace.toDual ℝ F (gradient f (g x))).comp (fderiv ℝ g x) =
          InnerProductSpace.toDual ℝ E ((fderiv ℝ g x).adjoint (gradient f (g x))) := by
        ext v
        simp [InnerProductSpace.toDual_apply_apply, ContinuousLinearMap.adjoint_inner_left]
      rw [heq] at hc
      exact hc
    have hcoerc := hjac x (gradient f (g x))
    rw [← ContinuousLinearMap.adjoint_inner_left, real_inner_self_eq_norm_sq] at hcoerc
    have hmul := mul_le_mul_of_nonneg_left hbase hσ
    rw [hchain.gradient]
    dsimp only [Function.comp_def]
    rw [hxstar]
    nlinarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexPLPullback

Exact module and namespace context

Scope and omitted-condition boundaries

The conclusion is the numerical PL inequality and a lifted global minimizer. Definition2.5 additionally asks for a continuously differentiable objective and a positive PL constant. The exercise does not explicitly impose continuity of Dg or sigma>0. Neither is silently inferred here: sigma=0 is a degenerate inequality, and continuous differentiability of the composite remains a separate obligation.
Real complete Hilbert spaces and everywhere Frechet differentiability generalize the source finite Euclidean spaces and Section2 C2 objective convention. Completeness provides Riesz gradients and adjoints. No infinite-dimensional minimizer-existence theorem is claimed: the source attained minimizer z of f is supplied and surjectivity constructs its preimage.
The source uses a d-by-n Jacobian J, transposed relative to Dg:R^d to R^n. Here A=Dg and J corresponds to A-adjoint, so J-transpose J corresponds to A A-adjoint. The assumed operator quadratic form is exactly the adjoint norm square. It is not a lower bound on A on the parameter space. No compiled matrix-coordinate identification theorem is asserted.
No convexity, uniqueness or multiplicity of composite minimizers, gradient Lipschitz upper bound, gradient-descent rate, Riemannian statement or companion-paper completion follows. The gradient of the composite and its minimum are conclusions, not supplied certificates.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn

Mathlib API called (external library)

HasFDerivAt.comp
hasGradientAt_iff_hasFDerivAt
ContinuousLinearMap.adjoint_inner_left
real_inner_le_norm
mul_le_mul_of_nonneg_left

Mathematical sources

Chewi Exercise2.3, Definition2.5 and Section2 conventions — Numerical inequality component; the positive-modulus and C1 definition package is kept separate.
Actual nonlinear parametrization test — Instantiates the theorem with a nonlinear surjection and proves its derivative/minimum certificates.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.