StrongConvexPLPullback: mathematical reading route

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.

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_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