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

Integrate the gradient along a segment

AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC1.sub_eq_integral_gradient · theorem · Teaching coverage

Statement

For every x,v in a complete real inner-product space and every C¹ real-valued f, the difference f(x+v)−f(x) equals the integral of the gradient pairing along that segment.

\[f(x+v)-f(x)=\int_0^1\langle\nabla f(x+sv),v\rangle\,ds.\]

All objects and hypotheses

  • E is a complete real inner-product space and f:E→ℝ is continuously Fréchet differentiable on all E.
  • gradient f is the genuine gradient supplied by C¹, not an unsupported totalized derivative.
  • x,v∈E are arbitrary, including v=0; the integral is with respect to Lebesgue measure on [0,1].

Mathematical proof

1. Differentiate the affine segment

C¹ gives a genuine derivative of f at every point. The chain rule differentiates the composition with x+sv, including the two endpoints.

\[\frac{d}{ds}f(x+sv)=\langle\nabla f(x+sv),v\rangle.\]
Corresponding Lean step

hd: DifferentiableAt.hasGradientAt, HasFDerivAt.comp_hasDerivAt and the derivative of x+s•v.

2. Establish integrability, then apply FTC

The derivative map is continuous because f is C¹. Evaluating it on the fixed direction v and composing with the segment gives a continuous scalar integrand; compact-interval integrability follows. FTC and the values at 0 and 1 give the identity.

\[\int_0^1\frac{d}{ds}f(x+sv)\,ds=f(x+v)-f(x).\]
Corresponding Lean step

hc uses ContDiff.continuous_fderiv and Continuous.clm_apply; Continuous.intervalIntegrable and intervalIntegral.integral_eq_sub_of_hasDerivAt finish.

Lean statement · sub_eq_integral_gradient

For every x,v in a complete real inner-product space and every C¹ real-valued f, the difference f(x+v)−f(x) equals the integral of the gradient pairing 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 sub_eq_integral_gradient {f : E → ℝ} (hf : ContDiff ℝ 1 f) (x v : E) :
    f (x + v) - f x = ∫ s : ℝ in 0..1, inner ℝ (gradient f (x + s • v)) v

Exact module and namespace context

Lean proof · sub_eq_integral_gradient

C¹ gives a genuine derivative of f at every point. The chain rule differentiates the composition with x+sv, including the two endpoints. The derivative map is continuous because f is C¹. Evaluating it on the fixed direction v and composing with the segment gives a continuous scalar integrand; compact-interval integrability follows. FTC and the values at 0 and 1 give the identity.

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

/-- Quantitative gradient monotonicity implies the chord inequality by the
source's two affine-segment FTC identities and integration of their difference.
The modulus can be signed; no Hessian or extra integrability is assumed. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • A reusable Hilbert-space generalization of the segment identity used in the source; no convexity, Hessian, infinite-time integral or measure on E is asserted.

Source and reuse

ASTIS parents called

    Mathlib API called (external library)

    • ContDiff.continuous_fderiv; Continuous.clm_apply; InnerProductSpace.toDual_symm_apply
    • DifferentiableAt.hasGradientAt; HasFDerivAt.comp_hasDerivAt
    • Continuous.intervalIntegrable; intervalIntegral.integral_eq_sub_of_hasDerivAt

    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.