Co-finiteness and the blow-up of the gradient

A finite differentiable convex function on a finite-dimensional space is co-finite exactly when ‖∇f xᵢ‖ → ∞ for every sequence with ‖xᵢ‖ → ∞. This is the criterion that makes co-finiteness usable: it turns a hypothesis about the recession function — equivalently about dom f* — into one that can be checked on the gradient mapping alone.

Main results

• forall_tendsto_norm_atTop_iff_isBounded — for an arbitrary g, the sequential condition is boundedness of every sublevel set {x | ‖g x‖ ≤ b}.
• isBounded_setOf_norm_gradient_le_of_dom_conj_eq_univ — the easy half: when dom f* = E, the set of points whose gradient lies in a ball is ∂f* of that ball, hence compact.
• dom_conj_eq_univ_of_isBounded, cofinite_iff_forall_tendsto_norm_gradient_atTop — the hard half, and the criterion itself (Lemma 26.7 in [^1]).

Implementation notes

The hard half is proved by showing D = ∇f(E) clopen in the connected space E, rather than by the book's case split at a boundary point of dom f*. Openness comes from the normal cone: a non-zero n normal to dom f* at v = ∇f x puts the whole half-line x + t n, t ≥ 0, inside ∂f*(v), so every point of it has gradient v and {y | ‖∇f y‖ ≤ ‖v‖} is unbounded.

References

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

Sequences going to infinity versus bounded sublevel sets

theorem Tdaf.ConvexAnalysis.forall_tendsto_norm_atTop_iff_isBounded {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup F] (g : E → F) : (∀ (xs : ℕ → E), Filter.Tendsto (fun (i : ℕ) => ‖xs i‖) Filter.atTop Filter.atTop → Filter.Tendsto (fun (i : ℕ) => ‖g (xs i)‖) Filter.atTop Filter.atTop) ↔ ∀ (b : ℝ), Bornology.IsBounded {x : E | ‖g x‖ ≤ b}

‖g xᵢ‖ → ∞ along every sequence with ‖xᵢ‖ → ∞ is boundedness of every sublevel set of ‖g‖. No convexity and no linearity.

The gradient criterion for co-finiteness

theorem Tdaf.ConvexAnalysis.isBounded_setOf_norm_gradient_le_of_dom_conj_eq_univ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) (hdom : dom f = Set.univ) (hdiff : ∀ (z : E), DifferentiableAtFn f z) (hdc : dom (conj (innerₗ E) f) = Set.univ) (b : ℝ) : Bornology.IsBounded {x : E | ‖gradient (fun (w : E) => (f w).toReal) x‖ ≤ b}

The easy half: if dom f* = E then {x | ‖∇f x‖ ≤ b} is bounded, being contained in ∂f* of the closed ball of radius b, which is compact.

theorem Tdaf.ConvexAnalysis.gradientRange_subset_interior_dom_conj_of_isBounded {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) (hdom : dom f = Set.univ) (hdiff : ∀ (z : E), DifferentiableAtFn f z) (hbd : ∀ (b : ℝ), Bornology.IsBounded {x : E | ‖gradient (fun (w : E) => (f w).toReal) x‖ ≤ b}) : gradientRange f ⊆ interior (dom (conj (innerₗ E) f))

The hard half, first step: the range of ∇f lies inside int (dom f*). A non-zero n normal to dom f* at v = ∇f x may be added to x with any non-negative coefficient without leaving ∂f*(v), so the whole half-line x + t n has gradient v and {y | ‖∇f y‖ ≤ ‖v‖} is unbounded.

theorem Tdaf.ConvexAnalysis.isClosed_gradientRange_of_isBounded {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) (hdom : dom f = Set.univ) (hdiff : ∀ (z : E), DifferentiableAtFn f z) (hbd : ∀ (b : ℝ), Bornology.IsBounded {x : E | ‖gradient (fun (w : E) => (f w).toReal) x‖ ≤ b}) : IsClosed (gradientRange f)

The hard half, second step: the range of ∇f is closed. A convergent sequence of gradients is bounded, so the points carrying them lie in one bounded sublevel set, and a convergent subsequence of those points has the limit gradient as its gradient.

theorem Tdaf.ConvexAnalysis.dom_conj_eq_univ_of_isBounded {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) (hdom : dom f = Set.univ) (hdiff : ∀ (z : E), DifferentiableAtFn f z) (hbd : ∀ (b : ℝ), Bornology.IsBounded {x : E | ‖gradient (fun (w : E) => (f w).toReal) x‖ ≤ b}) : dom (conj (innerₗ E) f) = Set.univ

The hard half: bounded sublevel sets of ‖∇f‖ force dom f* = E. Here ∇f(E) is non-empty, open and closed, and E is connected.

theorem Tdaf.ConvexAnalysis.cofinite_iff_forall_tendsto_norm_gradient_atTop {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) (hdom : dom f = Set.univ) (hdiff : ∀ (z : E), DifferentiableAtFn f z) : Cofinite f ↔ ∀ (xs : ℕ → E), Filter.Tendsto (fun (i : ℕ) => ‖xs i‖) Filter.atTop Filter.atTop → Filter.Tendsto (fun (i : ℕ) => ‖gradient (fun (w : E) => (f w).toReal) (xs i)‖) Filter.atTop Filter.atTop

A finite differentiable convex function is co-finite exactly when the norm of its gradient tends to infinity along every sequence tending to infinity.