Samplinglib mathematical lesson

The genuine Hessian integral represents the full gradient difference

AutoSamplingTheory.TechnicalLemmas.Analysis.HessianSecantOperator.hessian_secant_operator · theorem · Teaching coverage

Read this first

Mathematical statement

For every complete real inner-product space E, every globally C2 real f with signed global genuine-Hessian diagonal bounds alpha,beta, and all x,y, let phi(t) be the Riesz operator of D2f(y+t(x-y)) and H=integral_0^1 phi(t) dt in ordinary Lebesgue measure. Then phi is interval integrable, gradient f x-gradient f y=H(x-y), H is symmetric, all v satisfy alpha||v||^2≤inner(Hv,v)≤beta||v||^2, and ||H||op≤max(|alpha|,|beta|). In finite Euclidean space this specializes to the source actual H with alpha=1/(2kappa),beta=1; V_eta smoothness/curvature must still be proved separately.

\[H(x,y)=\int_0^1[D^2f(y+t(x-y))]^{\sharp}\,dt,\quad\nabla f(x)-\nabla f(y)=H(x,y)(x-y),\quad\alpha I\preceq H\preceq\beta I,\quad\|H\|_{\rm op}\le\max(|\alpha|,|\beta|).\]

Lean statement · hessian_secant_operator

Exact nested genuine Frechet derivative, Riesz operator and ordinary unit-interval Bochner integral; all-vector identity and signed bounds.

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 hessian_secant_operator {f : E → ℝ} {α β : ℝ}
    (hf : ContDiff ℝ 2 f)
    (hlo : ∀ z v, α * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ f) z v) v)
    (hup : ∀ z v, (fderiv ℝ (fderiv ℝ f) z v) v ≤ β * ‖v‖ ^ 2)
    (x y : E) :
    let φ := fun t : ℝ => continuousLinearMapOfBilin
      (fderiv ℝ (fderiv ℝ f) (y + t • (x - y)))
    let H := ∫ t : ℝ in 0..1, φ t
    IntervalIntegrable φ volume 0 1 ∧
      gradient f x - gradient f y = H (x - y) ∧
      H.IsSymmetric ∧
      (∀ v, α * ‖v‖ ^ 2 ≤ inner ℝ (H v) v ∧
        inner ℝ (H v) v ≤ β * ‖v‖ ^ 2) ∧
      ‖H‖ ≤ max |α| |β|

Exact module and namespace context

Proof roadmap

1Construct the actual operator and derive regularity
Represent each genuine second derivative by the continuous Riesz map, using Mathlib continuousLinearMapOfBilin. C2 makes Df C1 and D2f continuous. Composing with the affine segment and fixed continuous Riesz map gives a continuous operator-valued phi; hence its ordinary unit-interval Bochner integral exists. No matrix or integrability certificate is supplied.
2Commute genuine integral evaluation and arbitrary pairing
Continuous evaluation and the fixed continuous linear functional inner(w,.) commute with the actual Bochner integral. Real symmetry of the inner product turns this into the displayed all-vector identity. Both integral commutations use the derived interval integrability.
3Derive the full gradient secant identity by FTC
Put v=x-y. For any w, differentiating t → Df(y+t v)[w] gives D2f(y+t v)[v,w]. Its continuity supplies scalar integrability. The ordinary FTC gives the difference Df(x)[w]-Df(y)[w]; Riesz identifies it with inner(gradient f x-gradient f y,w). Equality against every w yields the full vector equality, not merely its diagonal pairing.
4Inherit genuine symmetry
C2 supplies symmetry of the actual second derivative. The all-vector pairing identity shows inner(Hv,w)=inner(Hw,v)=inner(v,Hw). This does not assume self-adjointness of an unrelated matrix.
5Integrate the actual two diagonal bounds
For each v, integrate the constant bounds alpha||v||^2 and beta||v||^2 against ordinary Lebesgue measure on the unit interval. Integral monotonicity and hinner give the inherited inequalities. Signed moduli and dimension zero require no extra positivity or order hypothesis.
6Control the actual operator norm
For the symmetric H, Mathlib identifies its norm with the supremum of absolute Rayleigh quotients. For nonzero v, the previous signed inequalities bound their absolute value by max(|alpha|,|beta|); v=0 gives zero. This proves the stated norm bound even on the zero space. In the paper alpha=1/(2kappa),beta=1,kappa≥1 gives norm≤1 once its curvature premises are produced.

