When a subspace meets a relative interior

The constraint qualifications of the exactness theory — "the range of A meets ri (dom g)", "the effective domains have a common relative interior point" — are primal conditions. This file turns them into dual ones: statements about the directions of the pairing in which the sets are bounded.

The engine is proper separation. Two nonempty convex sets have disjoint relative interiors exactly when some hyperplane separates them properly, and over a compatible pairing the separating functional is ⟨·, y⟩ for a y of the second space; the two conditions defining proper separation then read as two inequalities between values of the pairing. When one of the two sets is a subspace L, a direction in which the pairing is bounded on L is one in which it vanishes on L, so both extrema over L collapse to 0 and the condition becomes a statement about a single set together with the annihilator of L.

Main results

• exists_pairing_le_iff_disjoint_relint — proper separation over a pairing: ri C₁ and ri C₂ are disjoint exactly when the pairing with some y is nowhere larger on C₁ than on C₂ and is strictly smaller somewhere.
• submodule_inter_relint_nonempty_iff, submodule_inter_relint_nonempty_iff_supportFn — the subspace case, pointwise and through the support function.
• submodule_inter_relint_dom_nonempty_iff — the effective-domain case, with the support function of dom f rewritten as the recession function of f* (Lemma 16.2 in [^1]).
• exists_apply_mem_relint_dom_iff — the same for the range of a linear map, whose annihilator on the other side of the pairing is the kernel of the adjoint (Corollary 16.2.1 in [^1]).

Implementation notes

The general statement is written with pointwise inequalities ⟨x₁, y⟩ ≤ ⟨x₂, y⟩, which mention no EReal; the support function appears only once one of the two sets is a subspace, where two of the four extrema of the proper-separation criterion become 0.

Only E is topologised: proper separation happens there and needs finite dimension, while F enters through IsCompatiblePairing alone and is a bare module. Proper (conj B f) is a hypothesis rather than a conclusion, following recessionFn_conj; a caller in finite dimensions discharges it with proper_conj_of_proper.

References

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

Boundedness on a subspace

theorem Tdaf.ConvexAnalysis.forall_pairing_eq_zero_of_forall_le {E : Type u_1} {F : Type u_2} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {y : F} {L : Submodule ℝ E} {c : ℝ} (h : ∀ x ∈ L, (B x) y ≤ c) (x : E) : x ∈ L → (B x) y = 0

A linear function bounded above on a subspace vanishes on it. A subspace is closed under arbitrary real scaling, so a single nonzero value would make the pairing unbounded.

A subspace is relatively open

theorem Tdaf.ConvexAnalysis.intrinsicInterior_coe_submodule {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℝ E) : intrinsicInterior ℝ ↑L = ↑L

The relative interior of a subspace is the subspace itself.

Proper separation, read through the pairing

