Gradient monotonicity is equivalent to a Hessian lower bound

Fix x,v and let g(t)=Df(x+tv)[v]. Apply gradient monotonicity at x and x+tv with t>0. The displacement is tv and its squared norm is t²‖v‖². Cancelling the positive t and dividing once more by t gives a bound on the difference quotient. C² gives g′(0)=D²f(x)[v,v]. The displayed inequality holds for all positive t, so passage to t↓0 preserves it. Neither m nor ‖v‖ is divided by. For v=y−x the Hessian bound holds along x+tv. C² gives a continuous integrand and interval integrability. Integrate the constant lower bound over an interval of length one, then use the preceding segment 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 gradient_mono_iff_fderiv2_lower
    {f : E → ℝ} {m : ℝ} (hf : ContDiff ℝ 2 f) :
    (∀ x y : E, m * ‖y - x‖ ^ 2 ≤
      inner ℝ (gradient f y - gradient f x) (y - x)) ↔
    ∀ x v : E, m * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ f) x v) v := by
  have hfd : ContDiff ℝ 1 (fderiv ℝ f) := hf.fderiv_right (by norm_num)
  constructor
  · intro hm x v
    let g : ℝ → ℝ := fun t => fderiv ℝ f (x + t • v) v
    have hdAll (t : ℝ) : HasDerivAt g
        ((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 hd : HasDerivAt g ((fderiv ℝ (fderiv ℝ f) x v) v) 0 := by
      simpa using hdAll 0
    apply ge_of_tendsto hd.tendsto_slope_zero_right
    filter_upwards [self_mem_nhdsWithin] with t ht
    have ht : 0 < t := ht
    have h := hm x (x + t • v)
    rw [add_sub_cancel_left, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs,
      inner_smul_right, inner_sub_left] at h
    have hscaled : t * (m * ‖v‖ ^ 2) ≤ g t - g 0 := by
      apply le_of_mul_le_mul_left (a := t) _ ht
      simpa [g, gradient, Function.comp_def, pow_two, mul_assoc, mul_left_comm, mul_comm] using h
    simpa [smul_eq_mul, div_eq_inv_mul] using
      (le_div_iff₀ ht).mpr (by simpa [mul_comm] using hscaled)
  · intro hH x y
    let v := y - x
    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
    have h := intervalIntegral.integral_mono_on (by norm_num : (0 : ℝ) ≤ 1)
      (intervalIntegrable_const : IntervalIntegrable (fun _ : ℝ => m * ‖v‖ ^ 2) volume 0 1)
      (hc.intervalIntegrable 0 1) (fun t _ => hH (x + t • v) v)
    rw [← gradient_sub_inner_eq_integral_fderiv2 hf x v] at h
    simpa [v] using h

/-- Proposition 1.6 part 2, with the source's whole Euclidean domain,
nonnegative modulus and C² regularity. Together with the C¹ theorem this
connects all four source conditions. -/

Exact module and namespace context