Auxiliary lemmas about EReal #
Convex analysis over EReal needs a handful of order and arithmetic facts that Mathlib does not
provide directly. They are collected here so that they do not accumulate as ad hoc haves
throughout the library.
Rockafellar's arithmetic conventions #
Rockafellar (Convex Analysis, §4) fixes the conventions
α + ∞ = ∞for-∞ < α ≤ ∞,α - ∞ = -∞for-∞ ≤ α < ∞,0 · ∞ = 0,inf ∅ = +∞,sup ∅ = -∞,
and leaves ∞ - ∞ undefined, avoiding it by properness hypotheses. Every one of these agrees
with the corresponding fact about EReal in Mathlib, so no bespoke arithmetic type is needed; see
the examples below, which are exactly the conventions listed in the book.
Negation distributes over an EReal sum as soon as neither summand is ⊤, so that the
forbidden ∞ - ∞ cannot arise. Mathlib's EReal.neg_add has the sharpest hypotheses; this is the
symmetric special case that concave/convex sign transfer actually uses.
The hypotheses of Tdaf.EReal.neg_combo are load-bearing: at u = ⊤, v = ⊥ the two sides
are ⊥ and ⊤.
Multiplication by a positive real scalar reflects, as well as preserves, the order on EReal.
The reflection direction is proved by multiplying by the inverse scalar, since EReal has
PosMulMono but not PosMulStrictMono.
If z is at most every positive real, then z ≤ 0. The conclusion is genuinely weaker
than z ≤ r for a fixed r: z may be any non-positive extended real. It is how "the optimal
value is not positive" is extracted from feasible solutions whose values tend to 0.
A positive real factor distributes over a sum whose right summand is real. No side
condition beyond 0 < l is needed: l * ⊤ = ⊤ and l * ⊥ = ⊥ for l > 0, and a real summand
can cancel neither.
If a finite sum of EReals none of which is ⊥ is not ⊤, then no term is ⊤. This is the
form in which "the sum is unambiguous" gets used: it turns a finite bound on a sum into a finite
bound on each term.
The symmetry of Fenchel's inequality, and the single EReal fact that carries the whole of
§12: a - z ≤ w ↔ a - w ≤ z whenever a is a real number. There is no side condition: all eight
degenerate combinations of ⊥ and ⊤ work out, because a is finite.
The mirror of Tdaf.EReal.coe_sub_le_comm, for the concave side of the theory:
z ≤ a - w ↔ w ≤ a - z whenever a is a real number. It says that z ↦ a - z is an antitone
involution of EReal, and, like its convex counterpart, it carries no side condition.
Multiplication by a positive real commutes with an infimum. EReal has PosMulMono but no
PosMulStrictMono, so the reverse inequality goes through a⁻¹.
Negation exchanges suprema and infima. Unlike addition, negation is an order-reversing
involution of EReal with no exceptional values, so this needs no hypothesis. It is what turns
every statement about conj into one about concaveConj.
The companion of Tdaf.EReal.neg_iSup.
Negating a difference whose minuend is a real number turns it around, with no side
condition: the finite term rules out both ∞ - ∞ collisions by itself, where the unrestricted
EReal.neg_sub needs two hypotheses.
Negation turns a difference around, provided neither of the two ∞ - ∞ collisions occurs.
EReal.neg_sub's hypotheses are a disjunction each; this and neg_sub_comm' are the two ways of
satisfying them. neg_coe_sub above is the case where a finite minuend satisfies both at once.
A constant that is not -∞ slides out of a supremum as a subtrahend. The hypothesis rules
out the disagreement at c = ⊥: there (⨆ i, u i) - ⊥ is ⊤ as soon as the supremum is not ⊥,
while u i - ⊥ is ⊤ only where u i ≠ ⊥. Over an empty index set both sides are ⊥.
The dual of Tdaf.EReal.iSup_add_coe, and like it hypothesis-free: the empty index set works
too, since ⊤ + r = ⊤.
The set-indexed form of Tdaf.EReal.iSup_add_coe.
The set-indexed form of Tdaf.EReal.iInf_add_coe.
The supremum of a sum splits, provided neither family takes ⊥; if either index set is
empty both sides are ⊥. This is what turns "the epigraph of an infimal convolution is a sum of
epigraphs" into "the conjugate of an infimal convolution is a sum of conjugates" (Theorem 16.4).
A real constant may be moved in and out of an infimum from the left. The mirror of
Tdaf.EReal.iInf_add_coe, which has it on the right.
An arbitrary constant may be moved in and out of an infimum whose value is not ⊥. Note
where the hypothesis sits: for suprema (Tdaf.EReal.biSup_add_of_ne_bot) it is the values that
must avoid ⊥; here it is the infimum itself.
The infimum of a sum splits, provided neither infimum is ⊥. The infimal mirror of
Tdaf.EReal.biSup_add_biSup, but with a different hypothesis: for suprema it is the values that
must avoid ⊥, here it is the two infima themselves.
An infimum over a product of a separated sum splits, under the single hypothesis that
neither infimum is ⊤. Unlike Tdaf.EReal.iInf_add_iInf_of_ne_bot, the ⊥ cases are handled
rather than excluded: when one infimum is ⊥ the other being below ⊤ forces both sides to ⊥.
Some hypothesis is necessary — for ψ i = -i on ℕ and φ ≡ ⊤ the sides are ⊤ and ⊥.
A real summand slides out of the subtrahend. p - (u + q) = (p - q) - u for real p, q
and arbitrary u : EReal. Both are finite, so no ∞ - ∞ collision arises: at u = ⊤ both sides
are ⊥ and at u = ⊥ both sides are ⊤.
The same difference, folded the other way: p - (u + q) = (p - u) + (-q). The unprimed
form collects both reals on the left; this one keeps p - u intact. Interderivable, but a rw
matches one and not the other.
The difference quotient of a sum splits. For c > 0, reals p, q and u, v never
⊥, c * (u - p) + c * (v - q) = c * ((u + v) - (p + q)). This is the EReal arithmetic behind
the recession-function half of Rockafellar's Theorem 9.3: the difference quotients defining f0⁺
and g0⁺ add up to the one defining (f + g)0⁺.
Two slack inequalities cannot compensate each other. If u and v are bounded below by
reals p and q, and their sum is bounded above by p + q, then each is pinned to its own bound.
Stated one-sided; apply it again with add_comm for the other summand. Rockafellar's Theorem 23.8
is where it is needed: the exact-sum hypothesis delivers one joint equality in Fenchel's
inequality, and this splits it into y₁ ∈ ∂f x and y₂ ∈ ∂g x.
The m-ary form of Tdaf.EReal.le_coe_of_add_le_coe_add. If each u i is bounded below
by the real c i and the sum of the u i is bounded above by the sum of the c i, then every one
of the m inequalities is tight. The two-summand version does not iterate — there is no
subtraction on EReal to peel a summand off with — so the proof splits s as {j} ∪ s.erase j
and applies it once, with the two partial sums as the second pair.