Fréchet Derivatives and Subgradients

This file establishes the connection between Fréchet derivatives (HasFDerivWithinAt, HasFDerivAt) and subgradients (HasSubgradientWithinAt f g s x) for convex functions.

Main results

• HasFDerivWithinAt.hasSubgradientWithinAt: A Fréchet derivative within s of a function convex on s is a subgradient on s. HasFDerivAt.hasSubgradientWithinAt is the special case of a derivative at a point.
• HasFDerivAt.eq_of_hasSubgradientWithinAt: Uniqueness of the subgradient at an interior differentiable point.
• HasFDerivAt.subdifferentialWithin_add: Subdifferential sum rule when one component is Fréchet differentiable.

theorem HasFDerivWithinAt.tendsto_bregDiv_slope_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E} {g : E →L[ℝ] F} (hderiv : HasFDerivWithinAt f g s x) (w : E) : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • bregDiv f (x + t • w) x g) (nhdsWithin 0 ((fun (t : ℝ) => x + t • w) ⁻¹' s \ {0})) (nhds 0)

As t → 0 along the steps t with x + t • w ∈ s, the linearization error of a function Fréchet differentiable within s scaled by t⁻¹ converges to 0.

theorem HasFDerivAt.tendsto_bregDiv_slope_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {x : E} {g : E →L[ℝ] F} (hderiv : HasFDerivAt f g x) (w : E) : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • bregDiv f (x + t • w) x g) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

As the step size t → 0⁺, the linearization error of a Fréchet differentiable function scaled by t⁻¹ converges to 0.

theorem ConvexOn.bregDiv_slope_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E} [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] (hf : ConvexOn ℝ s f) {z : E} (hx : x ∈ s) (hz : z ∈ s) (J : E →L[ℝ] F) {t : ℝ} (ht0 : 0 < t) (ht1 : t ≤ 1) : t⁻¹ • _root_.bregDiv f (x + t • (z - x)) x J ≤ _root_.bregDiv f z x J

Scaled Bregman divergence monotonicity along segments for convex functions.

theorem HasFDerivWithinAt.hasSubgradientWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E} {g : E →L[ℝ] F} [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] [OrderClosedTopology F] (hderiv : HasFDerivWithinAt f g s x) (hf : ConvexOn ℝ s f) (hx : x ∈ s) : HasSubgradientWithinAt f g s x

A Fréchet derivative within s of a function convex on s is a subgradient on s.

theorem HasFDerivAt.hasSubgradientWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E} {g : E →L[ℝ] F} [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] [OrderClosedTopology F] (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ s f) (hx : x ∈ s) : HasSubgradientWithinAt f g s x

A Fréchet derivative of a convex function is a subgradient.

theorem HasFDerivAt.le_of_hasSubgradientWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E} {g h : E →L[ℝ] F} [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] [OrderClosedTopology F] (hderiv : HasFDerivAt f g x) (hs : s ∈ nhds x) (hsub : HasSubgradientWithinAt f h s x) (w : E) : h w ≤ g w

theorem HasFDerivAt.eq_of_hasSubgradientWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E} {g h : E →L[ℝ] F} [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] [OrderClosedTopology F] (hderiv : HasFDerivAt f g x) (hs : s ∈ nhds x) (hsub : HasSubgradientWithinAt f h s x) : h = g

Uniqueness of the subgradient at an interior differentiable point.

theorem HasFDerivAt.subdifferentialWithin_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E} {g : E →L[ℝ] F} [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] [OrderClosedTopology F] (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ s f) (hs : s ∈ nhds x) : subdifferentialWithin ℝ f s x = {g}

The subdifferential of a convex, differentiable function at an interior point is the singleton containing its derivative.

theorem subdifferentialWithin_const_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} {x : E} [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] [OrderClosedTopology F] (c : F) (hs : s ∈ nhds x) : subdifferentialWithin ℝ (fun (x : E) => c) s x = {0}

The subdifferential of a constant function at an interior point is {0} (the normal cone to s at an interior point is trivial).

theorem HasFDerivAt.hasSubgradientWithinAt_add_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} {x : E} [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] [OrderClosedTopology F] {f₁ f₂ : E → F} {g₁ g : E →L[ℝ] F} (hderiv₁ : HasFDerivAt f₁ g₁ x) (hf₁ : ConvexOn ℝ s f₁) (hf₂ : ConvexOn ℝ s f₂) (hx : x ∈ s) : HasSubgradientWithinAt (f₁ + f₂) g s x ↔ HasSubgradientWithinAt f₂ (g - g₁) s x

Subdifferential sum rule when f₁ is convex and Fréchet differentiable at x and f₂ is convex on s: g is a subgradient of f₁ + f₂ at x if and only if g - g₁ is a subgradient of f₂ at x.

theorem HasFDerivAt.subdifferentialWithin_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {s : Set E} {x : E} [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] [OrderClosedTopology F] {f₁ f₂ : E → F} {g₁ : E →L[ℝ] F} (hderiv₁ : HasFDerivAt f₁ g₁ x) (hf₁ : ConvexOn ℝ s f₁) (hf₂ : ConvexOn ℝ s f₂) (hx : x ∈ s) : subdifferentialWithin ℝ (f₁ + f₂) s x = {g₁} + subdifferentialWithin ℝ f₂ s x

Subdifferential sum rule in set form: ∂[ℝ, s, x](f₁ + f₂) = {g₁} + ∂[ℝ, s, x](f₂).

theorem HasFDerivAt.subdifferentialWithin_eq_add_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E} {g : E →L[ℝ] F} [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] [OrderClosedTopology F] (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ s f) (hx : x ∈ s) : subdifferentialWithin ℝ f s x = {g} + subdifferentialWithin ℝ (fun (x : E) => 0) s x

When f is convex and Fréchet differentiable at x ∈ s, its subdifferential is g + ∂[ℝ, s, x](0) (the derivative plus the normal cone to s at x).