Exact duality: when the closure may be omitted #
Almost every "exact" duality statement has the shape
if
ri (dom f₁) ∩ … ∩ ri (dom fₘ) ≠ ∅then the closure operation can be dropped and the infimum defining the dual operation is attained
(conjugates of sums, of inverse images and of suprema; subdifferential calculus; the duality theorems of convex programming). The relative interior condition is one sufficient condition among several; there are polyhedral variants, a continuity variant valid in any topological vector space, and Attouch–Brezis conditions in Banach spaces.
This file names the conclusion. IsExactSum and IsExactImage are hypothesis-only interfaces,
and the sufficient conditions for them are proved in the module that owns each hypothesis
(IsExactSum.of_relint in Duality/Relint.lean, .of_polyhedral in Polyhedral/Duality.lean).
Main definitions #
IsExactSum B f g—fandgadd exactly: both are proper, and the infimal convolution defining(f + g)*is attained.IsExactFinsetSum B s f— the same for a finite family, the form them-ary statements need.IsExactImage B B' A A' hA g—gpulls back exactly alongA:gis proper, and the infimum defining(g A)*over the fibres of the transposeA'is attained.
Main results #
conj_add_le_infConv,conj_compLin_le_mapLin,conj_finsetSum_le_sum_toInfConvFn— the unconditional halves:(f + g)* ≤ f* □ g*and(g A)* ≤ A' (g*), with no hypothesis at all.IsExactSum.conj_add,IsExactSum.exists_conj_add_eq— the exact half for a sum:(f + g)* = f* □ g*with the infimal convolution attained (Theorem 16.4 in [^1]);IsExactFinsetSum.conj_finsetSumis them-ary form.IsExactImage.conj_compLin,IsExactImage.exists_conj_compLin_eq— the exact half for an inverse image:(g A)* = A' (g*), the infimum over the fibre attained (Theorem 16.3 in [^1]).IsExactFinsetSum.singleton,.cons,.of_split— the family interface built out of binary ones, which is how everym-ary constraint qualification is discharged.IsExactSum.proper_add,IsExactFinsetSum.proper_finsetSum,IsExactImage.proper_compLin— the interfaces are unsatisfiable when the effective domains miss each other.
Implementation notes #
The equality is a theorem, not a field of the structure. (f + g)* ≤ f* □ g* holds for arbitrary
f and g, and an interface stating the equality would be unsatisfiable where it looks most
innocent: when dom f ∩ dom g = ∅ we have (f + g)* ≡ -∞, while the conjugate of a proper
function is never -∞. What the interface carries is the attainment, exact_le.
IsExactImage.exact_le asks for a point of the fibre A' ⁻¹' {y} only where (g A)* y is finite.
Without that guard the interface is unsatisfiable whenever A' is not surjective: at a y outside
the range of A' there is no z to produce, while both sides of the identity are legitimately
+∞ there.
The family interface is not an iterated binary one: □ does not preserve ≠ ⊥, so the binary
bound cannot be iterated, and what iterates is the construction, IsExactFinsetSum.cons. And
exact_le demands a splitting of every y, so IsExactFinsetSum B ∅ f forces F to be trivial —
the empty family is not exact, just as two functions with disjoint effective domains are not.
References #
[^1]: R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §16, §20, §23, §31.
Sums: the unconditional half #
An affine minorant of f and one of g add to an affine minorant of f + g. Read through
conj_le_coe_iff this is the whole unconditional content of the conjugate-of-a-sum identity.
Unconditionally, the conjugate of a sum is at most the infimal convolution of the
conjugates, for arbitrary f and g. The reverse inequality is what IsExactSum asks for, and
what every constraint qualification exists to supply.
The pointwise form of conj_add_le_infConv, which is not unconditional: if f ≡ +∞ and g
takes -∞ somewhere then (f + g)* ≡ +∞ while f* y₁ + g* y₂ = ⊥ + ⊤ = ⊥. Nonempty effective
domains rule that out.
Sums: the interface #
f and g add exactly with respect to the pairing B: both are proper, and the infimal
convolution f* □ g* is attained at every point — equivalently (IsExactSum.conj_add), the
conjugate of the sum is the infimal convolution of the conjugates. This is the conclusion the
relative-interior and polyhedral qualifications both deliver.
- proper_left : Proper f
The left summand is proper.
- proper_right : Proper g
The right summand is proper.
At every
ythe infimal convolution defining(f + g)*is attained: some splittingy = y₁ + y₂already achieves the value. The reverse inequality is unconditional (conj_add_le_infConv), so this is the entire content.
Instances For
The interface rules out disjoint effective domains: the sum of two exactly-adding functions is itself proper.
The exact half: the conjugate of a sum is the infimal convolution of the conjugates.
The infimal convolution is attained, which is the half the constraint qualifications are for.
The pointwise m-ary form: (f₁ + ⋯ + fₘ)* (y₁ + ⋯ + yₘ) ≤ f₁* y₁ + ⋯ + fₘ* yₘ. Nonempty
effective domains keep the right-hand side from collapsing to ⊥ through a ⊤ + ⊥.
The m-ary form, unconditionally:
(f₁ + ⋯ + fₘ)* ≤ f₁* □ ⋯ □ fₘ*, the □-product being the AddCommMonoid sum of InfConvFn F.
No properness may be assumed at the intermediate stages, since □ does not preserve it; the
induction runs on infConv_mono and never re-enters the infimum formula.
A finite family (fᵢ)_{i ∈ s} adds exactly with respect to the pairing B: every member
is proper, and the m-fold infimal convolution f₁* □ ⋯ □ fₘ* is attained at every point —
equivalently, the conjugate of f₁ + ⋯ + fₘ is f₁* □ ⋯ □ fₘ*.
IsExactSum is the case of two. Every consequence below is proved once, for the family;
IsExactFinsetSum.cons and .of_split build a family interface out of binary ones.
Every member of the family is proper.
- exact_le (y : F) : ∃ (y' : ι → F), ∑ i ∈ s, y' i = y ∧ ∑ i ∈ s, conj B (f i) (y' i) ≤ conj B (∑ i ∈ s, f i) y
At every
ythem-fold infimal convolution defining(f₁ + ⋯ + fₘ)*is attained: some splittingy = y₁ + ⋯ + yₘalready achieves the value. The reverse inequality is unconditional (conj_finsetSum_le_sum_toInfConvFn), so this is the entire content.
Instances For
The interface rules out effective domains with empty intersection, exactly as in the binary case.
The m-ary exact half: the conjugate of a finite sum is the infimal convolution of the
conjugates.
The m-fold infimal convolution is attained, which is the half the constraint
qualifications are for:
(f₁ + ⋯ + fₘ)* y = inf {f₁* y₁ + ⋯ + fₘ* yₘ | y₁ + ⋯ + yₘ = y}, with the infimum attained.
A one-element family adds exactly as soon as its member is proper: there is nothing to
split. This is the base case of every m-ary constraint qualification.
Adjoining one summand. A family adds exactly as soon as its tail does and the new summand
adds exactly to the sum of the tail: the induction step every m-ary constraint qualification
runs on.
Gluing two exactly-adding subfamilies. If s splits into disjoint t and u, both of
which add exactly, and the two partial sums add exactly to each other, then s adds exactly. This
is the form the polyhedral proof uses, with t the polyhedral indices and u the rest; the
splitting is spelled pointwise so that no DecidableEq instance is needed.
Images #
Unconditionally, the conjugate of the inverse image g A is at most the image under the
transpose of the conjugate of g. Only the adjointness datum is used.
g pulls back exactly along A: g is proper, and the infimum over the fibres of the
transpose A' that defines A' (g*) is attained — equivalently, (g A)* = A' (g*).
The transpose A' and the adjointness hA are data: between arbitrarily paired spaces a linear
map need not have an adjoint at all.
- proper : Proper g
The function being pulled back is proper.
- exact_le (y : F) : conj B (compLin g A) y < ⊤ → ∃ (z : H), A' z = y ∧ conj B' g z ≤ conj B (compLin g A) y
Wherever
(g A)* yis finite, the infimum definingA' (g*) yis attained on the fibre ofA'overy. The reverse inequality is unconditional (conj_compLin_le_mapLin).The guard
(g A)* y < ⊤is not a weakening of convenience: without it the field would demand a point of the fibreA' ⁻¹' {y}for everyy, i.e. it would silently forceA'to be surjective.
Instances For
The exact half: the conjugate of an inverse image is the image of the conjugate under the transpose.
The infimum over the fibre is attained, which is the half the constraint qualifications are for.