Prove2Me

Theorem 4.25 — (ψc)c=ψ(\psi^c)^c=\psi for cc-concave ψ\psi

Proved
MongeKantorovichYao.cConjugate_cConjugate_of_isCConcave

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

c-concavityoptimal-transport

Let X,YX,Y be sets and c:X×Y→Rc : X\times Y\to\mathbb R. If ψ:X→R\psi : X\to\mathbb R is cc-concave, then its double cc-conjugate is ψ\psi itself:

(ψc)c(x)=inf⁡y∈Y(c(x,y)−inf⁡x′∈X(c(x′,y)−ψ(x′)))=ψ(x)for all x∈X.(\psi^c)^c(x)=\inf_{y\in Y}\Big(c(x,y)-\inf_{x'\in X}\big(c(x',y)-\psi(x')\big)\Big)=\psi(x)\qquad\text{for all }x\in X.

This is used to show that the dual potentials ψ\psi and φ=ψc\varphi=\psi^c determine each other, which gives their boundedness in the proof of Proposition 4.31.

Formalization Note Both conjugates are computed in the extended reals.

Preamble
import Mathlib
import Definitions.Def_MongeKantorovichYao_Defs

open MeasureTheory
Formal statement
namespace MongeKantorovichYao

theorem cConjugate_cConjugate_of_isCConcave {X Y : Type*}
    (c : X × Y → ℝ) (ψ : X → ℝ) (hψ : IsCConcave c ψ) :
    cConjugate' c (cConjugate c (fun x => (ψ x : EReal))) = fun x => (ψ x : EReal) := by sorry

end MongeKantorovichYao
Source
Colin Yao, *Monge–Kantorovich and Transportation Theory* (paper dated September 10, 2023), p. 15, Theorem 4.25 (proof referred to Appendix A.4, p. 26)
Read-back

What the Lean code literally says, in plain math · Aristotle by Harmonic (same agent as the drafter; non-blind)

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source paper and of the intended meaning. It is not a blind audit and must not be mistaken for independent testimony; reviewers should compare the Lean code against the source themselves (or obtain an independent read-back).

Data and hypotheses. Arbitrary types X,YX,Y (no structure), a function c:X×Y→Rc : X\times Y\to\mathbb R, and ψ:X→R\psi : X\to\mathbb R which is cc-concave: there is a real-valued φ\varphi on YY with ψ(x)=inf⁡y(c(x,y)−φ(y))\psi(x)=\inf_{y}(c(x,y)-\varphi(y)) for every xx (infimum in the extended reals).

Conclusion. Define, in [−∞,∞][-\infty,\infty], ψc(y)=inf⁡x′∈X(c(x′,y)−ψ(x′))\psi^c(y)=\inf_{x'\in X}(c(x',y)-\psi(x')) and then (ψc)c(x)=inf⁡y∈Y(c(x,y)−ψc(y))(\psi^c)^c(x)=\inf_{y\in Y}(c(x,y)-\psi^c(y)) (with a−(+∞)=−∞a-(+\infty)=-\infty, a−(−∞)=+∞a-(-\infty)=+\infty). Then (ψc)c(x)=ψ(x)(\psi^c)^c(x)=\psi(x) for every x∈Xx\in X, as an equality of functions X→[−∞,∞]X\to[-\infty,\infty].

Edge cases. If XX is empty the statement is trivial; if YY is empty and XX nonempty the hypothesis cannot hold (the infimum over an empty set is +∞≠ψ(x)+\infty\ne\psi(x)).

Human review

  • Endorsed by Shuze Chen · Sep 30, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Sep 30, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph