The relative-interior constraint qualification

Duality/Exact.lean names the conclusions IsExactImage and IsExactSum — that a conjugate formula holds with the infimum attained. This file supplies the first sufficient condition for each, the classical relative-interior hypothesis:

A ⁻¹' ri (dom g) ≠ ∅        and        ri (dom f) ∩ ri (dom g) ≠ ∅.

Both reduce to the same two ingredients: closedness of the dual object — a linear image, or a sum, of closed convex sets — and the fact that a linear function which is ≤ 0 on a convex set and attains that bound at a relative interior point is constant on the set.

Main results

• IsExactImage.of_relint — a proper convex g pulls back exactly along a linear map whose range meets ri (dom g) (Theorem 16.3 in [^1]). IsExactImage.of_relint_closed is the closed case, which carries the argument.
• IsExactSum.of_relint — two proper convex functions whose effective domains share a relative interior point add exactly (Theorem 16.4 in [^1]); IsExactSum.of_relint_closed is again the closed case, and IsExactFinsetSum.of_relint the m-ary form.
• TendstoClFnAlongSegment — "cl f is the limit of f along segments issuing from x₀", the single hypothesis shared by the two ways of obtaining it: x₀ ∈ ri (dom f) for a proper convex f, and x₀ ∈ dom f for a closed proper convex one.
• conj_add_eq_conj_clFn_add_clFn, conj_compLin_eq_conj_compLin_clFn — passing to closures does not change the conjugate of a sum or of a composition, which is what removes closedness from the two constructors.
• proper_conj_of_proper — in finite dimensions a proper convex f already has f* proper, with no closedness hypothesis.

Implementation notes

Closures are compared in the conjugate form (f + g)* = (cl f + cl g)* rather than as cl (f + g) = cl f + cl g (which is clFn_add, in Recession/Closedness.lean). The conjugate form is weaker but cheaper: the identity of closures needs the segment limit for f + g as well, hence a relative interior point of both domains, whereas the conjugate form makes do with a point of dom f and one of ri (dom g).

The two rules topologise opposite spaces. The image rule puts the image closedness theorem on H, so H must be finite-dimensional, and ri (dom g) puts G there too; F only receives an image and E is never topologised. The sum rule is the reverse: ri (dom f) needs only a normed E, while the sum closedness theorem runs in F × ℝ and so F must be finite-dimensional.

References

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

