ConvexSmoothGradient: mathematical reading route

Fix x,y and write d=∇f(y)−∇f(x), z=y−d/β. Convexity and the actual gradient give the supporting-plane lower bound at x. This says f minus its tangent plane at x is minimized at x. The positive β makes the trial step meaningful. Apply the original upper model from y to z. Insert z−y=−d/β and z−x=(y−x)−d/β in the two models. Combining the inequalities eliminates f(z). The difference of the two linear terms is ⟨d,d⟩/β. Multiplication by 2β gives the shared division-free statement. The Lean proof carries out the same field arithmetic with β≠0 and positive reciprocal. The source reciprocal form is only recovered for β>0.

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_gap_sq_le_bregman {f : E → ℝ} {β : ℝ}
    (hf : ContDiff ℝ 1 f) (hc : ConvexOn ℝ univ f) (hβ : 0 < β)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖gradient f y - gradient f x‖ ^ 2 ≤
      2 * β * (f y - f x - inner ℝ (gradient f x) (y - x)) := by
  let d := gradient f y - gradient f x
  let z := y - β⁻¹ • d
  have hl := StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn
    (strongConvexOn_zero.mpr hc)
    (fun w _ => (hf.differentiable_one w).hasGradientAt) (mem_univ x) (mem_univ z)
  simp only [zero_div, zero_mul, add_zero] at hl
  have hh := hu y z
  have hzx : z - x = (y - x) - β⁻¹ • d := by dsimp [z]; abel
  rw [hzx, inner_sub_right, inner_smul_right] at hl
  have hzy : z - y = -(β⁻¹ • d) := by dsimp [z]; abel
  rw [hzy, inner_neg_right, inner_smul_right, norm_neg, norm_smul,
    Real.norm_eq_abs, mul_pow, sq_abs] at hh
  have hd : inner ℝ (gradient f y) d - inner ℝ (gradient f x) d = ‖d‖ ^ 2 := by
    rw [← inner_sub_left]
    exact real_inner_self_eq_norm_sq d
  have h := le_trans hl hh
  have hb : β ≠ 0 := ne_of_gt hβ
  apply (mul_le_mul_iff_right₀ (inv_pos.mpr hβ)).mp
  field_simp [hb] at h ⊢
  nlinarith

Exact module and namespace context

Fix x,y and set d=∇f(y)−∇f(x). For ε>0, the β upper model implies the (β+ε) model because squared norm is nonnegative. Thus the positive-modulus Bregman bound applies even when β=0. The values f(x),f(y) cancel. The two Bregman gaps sum to the gradient-displacement pairing, while reversing the gradient difference preserves its squared norm. Let ε decrease to zero. The right side is affine and continuous in ε, and order is closed in ℝ. This proves the scaled bound for all β≥0. At β=0 the norm square must be zero, so the gradient is constant; no inverse at zero is used.

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_cocoercive {f : E → ℝ} {β : ℝ}
    (hf : ContDiff ℝ 1 f) (hc : ConvexOn ℝ univ f) (hβ : 0 ≤ β)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + β / 2 * ‖y - x‖ ^ 2)
    (x y : E) :
    ‖gradient f y - gradient f x‖ ^ 2 ≤
      β * inner ℝ (gradient f y - gradient f x) (y - x) := by
  have he (ε : ℝ) (hε : 0 < ε) :
      ‖gradient f y - gradient f x‖ ^ 2 ≤
        (β + ε) * inner ℝ (gradient f y - gradient f x) (y - x) := by
    have hu' (a b : E) : f b ≤ f a + inner ℝ (gradient f a) (b - a) +
        (β + ε) / 2 * ‖b - a‖ ^ 2 := by
      have := hu a b
      nlinarith [sq_nonneg ‖b - a‖]
    have hxy := gradient_gap_sq_le_bregman hf hc (add_pos_of_nonneg_of_pos hβ hε) hu' x y
    have hyx := gradient_gap_sq_le_bregman hf hc (add_pos_of_nonneg_of_pos hβ hε) hu' y x
    rw [norm_sub_rev (gradient f x), show x - y = -(y - x) by abel, inner_neg_right] at hyx
    rw [inner_sub_left]
    nlinarith
  have ht : Tendsto (fun ε : ℝ => (β + ε) *
      inner ℝ (gradient f y - gradient f x) (y - x)) (𝓝[>] 0)
      (𝓝 (β * inner ℝ (gradient f y - gradient f x) (y - x))) := by
    simpa using (tendsto_const_nhds.add (tendsto_id.mono_left nhdsWithin_le_nhds :
      Tendsto (fun ε : ℝ => ε) (𝓝[>] 0) (𝓝 0))).mul tendsto_const_nhds
  apply ge_of_tendsto ht
  filter_upwards [self_mem_nhdsWithin] with ε hε
  exact he ε hε

Exact module and namespace context

Write d=∇f(y)−∇f(x), v=y−x. Multiply the inner-product upper bound by the nonnegative β and combine it with cocoercivity. If ‖d‖=0, the desired inequality is immediate. Otherwise ‖d‖>0 and cancellation yields the Lipschitz estimate. This does not divide by β and therefore includes β=0.

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_lipschitz {f : E → ℝ} {β : NNReal}
    (hf : ContDiff ℝ 1 f) (hc : ConvexOn ℝ univ f)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + (β : ℝ) / 2 * ‖y - x‖ ^ 2) :
    LipschitzWith β (gradient f) := by
  rw [lipschitzWith_iff_norm_sub_le]
  intro x y
  have h := gradient_cocoercive hf hc β.coe_nonneg hu y x
  have hs := mul_le_mul_of_nonneg_left
    (real_inner_le_norm (gradient f x - gradient f y) (x - y)) β.coe_nonneg
  by_cases hz : ‖gradient f x - gradient f y‖ = 0
  · rw [hz]
    positivity
  · apply (mul_le_mul_iff_left₀ (lt_of_le_of_ne (norm_nonneg _) (Ne.symm hz))).mp
    nlinarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSmoothGradient

Exact module and namespace context