Recession functions, conjugates and polar cones

Two dual dictionaries between a function's recession data and its conjugate's effective domain. At the level of functions, the recession function of a conjugate is the support function of the effective domain; at the level of cones, the recession cone of a conjugate is the polar of the effective domain, which is the same statement read at the level 0.

One direction is free: bounding the supremum that defines f* termwise gives (f*) 0⁺ ≤ δ*(· | dom f) with no hypothesis at all. The reverse needs a z at which f* is finite, so that Fenchel's inequality at z + a • y can be pushed to a → ∞; that is the hypothesis Proper (conj B f), automatic for a closed proper convex f.

Main results

• recessionFn_conj — (f*) 0⁺ = δ*(· | dom f) (Theorem 13.3 in [^1]). The dual form f 0⁺ = δ*(· | dom f*) is recessionFn_eq_supportFn_dom_conj in Duality/Level.lean.
• constancySpace_conj — the constancy space of f* is the annihilator of dom f. This is the form the image and duality theorems consume: "f* is constant along z" becomes "z annihilates dom f", which a relative-interior hypothesis can discharge.
• recessionConeFn_conj, recessionConeFn_conj_hull, recessionConeFn_eq_polarCone_dom_conj, polarCone_recessionConeFn — both polar assertions (Theorem 14.2 in [^1]), each in the direct form and in the cone-generated phrasing. The direct form is stated against dom f rather than the cone it generates; a polar cone cannot tell the two apart (polarCone_hull).
• zero_mem_interior_iff_polarCone_eq_zero — a nonempty convex set has the origin in its interior exactly when its polar cone is trivial. Composed with the polar dictionary and the level-set theory this gives isBounded_setOf_le_iff_zero_mem_interior_dom_conj.

References

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

theorem Tdaf.ConvexAnalysis.recessionFn_conj_le_supportFn_dom {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) (f : E → EReal) : recessionFn (conj B f) ≤ supportFn B (dom f)

The unconditional half: (f*) 0⁺ ≤ δ*(· | dom f).

Bounding the supremum that defines f* termwise: off dom f the term is ⊥, and on dom f the bound ⟨x, y⟩ ≤ ν moves a⟨x, y⟩ past the supremum.

theorem Tdaf.ConvexAnalysis.supportFn_dom_le_recessionFn_conj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} (hp : Proper f) (hc : Proper (conj B f)) : supportFn B (dom f) ≤ recessionFn (conj B f)

The half that needs properness of f*: δ*(· | dom f) ≤ (f*) 0⁺.

Proper (conj B f) supplies a z at which f* is finite; Fenchel's inequality at z + a • y then reads ⟨x, z⟩ + a⟨x, y⟩ - f x ≤ f* z + a ν, and letting a → ∞ forces ⟨x, y⟩ ≤ ν.

theorem Tdaf.ConvexAnalysis.recessionFn_conj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} (hp : Proper f) (hc : Proper (conj B f)) : recessionFn (conj B f) = supportFn B (dom f)

The recession function of a conjugate is the support function of the effective domain, (f*) 0⁺ = δ*(· | dom f).

theorem Tdaf.ConvexAnalysis.constancySpace_conj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} (hp : Proper f) (hc : Proper (conj B f)) : constancySpace (conj B f) = {y : F | ∀ x ∈ dom f, (B x) y = 0}

The constancy space of a conjugate is the annihilator of the effective domain. This is what the constancy hypothesis of the image theorem becomes for f*: "f* is constant along y" says exactly that y pairs to zero with every point of dom f.

Recession cones and polars of effective domains

theorem Tdaf.ConvexAnalysis.recessionConeFn_conj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} (hp : Proper f) (hc : Proper (conj B f)) : recessionConeFn (conj B f) = polarCone B (dom f)

The recession cone of a conjugate is the polar of the effective domain. Stated against dom f rather than the cone it generates, which a polar cone cannot tell apart from it; recessionConeFn_conj_hull is the cone-generated phrasing. The proof reads the support-function identity at the level 0: (f*)0⁺ y ≤ 0 says ⟨x, y⟩ ≤ 0 for every x ∈ dom f.

theorem Tdaf.ConvexAnalysis.recessionConeFn_conj_hull {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} (hp : Proper f) (hc : Proper (conj B f)) : polarCone B ↑(PointedCone.hull ℝ (dom f)) = recessionConeFn (conj B f)

The same in cone-generated form: the polar of the convex cone generated by dom f is the recession cone of f*.

theorem Tdaf.ConvexAnalysis.recessionConeFn_eq_polarCone_dom_conj {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {f : E → EReal} (hf : ConvexFn f) (hcl : ClosedFn f) (hp : Proper f) : recessionConeFn f = polarCone B.flip (dom (conj B f))

Before polars are taken: the recession cone of a closed proper convex function is the polar of the effective domain of its conjugate — the previous result applied to f*, using f** = f. This is the form the existence theory for minimisers consumes.

theorem Tdaf.ConvexAnalysis.polarCone_recessionConeFn {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] [LocallyConvexSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] {f : E → EReal} (hf : ConvexFn f) (hcl : ClosedFn f) (hp : Proper f) : polarCone B (recessionConeFn f) = closure ↑(PointedCone.hull ℝ (dom (conj B f)))

The polar of the recession cone of a closed proper convex function is the closure of the convex cone generated by dom f*. Take polars in recessionConeFn_eq_polarCone_dom_conj and apply the bipolar theorem.

Bounded level sets

theorem Tdaf.ConvexAnalysis.zero_mem_interior_iff_polarCone_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] {D : Set F} (hD : Convex ℝ D) (hne : D.Nonempty) : 0 ∈ interior D ↔ polarCone B.flip D = {0}

The origin is interior to a convex set exactly when its polar cone is trivial. Both directions run on the absorbency criterion for interior points: forwards, absorbency at the origin makes every value of the pairing vanish, and the pairing separates points; backwards, the bipolar theorem turns a trivial polar into "the cone generated by D is dense", which passing to the relative interior of a closure upgrades to absorbency again. Nonemptiness is not decorative: for D = ∅ between two trivial spaces the polar is {0} while the interior is empty.

theorem Tdaf.ConvexAnalysis.isBounded_setOf_le_iff_zero_mem_interior_dom_conj {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] {f : E → EReal} (hf : ConvexFn f) (hcl : ClosedFn f) (hp : Proper f) : (∀ (α : ℝ), Bornology.IsBounded {z : E | f z ≤ ↑α}) ↔ 0 ∈ interior (dom (conj B f))

Every level set of a closed proper convex function is bounded exactly when the origin is interior to the effective domain of the conjugate. The polar dictionary turns the recession cone of f into the polar of dom f*, every nonempty level set has that same recession cone, and a nonempty closed convex set is bounded exactly when its recession cone is trivial.