theorem Tdaf.ConvexAnalysis.exists_pairing_le_iff_disjoint_relint {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {C₁ C₂ : Set E} (h₁ : Convex ℝ C₁) (h₂ : Convex ℝ C₂) (hne₁ : C₁.Nonempty) (hne₂ : C₂.Nonempty) : (∃ (y : F), (∀ x₁ ∈ C₁, ∀ x₂ ∈ C₂, (B x₁) y ≤ (B x₂) y) ∧ ∃ x₁ ∈ C₁, ∃ x₂ ∈ C₂, (B x₁) y < (B x₂) y) ↔ Disjoint (intrinsicInterior ℝ C₁) (intrinsicInterior ℝ C₂)

Proper separation over a pairing. Two nonempty convex sets have disjoint relative interiors exactly when the pairing with some y is nowhere larger on C₁ than on C₂ and is strictly smaller at one pair of points.

theorem Tdaf.ConvexAnalysis.submodule_inter_relint_nonempty_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {C : Set E} (L : Submodule ℝ E) (hC : Convex ℝ C) (hne : C.Nonempty) : (↑L ∩ intrinsicInterior ℝ C).Nonempty ↔ ¬∃ (y : F), (∀ x ∈ L, (B x) y = 0) ∧ (∀ x ∈ C, (B x) y ≤ 0) ∧ ∃ x ∈ C, (B x) y < 0

A subspace meets the relative interior of a convex set exactly when no direction of the pairing annihilates the subspace, is nowhere positive on the set and is negative somewhere on it. The annihilator condition is not assumed but implied: a direction along which the pairing is bounded below on a subspace vanishes on it.

theorem Tdaf.ConvexAnalysis.submodule_inter_relint_nonempty_iff_supportFn {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {C : Set E} (L : Submodule ℝ E) (hC : Convex ℝ C) (hne : C.Nonempty) : (↑L ∩ intrinsicInterior ℝ C).Nonempty ↔ ¬∃ (y : F), (∀ x ∈ L, (B x) y = 0) ∧ supportFn B C y ≤ 0 ∧ 0 < supportFn B C (-y)

A subspace meets the relative interior of a convex set, with the two conditions on the set read off its support function: δ*(y | C) ≤ 0 and δ*(-y | C) > 0.

The effective domain of a convex function

theorem Tdaf.ConvexAnalysis.submodule_inter_relint_dom_nonempty_iff {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [AddCommGroup F] [Module ℝ F] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} [IsCompatiblePairing B] {f : E → EReal} (L : Submodule ℝ E) (hf : ConvexFn f) (hp : Proper f) (hc : Proper (conj B f)) : (↑L ∩ intrinsicInterior ℝ (dom f)).Nonempty ↔ ¬∃ (y : F), (∀ x ∈ L, (B x) y = 0) ∧ recessionFn (conj B f) y ≤ 0 ∧ 0 < recessionFn (conj B f) (-y)

A subspace L meets ri (dom f) exactly when there is no y annihilating L with (f*) 0⁺ y ≤ 0 < (f*) 0⁺ (-y). The support function of dom f is the recession function of f* (recessionFn_conj), so this is the previous statement at C = dom f.

The range of a linear transformation

theorem Tdaf.ConvexAnalysis.forall_mem_range_eq_zero_iff {E : Type u_1} {F : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [AddCommGroup H] [Module ℝ H] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {B' : G →ₗ[ℝ] H →ₗ[ℝ] ℝ} {A : E →ₗ[ℝ] G} {A' : H →ₗ[ℝ] F} (hB : B.SeparatingRight) (hA : IsAdjointPair B B' A A') (y : H) : (∀ z ∈ A.range, (B' z) y = 0) ↔ A' y = 0

The annihilator of the range of A is the kernel of its adjoint. B.SeparatingRight is what recovers A' y = 0 from "⟨·, A' y⟩ vanishes identically".

theorem Tdaf.ConvexAnalysis.exists_apply_mem_relint_dom_iff {E : Type u_1} {F : Type u_2} {G : Type u_3} {H : Type u_4} [AddCommGroup E] [Module ℝ E] [AddCommGroup F] [Module ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] [AddCommGroup H] [Module ℝ H] {B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ} {B' : G →ₗ[ℝ] H →ₗ[ℝ] ℝ} [IsCompatiblePairing B'] {A : E →ₗ[ℝ] G} {A' : H →ₗ[ℝ] F} {g : G → EReal} (hB : B.SeparatingRight) (hA : IsAdjointPair B B' A A') (hg : ConvexFn g) (hp : Proper g) (hc : Proper (conj B' g)) : (∃ (x : E), A x ∈ intrinsicInterior ℝ (dom g)) ↔ ¬∃ (y : H), A' y = 0 ∧ recessionFn (conj B' g) y ≤ 0 ∧ 0 < recessionFn (conj B' g) (-y)

For a linear transformation A with adjoint A' and a proper convex g, some A x lies in ri (dom g) exactly when no y in the kernel of A' has (g*) 0⁺ y ≤ 0 < (g*) 0⁺ (-y): the subspace criterion above for L = range A.