Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

Integrate the Hessian along a segment

AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC2.gradient_sub_inner_eq_integral_fderiv2 · theorem · Teaching coverage

Statement

For every C² real-valued f on a complete real inner-product space and every x,v, the gradient difference between x+v and x, paired with v, equals the integral of the Hessian quadratic form along that segment.

\[\langle\nabla f(x+v)-\nabla f(x),v\rangle=\int_0^1 D^2f(x+tv)[v,v]\,dt.\]

All objects and hypotheses

  • E is a complete real inner-product space; f:E→ℝ is twice continuously Fréchet differentiable everywhere.
  • The Hessian quadratic form means the genuine second derivative D²f(x)[v,v]=(fderiv ℝ (fderiv ℝ f) x v) v. The pairing with the actual gradient equals Df(x)[v].
  • x,v∈E are arbitrary, including v=0. The integral uses real Lebesgue measure on [0,1].

Mathematical proof

1. Differentiate the scalar gradient pairing

Set g(t)=Df(x+tv)[v]. Because f is C², Df is C¹; compose its derivative with the affine segment and evaluate the resulting linear functional at the fixed v.

\[g(t)=Df(x+tv)[v],\qquad g^{\prime}(t)=D^2f(x+tv)[v,v].\]
Corresponding Lean step

hfd uses ContDiff.fderiv_right. hd uses HasFDerivAt.comp_hasDerivAt and HasDerivAt.clm_apply.

2. Integrate the genuine derivative

The second derivative is continuous. Composition with the segment and two evaluations preserve continuity, giving interval integrability. FTC gives g(1)−g(0). The gradient pairing identity identifies the endpoints.

\[\int_0^1g^{\prime}(t)\,dt=g(1)-g(0)=\langle\nabla f(x+v)-\nabla f(x),v\rangle.\]
Corresponding Lean step

hc: ContDiff.continuous_fderiv and Continuous.clm_apply; Continuous.intervalIntegrable and intervalIntegral.integral_eq_sub_of_hasDerivAt; gradient/Riesz simplification.

Lean statement · gradient_sub_inner_eq_integral_fderiv2

For every C² real-valued f on a complete real inner-product space and every x,v, the gradient difference between x+v and x, paired with v, equals the integral of the Hessian quadratic form along that segment.

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 gradient_sub_inner_eq_integral_fderiv2
    {f : E → ℝ} (hf : ContDiff ℝ 2 f) (x v : E) :
    inner ℝ (gradient f (x + v) - gradient f x) v =
      ∫ t : ℝ in 0..1, (fderiv ℝ (fderiv ℝ f) (x + t • v) v) v

Exact module and namespace context

Lean proof · gradient_sub_inner_eq_integral_fderiv2

Set g(t)=Df(x+tv)[v]. Because f is C², Df is C¹; compose its derivative with the affine segment and evaluate the resulting linear functional at the fixed v. The second derivative is continuous. Composition with the segment and two evaluations preserve continuity, giving interval integrability. FTC gives g(1)−g(0). The gradient pairing identity identifies the endpoints.

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 gradient_sub_inner_eq_integral_fderiv2
    {f : E → ℝ} (hf : ContDiff ℝ 2 f) (x v : E) :
    inner ℝ (gradient f (x + v) - gradient f x) v =
      ∫ t : ℝ in 0..1, (fderiv ℝ (fderiv ℝ f) (x + t • v) v) v := by
  have hfd : ContDiff ℝ 1 (fderiv ℝ f) := hf.fderiv_right (by norm_num)
  have hd (t : ℝ) : HasDerivAt (fun s : ℝ => fderiv ℝ f (x + s • v) v)
      ((fderiv ℝ (fderiv ℝ f) (x + t • v) v) v) t := by
    convert ((hfd.differentiable_one _).hasFDerivAt.comp_hasDerivAt t
      (((hasDerivAt_id t).smul_const v).const_add x)).clm_apply
      (hasDerivAt_const t v) using 1 <;> first | rfl | simp
  have hc : Continuous (fun t : ℝ => (fderiv ℝ (fderiv ℝ f) (x + t • v) v) v) :=
    (((hfd.continuous_fderiv (by norm_num)).comp
      (continuous_const.add (continuous_id.smul continuous_const))).clm_apply
        continuous_const).clm_apply continuous_const
  simpa [inner_sub_left, gradient, Function.comp_def] using
    (intervalIntegral.integral_eq_sub_of_hasDerivAt
      (fun t _ => hd t) (hc.intervalIntegrable 0 1)).symm

/-- Global quantitative gradient monotonicity is equivalent to the genuine
Hessian diagonal lower bound, by a right derivative limit and the FTC. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • The source segment identity generalized from Euclidean space to complete real inner-product space. No convexity or Hessian bound is assumed.

Source and reuse

ASTIS parents called

    Mathlib API called (external library)

    • ContDiff.fderiv_right; ContDiff.differentiable_one; ContDiff.continuous_fderiv
    • HasFDerivAt.comp_hasDerivAt; HasDerivAt.clm_apply; Continuous.clm_apply
    • Continuous.intervalIntegrable; intervalIntegral.integral_eq_sub_of_hasDerivAt; InnerProductSpace.toDual_symm_apply

    Mathematical sources

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