ε-subgradients

A vector y is an ε-subgradient of f at x when the subgradient inequality holds up to a slack ε: f z ≥ (f x - ε) + ⟨z - x, y⟩ for every z. The set of them, ∂_ε f x, is closed and convex and decreases to ∂f x as ε ↓ 0, and its support function decreases to the directional derivative f'(x; ·), not merely to the closure δ*(· | ∂f x). That is the exact dual of the discrepancy between f'(x; ·) and its own closure.

Main definitions

• epsSubgradient B ε f x — the ε-subdifferential ∂_ε f x ⊆ F.
• shiftFn f x c — w ↦ f (x + w) + c, f translated so that x sits at the origin.

Main results

• epsSubgradient_eq_setOf_conj_le, iInter_epsSubgradient — ∂_ε f x is a level set of a conjugate, and ⋂_{ε > 0} ∂_ε f x = ∂f x.
• posHomGen_shiftFn — the directional derivative is the positively homogeneous convex function generated by the shift. This is the identity everything turns on, and it needs no topology.
• supportFn_epsSubgradient_apply — δ*(y | ∂_ε f x) = inf_{λ > 0} (f (x + λ y) - f x + ε) / λ.
• dirDeriv_eq_iInf_supportFn_epsSubgradient — ⨅_{ε > 0} δ*(· | ∂_ε f x) = f'(x; ·) (Theorem 23.6 in [^1]).

Implementation notes

The classical lim_{ε ↓ 0} is an infimum over ε > 0 here, the same thing because ε ↦ ∂_ε f x is monotone. Finite dimension is used once, to make the generated function closed and so remove the closure from the support-function identity. shiftFn adds a real constant rather than subtracting f x, which avoids EReal subtraction; every lemma below carries f x = (r : ℝ).

References

[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §23.

An EReal service lemma

⨅_{ε > 0} (z + ε) = z, with no hypothesis on z — the two improper values are absorbing for + ε. This is what makes ∂f x the intersection of the nest, and what removes the ε at the end of the main proof.

theorem Tdaf.ConvexAnalysis.iInf_add_pos_coe (z : EReal) : ⨅ ε ∈ Set.Ioi 0, z + ↑ε = z

theorem Tdaf.ConvexAnalysis.le_of_forall_pos_le_add {u v : EReal} (h : ∀ (ε : ℝ), 0 < ε → u ≤ v + ↑ε) : u ≤ v

From u ≤ v + ε for every ε > 0 follows u ≤ v.

theorem Tdaf.ConvexAnalysis.coe_le_add_coe_iff {s t : ℝ} {u : EReal} : ↑s ≤ u + ↑t ↔ ↑(s - t) ≤ u

Moving a real constant across ≤ against a real coercion, on the right.

theorem Tdaf.ConvexAnalysis.coe_add_le_add_coe_iff {s t c : ℝ} {u : EReal} : ↑s + ↑c ≤ u + ↑t ↔ ↑c ≤ u + ↑(t - s)

Slack transfer: a real constant may be moved from one side of an inequality with slack to the other. This is the bookkeeping behind epsSubgradient_eq_supportSet.

theorem Tdaf.ConvexAnalysis.coe_mul_eq_div_coe_inv (a : ℝ) (z : EReal) : ↑a * z = z / ↑a⁻¹

Multiplying by a positive real is dividing by its reciprocal.

theorem Tdaf.ConvexAnalysis.iInf_add_sub_pos_coe (u : EReal) (s : ℝ) : ⨅ ε ∈ Set.Ioi 0, u + ↑(ε - s) = u + ↑(-s)

Letting ε ↓ 0 in u + (ε - s).

The ε-subdifferential

def Tdaf.ConvexAnalysis.epsSubgradient {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (ε : ℝ) (f : E → EReal) (x : E) : Set F

The ε-subdifferential of f at x: the set of y : F satisfying the subgradient inequality up to a slack of ε, f z ≥ (f x - ε) + ⟨z - x, y⟩ for every z. It is written in the equivalent form f x + ⟨z - x, y⟩ ≤ f z + ε, which keeps the shape of subgradient and makes epsSubgradient B 0 f x = subgradient B f x immediate.

Equations

• Tdaf.ConvexAnalysis.epsSubgradient B ε f x = {y : F | ∀ (z : E), f x + ↑((B (z - x)) y) ≤ f z + ↑ε}

@[simp]

theorem Tdaf.ConvexAnalysis.mem_epsSubgradient {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {x : E} {y : F} {ε : ℝ} : y ∈ epsSubgradient B ε f x ↔ ∀ (z : E), f x + ↑((B (z - x)) y) ≤ f z + ↑ε

@[simp]

theorem Tdaf.ConvexAnalysis.epsSubgradient_zero {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (x : E) : epsSubgradient B 0 f x = subgradient B f x

At ε = 0 the ε-subdifferential is the subdifferential.

theorem Tdaf.ConvexAnalysis.epsSubgradient_mono {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (x : E) {ε₁ ε₂ : ℝ} (h : ε₁ ≤ ε₂) : epsSubgradient B ε₁ f x ⊆ epsSubgradient B ε₂ f x

The ε-subdifferentials increase with ε.

theorem Tdaf.ConvexAnalysis.subgradient_subset_epsSubgradient {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {ε : ℝ} (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (x : E) (hε : 0 ≤ ε) : subgradient B f x ⊆ epsSubgradient B ε f x

Every subgradient is an ε-subgradient.

theorem Tdaf.ConvexAnalysis.iInter_epsSubgradient {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) (x : E) : ⋂ ε ∈ Set.Ioi 0, epsSubgradient B ε f x = subgradient B f x

The nest of ε-subdifferentials has intersection ∂f x. No hypothesis is needed: ⨅_{ε > 0} (z + ε) = z holds in EReal outright.

noncomputable def Tdaf.ConvexAnalysis.shiftFn {E : Type u_1} [AddCommGroup E] (f : E → EReal) (x : E) (c : ℝ) : E → EReal

The book's h, with a constant added: w ↦ f (x + w) + c. Its h y = f (x + y) - f x is shiftFn f x (-f x) and its h + ε is shiftFn f x (ε - f x), both under the standing hypothesis that f x is finite.

Equations

• Tdaf.ConvexAnalysis.shiftFn f x c w = f (x + w) + ↑c

@[simp]

theorem Tdaf.ConvexAnalysis.shiftFn_apply {E : Type u_1} [AddCommGroup E] (f : E → EReal) (x : E) (c : ℝ) (w : E) : shiftFn f x c w = f (x + w) + ↑c

theorem Tdaf.ConvexAnalysis.shiftFn_zero {E : Type u_1} [AddCommGroup E] {f : E → EReal} {x : E} {r c : ℝ} (hr : f x = ↑r) : shiftFn f x c 0 = ↑(r + c)

The value of shiftFn at the origin.

theorem Tdaf.ConvexAnalysis.convexFn_shiftFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} (hf : ConvexFn f) (x : E) (c : ℝ) : ConvexFn (shiftFn f x c)

A translate of a convex function, raised by a constant, is convex.

theorem Tdaf.ConvexAnalysis.proper_shiftFn {E : Type u_1} [AddCommGroup E] {f : E → EReal} (hp : Proper f) (x : E) (c : ℝ) : Proper (shiftFn f x c)

A translate of a proper function, raised by a constant, is proper.

The level-set description of ∂_ε f x

theorem Tdaf.ConvexAnalysis.epsSubgradient_eq_supportSet {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {x : E} {r : ℝ} (hr : f x = ↑r) (ε : ℝ) : epsSubgradient B ε f x = supportSet B (shiftFn f x (ε - r))

∂_ε f x is the set of linear functions minorizing h + ε, for h the translate w ↦ f (x + w) - f x.

theorem Tdaf.ConvexAnalysis.epsSubgradient_eq_setOf_conj_le {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {x : E} {r : ℝ} (hr : f x = ↑r) (ε : ℝ) : epsSubgradient B ε f x = {y : F | conj B (shiftFn f x (ε - r)) y ≤ 0}

∂_ε f x is the level set {y | h* y ≤ ε}, here with the ε folded into the function so that the level is 0.

theorem Tdaf.ConvexAnalysis.convex_epsSubgradient {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {x : E} {r : ℝ} (hr : f x = ↑r) (ε : ℝ) : Convex ℝ (epsSubgradient B ε f x)

∂_ε f x is convex: it is a level set of the convex function h*.

theorem Tdaf.ConvexAnalysis.isClosed_epsSubgradient {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsContinuousPairing B.flip] {f : E → EReal} {x : E} {r : ℝ} (hr : f x = ↑r) (ε : ℝ) : IsClosed (epsSubgradient B ε f x)

∂_ε f x is closed: it is a sublevel set of the lower semicontinuous function h*. Continuity of the pairing is needed on the F side only, which is where ∂_ε f x lives.

The directional derivative as a generated positively homogeneous function

theorem Tdaf.ConvexAnalysis.posHomGen_le_iInf_coe_mul {E : Type u_1} [AddCommGroup E] [Module ℝ E] (g : E → EReal) (v : E) : posHomGen g v ≤ ⨅ a ∈ Set.Ioi 0, ↑a * g (a⁻¹ • v)

The generated positively homogeneous function is bounded by every rescaled value of g: this is the half of the formula for posHomGen that needs neither convexity of g nor v ≠ 0.

theorem Tdaf.ConvexAnalysis.iInf_coe_mul_eq_iInf_div {E : Type u_1} [AddCommGroup E] [Module ℝ E] (g : E → EReal) (v : E) : ⨅ a ∈ Set.Ioi 0, ↑a * g (a⁻¹ • v) = ⨅ b ∈ Set.Ioi 0, g (b • v) / ↑b

The infimum defining posHomGen, reindexed by a ↦ a⁻¹ as a family of difference quotients.

theorem Tdaf.ConvexAnalysis.posHomGen_apply_eq_iInf_div {E : Type u_1} [AddCommGroup E] [Module ℝ E] {g : E → EReal} (hg : ConvexFn g) {v : E} (hv : v ≠ 0) : posHomGen g v = ⨅ b ∈ Set.Ioi 0, g (b • v) / ↑b

The generated function in difference-quotient form: away from the origin, posHomGen g v = inf {g (λ v) / λ | λ > 0}.

theorem Tdaf.ConvexAnalysis.shiftFn_neg_apply {E : Type u_1} [AddCommGroup E] {f : E → EReal} {x : E} {r : ℝ} (hr : f x = ↑r) (w : E) : shiftFn f x (-r) w = f (x + w) - f x

The shift written out: shiftFn f x (-f x) w = f (x + w) - f x.

theorem Tdaf.ConvexAnalysis.iInf_coe_mul_shiftFn_neg {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {x : E} {r : ℝ} (hr : f x = ↑r) (v : E) : ⨅ a ∈ Set.Ioi 0, ↑a * shiftFn f x (-r) (a⁻¹ • v) = dirDeriv f x v

The rescaled values of the shift are exactly the difference quotients defining f'(x; ·); their infimum is therefore the directional derivative.

theorem Tdaf.ConvexAnalysis.posHomGen_shiftFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → EReal} {x : E} {r : ℝ} (hf : ConvexFn f) (hr : f x = ↑r) : posHomGen (shiftFn f x (-r)) = dirDeriv f x

The directional derivative is the positively homogeneous convex function generated by h: f'(x; ·) = posHomGen (f (x + ·) - f x). Both inequalities are maximality arguments. No topology, and — unlike the book's own formula for posHomGen — no case distinction at v = 0.

The support functions of the ε-subdifferentials

theorem Tdaf.ConvexAnalysis.isClosed_epi_shiftFn {E : Type u_1} [NormedAddCommGroup E] {f : E → EReal} (hc : IsClosed (epi f)) (x : E) (c : ℝ) : IsClosed (epi (shiftFn f x c))

A translate of a function with closed epigraph, raised by a constant, has closed epigraph: the epigraph is the preimage of epi f under a homeomorphism of E × ℝ.

theorem Tdaf.ConvexAnalysis.shiftFn_sub_apply_zero {E : Type u_1} [NormedAddCommGroup E] {f : E → EReal} {x : E} {r : ℝ} (hr : f x = ↑r) (ε : ℝ) : shiftFn f x (ε - r) 0 = ↑ε

The value of h + ε at the origin is ε.

theorem Tdaf.ConvexAnalysis.closedFn_posHomGen_shiftFn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} {x : E} {ε r : ℝ} (hf : ConvexFn f) (hp : Proper f) (hc : IsClosed (epi f)) (hr : f x = ↑r) (hε : 0 < ε) : ClosedFn (posHomGen (shiftFn f x (ε - r)))

For ε > 0 the positively homogeneous convex function generated by h + ε is already closed, because h + ε is finite and positive at the origin. This removes the closure from the support-function identity below, and is the only place finite dimension is used.

theorem Tdaf.ConvexAnalysis.supportFn_epsSubgradient {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {x : E} {ε r : ℝ} [IsCompatiblePairing B] (hf : ConvexFn f) (hp : Proper f) (hc : IsClosed (epi f)) (hr : f x = ↑r) (hε : 0 < ε) : supportFn B.flip (epsSubgradient B ε f x) = posHomGen (shiftFn f x (ε - r))

For ε > 0 the support function of ∂_ε f x is the positively homogeneous convex function generated by h + ε, with no closure operation, by the previous lemma.

theorem Tdaf.ConvexAnalysis.supportFn_epsSubgradient_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {x : E} {ε r : ℝ} [IsCompatiblePairing B] (hf : ConvexFn f) (hp : Proper f) (hc : IsClosed (epi f)) (hr : f x = ↑r) (hε : 0 < ε) {v : E} (hv : v ≠ 0) : supportFn B.flip (epsSubgradient B ε f x) v = ⨅ b ∈ Set.Ioi 0, (f (x + b • v) - f x + ↑ε) / ↑b

The explicit formula: δ*(y | ∂_ε f x) = inf {(f (x + λ y) - f x + ε) / λ | λ > 0}.

theorem Tdaf.ConvexAnalysis.dirDeriv_eq_iInf_supportFn_epsSubgradient {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} {x : E} {r : ℝ} [IsCompatiblePairing B] (hf : ConvexFn f) (hp : Proper f) (hc : IsClosed (epi f)) (hr : f x = ↑r) (v : E) : ⨅ ε ∈ Set.Ioi 0, supportFn B.flip (epsSubgradient B ε f x) v = dirDeriv f x v

The support functions of the ε-subdifferentials decrease, as ε ↓ 0, to the directional derivative — not merely to its closure δ*(· | ∂f x). Both inequalities are read off posHomGen, letting ε ↓ 0 inside the rescaling to leave the difference quotients that define f'(x; ·).