theorem Tdaf.ConvexAnalysis.mem_constancySpace_conj_of_relint {E : Type u_1} {F : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup E] [Module ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup H] [NormedSpace ℝ H] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {B' : G →ₗ[ℝ] H →ₗ[ℝ] ℝ} {A : E →ₗ[ℝ] G} {A' : H →ₗ[ℝ] F} {g : G → EReal} [IsCompatiblePairing B'] [IsCompatiblePairing B'.flip] (hA : IsAdjointPair B B' A A') (hg : ClosedProperConvexFn g) {x₀ : E} (hx₀ : A x₀ ∈ intrinsicInterior ℝ (dom g)) {z : H} (hrec : recessionFn (conj B' g) z ≤ 0) (hz0 : A' z = 0) : z ∈ constancySpace (conj B' g)

The image closedness hypothesis for g* and the transpose A', discharged from the relative-interior condition: "g* recedes along z, and A' kills z" says that ⟨·, z⟩ is ≤ 0 on dom g and vanishes at A x₀ ∈ ri (dom g), which makes it constant there.

theorem Tdaf.ConvexAnalysis.IsExactImage.of_relint_closed {E : Type u_1} {F : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup E] [Module ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {B' : G →ₗ[ℝ] H →ₗ[ℝ] ℝ} {A : E →ₗ[ℝ] G} {A' : H →ₗ[ℝ] F} {g : G → EReal} [IsCompatiblePairing B'] [IsCompatiblePairing B'.flip] [IsCompatiblePairing B.flip] (hA : IsAdjointPair B B' A A') (hg : ClosedProperConvexFn g) {x₀ : E} (hx₀ : A x₀ ∈ intrinsicInterior ℝ (dom g)) : IsExactImage B B' A A' hA g

A closed proper convex function pulls back exactly along a linear map whose range meets the relative interior of its effective domain.

Sums

theorem Tdaf.ConvexAnalysis.le_of_mk_mem_recessionCone_epi_conj {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} [IsCompatiblePairing B] (hf : ClosedProperConvexFn f) {z : F} {ν : ℝ} (hp : (z, ν) ∈ recessionCone (epi (conj B f))) {x : E} (hx : x ∈ dom f) : (B x) z ≤ ν

A direction of recession of epi f* bounds the pairing on dom f: the recession function of f* is the support function of dom f, read one point at a time.

theorem Tdaf.ConvexAnalysis.mk_mem_linealitySpace_epi_conj_of_relint {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} [IsCompatiblePairing B] (hf : ClosedProperConvexFn f) {x₀ : E} (hx₀ : x₀ ∈ intrinsicInterior ℝ (dom f)) {z : F} {ν : ℝ} (hp : (z, ν) ∈ recessionCone (epi (conj B f))) (hν : ν ≤ (B x₀) z) : (z, ν) ∈ linealitySpace (epi (conj B f))

The relative-interior step for sums. If (z, ν) is a direction of recession of epi f* whose bound ν is already attained at a relative interior point of dom f, then (z, ν) lies in the lineality space: the recession direction reads as "⟨·, z⟩ ≤ ν on dom f", and a bound attained at a relative interior point is attained across the whole domain.

theorem Tdaf.ConvexAnalysis.IsExactSum.of_relint_closed {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f g : E → EReal} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] (hf : ClosedProperConvexFn f) (hg : ClosedProperConvexFn g) {x₀ : E} (hxf : x₀ ∈ intrinsicInterior ℝ (dom f)) (hxg : x₀ ∈ intrinsicInterior ℝ (dom g)) : IsExactSum B f g

Two closed proper convex functions add exactly as soon as their effective domains have a common relative interior point.

The proof is the closedness of a sum of convex sets, applied to epi f* and epi g*: once their sum is closed it is the epigraph of f* □ g*, and the splitting supplied at each of its points is the attainment IsExactSum.exact_le asks for.

Dropping closedness from the constraint qualifications

def Tdaf.ConvexAnalysis.TendstoClFnAlongSegment {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → EReal) (x₀ : E) : Prop

f is recovered along segments issuing from x₀: at every y the value (cl f) y is the limit of f along the half-open segment from x₀ to y.

This holds for a proper convex f when x₀ ∈ ri (dom f), and for a closed proper convex f when x₀ ∈ dom f. It is the only property of x₀ the closure-removal argument uses, so the two constraint qualifications run through one and the same lemma.

Equations

• Tdaf.ConvexAnalysis.TendstoClFnAlongSegment f x₀ = ∀ (y : E), Filter.Tendsto (fun (a : ℝ) => f ((1 - a) • x₀ + a • y)) (nhdsWithin 1 (Set.Iio 1)) (nhds (Tdaf.ConvexAnalysis.clFn f y))

theorem Tdaf.ConvexAnalysis.proper_conj_of_proper {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f : E → EReal} [IsCompatiblePairing B] (hf : ConvexFn f) (hp : Proper f) : Proper (conj B f)

In finite dimensions the conjugate of a proper convex function is proper, with no closedness hypothesis. It goes through the properness of cl f, which is where finite-dimensionality enters: f* = (cl f)*, and cl f is closed proper convex.

theorem Tdaf.ConvexAnalysis.ConvexFn.tendstoClFnAlongSegment {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf : ConvexFn f) (hp : Proper f) {x₀ : E} (hx₀ : x₀ ∈ intrinsicInterior ℝ (dom f)) : TendstoClFnAlongSegment f x₀

A proper convex function is recovered along segments issuing from any relative interior point of its effective domain.

theorem Tdaf.ConvexAnalysis.ClosedProperConvexFn.tendstoClFnAlongSegment {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} (hf : ClosedProperConvexFn f) {x₀ : E} (hx₀ : x₀ ∈ dom f) : TendstoClFnAlongSegment f x₀

A closed proper convex function is recovered along segments issuing from any point of its effective domain — no relative interior needed.

theorem Tdaf.ConvexAnalysis.conj_add_eq_conj_clFn_add_clFn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f g : E → EReal} (hf : ConvexFn f) (hpf : Proper f) (hg : ConvexFn g) (hpg : Proper g) {x₀ : E} (hsf : TendstoClFnAlongSegment f x₀) (hsg : TendstoClFnAlongSegment g x₀) : conj B (f + g) = conj B (clFn f + clFn g)

Passing to closures does not change the conjugate of a sum, in the form the constraint qualifications consume: if two proper convex functions are both recovered along segments issuing from one common point, then f + g and cl f + cl g have the same conjugate.

The stronger cl (f + g) = cl f + cl g needs the segment limit for f + g as well, hence a point of ri (dom f) ∩ ri (dom g). The conjugate form needs no such thing, since f* = (cl f)* holds outright; that is what lets a caller make do with a point of dom f and one of ri (dom g).

theorem Tdaf.ConvexAnalysis.IsExactSum.of_clFn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f g : E → EReal} [IsContinuousPairing B] (hpf : Proper f) (hpg : Proper g) (h : IsExactSum B (clFn f) (clFn g)) (hconj : conj B (f + g) = conj B (clFn f + clFn g)) : IsExactSum B f g

Exactness passes from the closures to the functions themselves, as soon as the sum has not changed its conjugate. conj_add_eq_conj_clFn_add_clFn is what supplies the second hypothesis.

