theorem is_l_smooth_on_fderiv_descent {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : NNReal} {D : Set E} {f : E → ℝ} (hD : Convex ℝ D) (hf : is_l_smooth_on f D L) {x y : E} (hx : x ∈ D) (hy : y ∈ D) : f y ≤ f x + (fderiv ℝ f x) (y - x) + ↑L / 2 * ‖y - x‖ ^ 2

Companion bridge for Lemma 5.7: on a convex set, L-smoothness gives the Banach-space quadratic upper model with the Fréchet derivative as linear term.

theorem is_l_smooth_on_univ_fderiv_descent {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : NNReal} {f : E → ℝ} (hf : is_l_smooth_on f Set.univ L) (x y : E) : f y ≤ f x + (fderiv ℝ f x) (y - x) + ↑L / 2 * ‖y - x‖ ^ 2

Global companion to is_l_smooth_on_fderiv_descent: on Set.univ, the convex-set descent estimate specializes to an unrestricted Fréchet-derivative quadratic upper model.

theorem is_l_smooth_on_descent_lemma {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : NNReal} {D : Set E} {f : E → ℝ} (hD : Convex ℝ D) (hf : is_l_smooth_on f D L) {x y : E} (hx : x ∈ D) (hy : y ∈ D) : f y ≤ f x + inner ℝ (gradient f x) (y - x) + ↑L / 2 * ‖x - y‖ ^ 2

Lemma 5.7: if D is convex and f is L-smooth on D, then f y ≤ f x + ⟪∇ f x, y - x⟫ + (L / 2) * ‖x - y‖² for all x, y ∈ D.

theorem is_l_smooth_on_univ_descent_lemma {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : NNReal} {f : E → ℝ} (hf : is_l_smooth_on f Set.univ L) (x y : E) : f y ≤ f x + inner ℝ (gradient f x) (y - x) + ↑L / 2 * ‖x - y‖ ^ 2

Global companion to Lemma 5.7: on Set.univ, L-smoothness gives the quadratic upper model with the ambient gradient field.