SmoothnessEquivalences: mathematical reading route

Write the upper model from x to y and from y to x. The values cancel on addition; the linear terms combine with opposite displacements. Each quadratic correction is β‖y−x‖²/2. For the converse set g=−f and m=−β. Linearity of the derivative and Riesz map gives ∇g=−∇f. The assumed one-sided upper bound becomes quantitative gradient monotonicity of g with signed modulus m. The signed gradient-to-chord theorem integrates along affine segments; C¹ supplies derivative continuity and interval integrability. Its chord conclusion and the genuine gradient yield the existing first-order lower model for g. Negating this inequality gives exactly the upper model for f, with coefficient β/2.

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 upper_model_iff_gradient_upper {f : E → ℝ} {β : ℝ}
    (hf : ContDiff ℝ 1 f) :
    (∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2) ↔
    ∀ x y, inner ℝ (gradient f y - gradient f x) (y - x) ≤ β * ‖y - x‖ ^ 2 := by
  have hg (x : E) : gradient (fun z => -f z) x = -gradient f x := by
    simp [gradient]
  constructor
  · intro h x y
    have hxy := h x y
    have hyx := h y x
    rw [show x - y = -(y - x) by abel, inner_neg_right, norm_neg] at hyx
    rw [inner_sub_left]
    linarith
  · intro h
    have hn : StrongConvexOn (univ : Set E) (-β) (fun z => -f z) :=
      ConvexityC1.strongConvexOn_univ_of_gradient_mono_integral hf.neg (by
        intro x y
        rw [hg, hg, inner_sub_left, inner_neg_left, inner_neg_left]
        have hxy := h x y
        rw [inner_sub_left] at hxy
        linarith)
    intro x y
    have hl := StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn hn
      (fun z _ => (hf.neg.differentiable_one z).hasGradientAt) (mem_univ x) (mem_univ y)
    rw [hg, inner_neg_left] at hl
    linarith

/-- With genuine C² regularity the same upper model is equivalent to the
Hessian diagonal upper bound, without assuming convexity. -/

Exact module and namespace context

C² implies C¹, so the preceding theorem replaces the upper model by its one-sided gradient inequality. Set g=−f and m=−β again. Genuine first and second Fréchet derivatives commute with negation. The compiled equivalence for g uses a positive-direction derivative limit in one direction and the Hessian segment FTC in the other. Multiplying the two lower inequalities by −1 gives the upper gradient and Hessian bounds. Neither β nor the norm of the direction is divided by, so zero and negative β and v=0 remain valid.

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 upper_model_iff_fderiv2_upper {f : E → ℝ} {β : ℝ}
    (hf : ContDiff ℝ 2 f) :
    (∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2) ↔
    ∀ x v, (fderiv ℝ (fderiv ℝ f) x v) v ≤ β * ‖v‖ ^ 2 := by
  have hg (x : E) : gradient (fun z => -f z) x = -gradient f x := by
    simp [gradient]
  have hH (x v : E) :
      (fderiv ℝ (fderiv ℝ (fun z => -f z)) x v) v =
        -(fderiv ℝ (fderiv ℝ f) x v) v := by
    rw [show fderiv ℝ (fun z => -f z) = -fderiv ℝ f by
      funext z; exact fderiv_fun_neg]
    rw [fderiv_neg]
    rfl
  rw [upper_model_iff_gradient_upper (hf.of_le (by norm_num))]
  have h := ConvexityC2.gradient_mono_iff_fderiv2_lower (m := -β) hf.neg
  simp only [hg, inner_sub_left, inner_neg_left, hH] at h
  constructor
  · intro hu x v
    have hl := h.mp (by
      intro x y
      have hxy := hu x y
      rw [inner_sub_left] at hxy
      linarith) x v
    linarith
  · intro hu x y
    have hl := h.mpr (by intro x v; have hv := hu x v; linarith) x y
    rw [inner_sub_left]
    linarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.SmoothnessEquivalences

Exact module and namespace context