theorem Tdaf.ConvexAnalysis.IsExactSum.of_relint {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {f g : E → EReal} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] (hf : ConvexFn f) (hpf : Proper f) (hg : ConvexFn g) (hpg : Proper g) {x₀ : E} (hxf : x₀ ∈ intrinsicInterior ℝ (dom f)) (hxg : x₀ ∈ intrinsicInterior ℝ (dom g)) : IsExactSum B f g

Two proper convex functions add exactly as soon as their effective domains have a relative interior point in common. Closedness is not needed; conj_add_eq_conj_clFn_add_clFn and the invariance of ri (dom f) under closure reduce it to IsExactSum.of_relint_closed.

Dropping closedness on the image side

theorem Tdaf.ConvexAnalysis.conj_compLin_eq_conj_compLin_clFn {E : Type u_1} {F : Type u_2} {G : Type u_3} [AddCommGroup E] [Module ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {g : G → EReal} (A : E →ₗ[ℝ] G) {x₀ : E} (hs : TendstoClFnAlongSegment g (A x₀)) : conj B (compLin g A) = conj B (compLin (clFn g) A)

Passing to closures does not change the conjugate of a composition: if g is recovered along segments issuing from A x₀, then g A and (cl g) A have the same conjugate.

Cheaper than conj_add_eq_conj_clFn_add_clFn: one limit rather than two, so no properness is needed, and E need not be topologised since the segment is pushed forward by A before any limit is taken. The book's form here is cl (g A) = (cl g) A (clFn_compLin), which does need E finite-dimensional.

theorem Tdaf.ConvexAnalysis.IsExactImage.of_relint {E : Type u_1} {F : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup E] [Module ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] [NormedAddCommGroup H] [NormedSpace ℝ H] [FiniteDimensional ℝ H] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {B' : G →ₗ[ℝ] H →ₗ[ℝ] ℝ} {A : E →ₗ[ℝ] G} {A' : H →ₗ[ℝ] F} {g : G → EReal} [IsCompatiblePairing B'] [IsCompatiblePairing B'.flip] [IsCompatiblePairing B.flip] (hA : IsAdjointPair B B' A A') (hg : ConvexFn g) (hp : Proper g) {x₀ : E} (hx₀ : A x₀ ∈ intrinsicInterior ℝ (dom g)) : IsExactImage B B' A A' hA g

A proper convex g pulls back exactly along a linear map whose range meets ri (dom g). Closedness is not needed; the reduction to IsExactImage.of_relint_closed is conj_compLin_eq_conj_compLin_clFn together with the fact that cl g has the same relative interior of effective domain.

Finitely many summands

theorem Tdaf.ConvexAnalysis.properConvexFn_finsetSum {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : Finset ι} {f : ι → E → EReal} (hf : ∀ i ∈ s, ConvexFn (f i)) (hpf : ∀ i ∈ s, Proper (f i)) {x₀ : E} (hx₀ : ∀ i ∈ s, x₀ ∈ dom (f i)) : ConvexFn (∑ i ∈ s, f i) ∧ Proper (∑ i ∈ s, f i) ∧ dom (∑ i ∈ s, f i) = ⋂ i ∈ s, dom (f i)

The sum of a finite family of proper convex functions with a common domain point, packaged as the three facts the binary constraint qualifications ask about it.

theorem Tdaf.ConvexAnalysis.mem_relint_dom_finsetSum {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Finset ι} {f : ι → E → EReal} (hf : ∀ i ∈ s, ConvexFn (f i)) (hpf : ∀ i ∈ s, Proper (f i)) {x₀ : E} (hx₀ : ∀ i ∈ s, x₀ ∈ intrinsicInterior ℝ (dom (f i))) : x₀ ∈ intrinsicInterior ℝ (dom (∑ i ∈ s, f i))

The relative interior of the effective domain of a sum: a point lying in the relative interior of every dom fᵢ lies in the relative interior of dom (f₁ + ⋯ + fₘ).

theorem Tdaf.ConvexAnalysis.IsExactFinsetSum.of_relint {ι : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {s : Finset ι} {f : ι → E → EReal} [IsCompatiblePairing B] [IsCompatiblePairing B.flip] (hs : s.Nonempty) (hf : ∀ i ∈ s, ConvexFn (f i)) (hpf : ∀ i ∈ s, Proper (f i)) {x₀ : E} (hx₀ : ∀ i ∈ s, x₀ ∈ intrinsicInterior ℝ (dom (f i))) : IsExactFinsetSum B s f

Finitely many proper convex functions add exactly as soon as the relative interiors of their effective domains have a point in common.

The induction is IsExactFinsetSum.cons; beyond the binary case it needs only that the effective domain of a partial sum is ⋂ dom fᵢ and that x₀ lies in the relative interior of that intersection (mem_relint_dom_finsetSum).