Full assumptions and notation

All objects and hypotheses

E is a complete real inner-product space (a real Hilbert space), including dimension zero. f:E→R is globally C2 in the Frechet sense. x,y and every test vector range over all E.
alpha,beta are real and may be signed. For every z,v, alpha||v||^2 ≤ D2f(z)[v,v] ≤ beta||v||^2. These are bounds on the genuine nested Frechet derivative, not on an independently supplied operator.
H(x,y) is the ordinary Lebesgue Bochner integral on[0,1] of the Riesz-represented D2f(y+t(x-y)). Its symmetry, continuity/measurability/integrability and secant identity are conclusions derived from C2, not hypotheses. Completeness permits the Riesz identification and Bochner operator integral.

Mathematical proof

1. Construct the actual operator and derive regularity

Represent each genuine second derivative by the continuous Riesz map, using Mathlib continuousLinearMapOfBilin. C2 makes Df C1 and D2f continuous. Composing with the affine segment and fixed continuous Riesz map gives a continuous operator-valued phi; hence its ordinary unit-interval Bochner integral exists. No matrix or integrability certificate is supplied.

\[\phi(t)=[D^2f(y+t(x-y))]^\sharp,\qquad\langle\phi(t)v,w\rangle=D^2f(y+t(x-y))[v,w].\]

Corresponding Lean step

hf.fderiv_right; hfd.continuous_fderiv; continuousLinearMapOfBilin; hc; hi

2. Commute genuine integral evaluation and arbitrary pairing

Continuous evaluation and the fixed continuous linear functional inner(w,.) commute with the actual Bochner integral. Real symmetry of the inner product turns this into the displayed all-vector identity. Both integral commutations use the derived interval integrability.

\[\langle Hv,w\rangle=\int_0^1D^2f(y+t(x-y))[v,w]\,dt.\]

Corresponding Lean step

hinner; ContinuousLinearMap.intervalIntegral_apply; innerSL; intervalIntegral_comp_comm

3. Derive the full gradient secant identity by FTC

Put v=x-y. For any w, differentiating t → Df(y+t v)[w] gives D2f(y+t v)[v,w]. Its continuity supplies scalar integrability. The ordinary FTC gives the difference Df(x)[w]-Df(y)[w]; Riesz identifies it with inner(gradient f x-gradient f y,w). Equality against every w yields the full vector equality, not merely its diagonal pairing.

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

Corresponding Lean step

hgrad; hd; hdcont; integral_eq_sub_of_hasDerivAt; gradient; ext_inner_right

4. Inherit genuine symmetry

C2 supplies symmetry of the actual second derivative. The all-vector pairing identity shows inner(Hv,w)=inner(Hw,v)=inner(v,Hw). This does not assume self-adjointness of an unrelated matrix.

\[D^2f(z)[v,w]=D^2f(z)[w,v]\quad\Longrightarrow\quad\langle Hv,w\rangle=\langle v,Hw\rangle.\]

Corresponding Lean step

hsym; hf.contDiffAt.isSymmSndFDerivAt; integral_congr; real_inner_comm

5. Integrate the actual two diagonal bounds

For each v, integrate the constant bounds alpha||v||^2 and beta||v||^2 against ordinary Lebesgue measure on the unit interval. Integral monotonicity and hinner give the inherited inequalities. Signed moduli and dimension zero require no extra positivity or order hypothesis.

\[\alpha\|v\|^2=\int_0^1\alpha\|v\|^2dt\le\langle Hv,v\rangle\le\int_0^1\beta\|v\|^2dt=\beta\|v\|^2.\]

Corresponding Lean step

hbound; intervalIntegral.integral_mono_on; intervalIntegrable_const; hvcont

6. Control the actual operator norm

For the symmetric H, Mathlib identifies its norm with the supremum of absolute Rayleigh quotients. For nonzero v, the previous signed inequalities bound their absolute value by max(|alpha|,|beta|); v=0 gives zero. This proves the stated norm bound even on the zero space. In the paper alpha=1/(2kappa),beta=1,kappa≥1 gives norm≤1 once its curvature premises are produced.

\[\|H\|_{\rm op}=\sup_v\left|\frac{\langle Hv,v\rangle}{\|v\|^2}\right|\le\max(|\alpha|,|\beta|).\]

Corresponding Lean step

H.norm_eq_iSup_rayleighQuotient; hbound; norm_pos_iff; abs_le; ciSup_le

Lean verification

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

Lean proof · hessian_secant_operator

Continuous Riesz composition, operator/inner integral commutation, arbitrary-pairing FTC, genuine C2 symmetry, integral order and symmetric Rayleigh norm.

Download module (.lean)

theorem hessian_secant_operator {f : E → ℝ} {α β : ℝ}
    (hf : ContDiff ℝ 2 f)
    (hlo : ∀ z v, α * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ f) z v) v)
    (hup : ∀ z v, (fderiv ℝ (fderiv ℝ f) z v) v ≤ β * ‖v‖ ^ 2)
    (x y : E) :
    let φ := fun t : ℝ => continuousLinearMapOfBilin
      (fderiv ℝ (fderiv ℝ f) (y + t • (x - y)))
    let H := ∫ t : ℝ in 0..1, φ t
    IntervalIntegrable φ volume 0 1 ∧
      gradient f x - gradient f y = H (x - y) ∧
      H.IsSymmetric ∧
      (∀ v, α * ‖v‖ ^ 2 ≤ inner ℝ (H v) v ∧
        inner ℝ (H v) v ≤ β * ‖v‖ ^ 2) ∧
      ‖H‖ ≤ max |α| |β| := by
  let φ := fun t : ℝ => continuousLinearMapOfBilin
    (fderiv ℝ (fderiv ℝ f) (y + t • (x - y)))
  let H := ∫ t : ℝ in 0..1, φ t
  change IntervalIntegrable φ volume 0 1 ∧ _
  have hfd : ContDiff ℝ 1 (fderiv ℝ f) := hf.fderiv_right (by norm_num)
  have hc : Continuous φ := by
    unfold φ continuousLinearMapOfBilin
    exact continuous_const.clm_comp ((hfd.continuous_fderiv (by norm_num)).comp
      (continuous_const.add (continuous_id.smul continuous_const)))
  have hi : IntervalIntegrable φ volume 0 1 := hc.intervalIntegrable 0 1
  have hinner (v w : E) : inner ℝ (H v) w =
      ∫ t : ℝ in 0..1, (fderiv ℝ (fderiv ℝ f) (y + t • (x - y)) v) w := by
    change inner ℝ ((∫ t : ℝ in 0..1, φ t) v) w = _
    rw [ContinuousLinearMap.intervalIntegral_apply hi v, real_inner_comm]
    change (innerSL ℝ w) (∫ t : ℝ in 0..1, φ t v) = _
    rw [← (innerSL ℝ w).intervalIntegral_comp_comm
      (((hc.clm_apply continuous_const : Continuous (fun t => φ t v))).intervalIntegrable
        (μ := volume) 0 1)]
    apply intervalIntegral.integral_congr
    intro t _
    exact (real_inner_comm w (φ t v)).symm.trans
      (continuousLinearMapOfBilin_apply _ v w)
  have hgrad : gradient f x - gradient f y = H (x - y) := by
    apply ext_inner_right ℝ
    intro w
    rw [hinner]
    have hd (t : ℝ) : HasDerivAt
        (fun s : ℝ => fderiv ℝ f (y + s • (x - y)) w)
        ((fderiv ℝ (fderiv ℝ f) (y + t • (x - y)) (x - y)) w) t := by
      convert ((hfd.differentiable_one _).hasFDerivAt.comp_hasDerivAt t
        (((hasDerivAt_id t).smul_const (x - y)).const_add y)).clm_apply
        (hasDerivAt_const t w) using 1 <;> first | rfl | simp
    have hdcont : Continuous (fun t : ℝ =>
        (fderiv ℝ (fderiv ℝ f) (y + t • (x - y)) (x - y)) w) :=
      (((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) (hdcont.intervalIntegrable 0 1)).symm
  have hsym : H.IsSymmetric := by
    intro v w
    change inner ℝ (H v) w = inner ℝ v (H w)
    have hw : inner ℝ v (H w) =
        ∫ t : ℝ in 0..1, (fderiv ℝ (fderiv ℝ f) (y + t • (x - y)) w) v :=
      (real_inner_comm v (H w)).symm.trans (hinner w v)
    rw [hinner, hw]
    apply intervalIntegral.integral_congr
    intro t _
    exact hf.contDiffAt.isSymmSndFDerivAt (by norm_num) v w
  have hbound (v : E) : α * ‖v‖ ^ 2 ≤ inner ℝ (H v) v ∧
      inner ℝ (H v) v ≤ β * ‖v‖ ^ 2 := by
    have hvcont : Continuous (fun t : ℝ =>
        (fderiv ℝ (fderiv ℝ f) (y + t • (x - y)) 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
    rw [hinner]
    constructor
    · simpa using intervalIntegral.integral_mono_on (by norm_num : (0 : ℝ) ≤ 1)
        (intervalIntegrable_const : IntervalIntegrable (fun _ : ℝ => α * ‖v‖ ^ 2) volume 0 1)
        (hvcont.intervalIntegrable 0 1) (fun t _ => hlo _ v)
    · simpa using intervalIntegral.integral_mono_on (by norm_num : (0 : ℝ) ≤ 1)
        (hvcont.intervalIntegrable 0 1)
        (intervalIntegrable_const : IntervalIntegrable (fun _ : ℝ => β * ‖v‖ ^ 2) volume 0 1)
        (fun t _ => hup _ v)
  refine ⟨hi, hgrad, hsym, hbound, ?_⟩
  rw [H.norm_eq_iSup_rayleighQuotient hsym]
  apply ciSup_le
  intro v
  change |inner ℝ (H v) v / ‖v‖ ^ 2| ≤ max |α| |β|
  by_cases hv : v = 0
  · simp [hv]
  · simp only [abs_div, abs_pow, abs_norm]
    apply (div_le_iff₀ (sq_pos_of_pos (norm_pos_iff.mpr hv))).mpr
    have hl := (hbound v).1
    have hu := (hbound v).2
    have hl' := mul_le_mul_of_nonneg_right
      ((neg_le_abs α).trans (le_max_left |α| |β|)) (sq_nonneg ‖v‖)
    have hu' := mul_le_mul_of_nonneg_right
      ((le_abs_self β).trans (le_max_right |α| |β|)) (sq_nonneg ‖v‖)
    exact abs_le.mpr ⟨by nlinarith, by nlinarith⟩

end AutoSamplingTheory.TechnicalLemmas.Analysis.HessianSecantOperator

Exact module and namespace context

Scope and omitted-condition boundaries

Only the actual Hessian-segment constructor in Lemma4.6. The source smoothed-potential C2/curvature producer, actual Picard-node weighted average H, first-order endpoint expansion/operator remainder, deterministic K contraction, stochastic Khat/Kbar, repeated history, PBPS and both full main results/composition remain independent. The signed Hilbert generalization is background, not an extra assumption on the finite-dimensional source theorem. No probability/cost guarantee or implemented kernel is asserted here.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

InnerProductSpace.continuousLinearMapOfBilin
InnerProductSpace.continuousLinearMapOfBilin_apply
ContDiff.fderiv_right
ContDiff.continuous_fderiv
ContinuousLinearMap.intervalIntegral_apply
ContinuousLinearMap.intervalIntegral_comp_comm
intervalIntegral.integral_eq_sub_of_hasDerivAt
ContDiffAt.isSymmSndFDerivAt
intervalIntegral.integral_mono_on
ContinuousLinearMap.norm_eq_iSup_rayleighQuotient
ext_inner_right

Mathematical sources

SPHMC Lemma4.6 actual Hessian constructor — Only the actual Hessian-segment constructor in Lemma4.6. The source smoothed-potential C2/curvature producer, actual Picard-node weighted average H, first-order endpoint expansion/operator remainder, deterministic K contraction, stochastic Khat/Kbar, repeated history, PBPS and both full main results/composition remain independent. The signed Hilbert generalization is background, not an extra assumption on the finite-dimensional source theorem. No probability/cost guarantee or implemented kernel is asserted here.

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