The infimal c-transform, c-concavity, and contact sets

The Kantorovich dual constraint on a pair of potentials φ : X → EReal and ψ : Y → EReal against a cost c : X × Y → ℝ is the pointwise inequality φ x + ψ y ≤ c (x, y). With φ fixed, the largest ψ satisfying it is the infimal c-transform cTransform c φ y = ⨅ x, (c (x, y) - φ x), and symmetrically with ψ fixed. This file builds that transform, the two closure operations it generates, the c-concave potentials they fix, and the contact set on which the dual constraint is an equality. It is the finite-real slice of the roadmap's broader transform interface; the analytic-sublevel interface lives in TauCeti.MeasureTheory.OptimalTransport.CTransform.Analytic, and the compact attainment and lower-semicontinuity interface in TauCeti.MeasureTheory.OptimalTransport.CTransform.Compact. The extended-cost interface is a follow-up slice. The elementary upper-semicontinuity result for infimal transforms, the Borel measurability it gives with no hypothesis on the opposite factor, and a metric continuity result for real-valued transforms are included here.

Even for a finite real cost and a finite real potential the infimum defining the transform can be -∞, so the transform must have an extended-real codomain; and once the codomain is extended, iterating the transform forces extended-real potentials. The cost is therefore taken finite here, and that is exactly what makes the subtraction safe: (c (x, y) : EReal) - φ x subtracts an arbitrary extended real from a real one, so it is never of the form ∞ - ∞, and no statement below hides such a term. Concretely, Mathlib's EReal.le_sub_iff_add_le applies with no side condition, which gives the adjunction ψ ≤ cTransform c φ ↔ φ ≤ cTransformSymm c ψ recorded as TauCeti.cTransform_galoisConnection. For an extended-valued cost the same formula is not the right one: with c ≡ ⊤ and φ ≡ 0, EReal subtraction gives ⊤ - ⊤ = ⊥, so the double transform of φ is ⊥ on nonempty factors and the inequality φ ≤ φᶜᶜ fails. The extended-cost interface needs its own conventions and is not built here.

Apart from the upper-semicontinuity and Borel measurability results, and the metric continuity result on pseudometric spaces, the two factors are bare types and the results are order-theoretic identities about the transform. They are the algebraic and topological halves of the Kantorovich dual problem, to be combined with the integrability conditions that make the two marginal integrals of a dual pair meaningful.

Main definitions

• TauCeti.cTransform c φ — the infimal c-transform y ↦ ⨅ x, (c (x, y) - φ x) of a potential on the source, and TauCeti.cTransformSymm c ψ, the symmetric transform x ↦ ⨅ y, (c (x, y) - ψ y) of a potential on the target;
• TauCeti.IsCConcave c φ and TauCeti.IsCConcaveSymm c ψ — the potentials that arise as a transform, equivalently those fixed by the corresponding double transform;
• TauCeti.contactSet c φ ψ — the set where the dual constraint holds with equality, and TauCeti.cSuperdifferential c φ, its instance at the canonical partner cTransform c φ.

Main statements

• TauCeti.add_cTransform_le — the transform is dual feasible against its own source potential, and TauCeti.le_cTransform_iff — it is the largest such partner; together these give TauCeti.cTransform_galoisConnection, the antitone Galois connection between the potentials on the two factors, and with it the order reversal TauCeti.cTransform_antitone;
• TauCeti.le_cTransformSymm_cTransform — a potential is dominated by its double transform, so transforming a dual feasible pair improves it, and TauCeti.cTransform_cTransformSymm_cTransform — a transform is unchanged by a further double transform;
• TauCeti.isCConcave_iff — c-concavity is exactly being fixed by the double transform;
• TauCeti.upperSemicontinuous_cTransform — an infimal transform of upper-semicontinuous sections is upper semicontinuous, and TauCeti.measurable_cTransform_of_upperSemicontinuous — it is then Borel measurable, while TauCeti.uniformContinuous_iInf_sub shows that a real-valued infimal transform is uniformly continuous when the target-variable sections of the cost share a uniform modulus and its infima are finite;
• TauCeti.cTransform_add_const — the transform turns an additive real constant into its negative, which is the normalisation freedom of the dual problem;
• TauCeti.cTransform_coe and TauCeti.cTransformSymm_coe — the extended-real transforms of coerced real potentials agree with the corresponding real infima whenever those infima are bounded below;
• TauCeti.contactSet_subset_contactSet_cTransformSymm_cTransform — sequentially transforming a feasible pair gives a dominating feasible pair with a larger contact set, and TauCeti.cTransformSymm_cTransform_eq_of_mem_cSuperdifferential — a potential agrees with its double transform at every point of its c-superdifferential.

This is the finite-real algebraic slice of Layer 2, item 2 of the optimal-transport roadmap.

References

• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, §2.4, where the c-transform, c-concavity and the c-superdifferential are introduced for a real cost;
• C. Villani, Optimal Transport: Old and New, Grundlehren 338, 2009, Chapter 5, in particular the discussion of c-convexity preceding Theorem 5.10;
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Progress in Nonlinear Differential Equations and their Applications 87, 2015, §1.6.

noncomputable def TauCeti.cTransform {X : Type u} {Y : Type v} (c : X × Y → ℝ) (φ : X → EReal) (y : Y) : EReal

The infimal c-transform of a potential φ on the source: the largest potential on the target that is dual feasible against φ for the cost c, namely cTransform c φ y = ⨅ x, (c (x, y) - φ x). The cost is real and the potential is extended real, so the subtraction is always defined; the infimum can be -∞, and it is ⊤ when X is empty.

Equations

• TauCeti.cTransform c φ y = ⨅ (x : X), ↑(c (x, y)) - φ x

noncomputable def TauCeti.cTransformSymm {X : Type u} {Y : Type v} (c : X × Y → ℝ) (ψ : Y → EReal) (x : X) : EReal

The infimal c-transform of a potential ψ on the target: the largest potential on the source that is dual feasible against ψ for the cost c, namely cTransformSymm c ψ x = ⨅ y, (c (x, y) - ψ y). It is TauCeti.cTransform for the transposed cost, and is provided so that no user has to transpose a product by hand.

Equations

• TauCeti.cTransformSymm c ψ x = ⨅ (y : Y), ↑(c (x, y)) - ψ y

theorem TauCeti.cTransform_apply {X : Type u} {Y : Type v} (c : X × Y → ℝ) (φ : X → EReal) (y : Y) : cTransform c φ y = ⨅ (x : X), ↑(c (x, y)) - φ x

The defining formula for the c-transform.

theorem TauCeti.cTransformSymm_apply {X : Type u} {Y : Type v} (c : X × Y → ℝ) (ψ : Y → EReal) (x : X) : cTransformSymm c ψ x = ⨅ (y : Y), ↑(c (x, y)) - ψ y

The defining formula for the symmetric c-transform.

theorem TauCeti.cTransformSymm_eq_cTransform {X : Type u} {Y : Type v} (c : X × Y → ℝ) (ψ : Y → EReal) : cTransformSymm c ψ = cTransform (fun (p : Y × X) => c (p.2, p.1)) ψ

The symmetric transform is the transform of the transposed cost.

theorem TauCeti.cTransform_le {X : Type u} {Y : Type v} (c : X × Y → ℝ) (φ : X → EReal) (x : X) (y : Y) : cTransform c φ y ≤ ↑(c (x, y)) - φ x

Each source point bounds the c-transform at each target point.

theorem TauCeti.cTransformSymm_le {X : Type u} {Y : Type v} (c : X × Y → ℝ) (ψ : Y → EReal) (x : X) (y : Y) : cTransformSymm c ψ x ≤ ↑(c (x, y)) - ψ y

Each target point bounds the symmetric c-transform at each source point.

theorem TauCeti.le_cTransform {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {a : EReal} {y : Y} (h : ∀ (x : X), a ≤ ↑(c (x, y)) - φ x) : a ≤ cTransform c φ y

A lower bound valid at every source point is a lower bound for the c-transform.

theorem TauCeti.le_cTransformSymm {X : Type u} {Y : Type v} {c : X × Y → ℝ} {ψ : Y → EReal} {a : EReal} {x : X} (h : ∀ (y : Y), a ≤ ↑(c (x, y)) - ψ y) : a ≤ cTransformSymm c ψ x

A lower bound valid at every target point is a lower bound for the symmetric c-transform.

theorem TauCeti.add_cTransform_le {X : Type u} {Y : Type v} (c : X × Y → ℝ) (φ : X → EReal) (x : X) (y : Y) : φ x + cTransform c φ y ≤ ↑(c (x, y))

The c-transform of φ is dual feasible against φ.

theorem TauCeti.cTransformSymm_add_le {X : Type u} {Y : Type v} (c : X × Y → ℝ) (ψ : Y → EReal) (x : X) (y : Y) : cTransformSymm c ψ x + ψ y ≤ ↑(c (x, y))

The symmetric c-transform of ψ is dual feasible against ψ.

theorem TauCeti.le_cTransform_iff {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {ψ : Y → EReal} : ψ ≤ cTransform c φ ↔ ∀ (x : X) (y : Y), φ x + ψ y ≤ ↑(c (x, y))

The c-transform of φ is the largest potential on the target that is dual feasible against φ.

theorem TauCeti.le_cTransformSymm_iff {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {ψ : Y → EReal} : φ ≤ cTransformSymm c ψ ↔ ∀ (x : X) (y : Y), φ x + ψ y ≤ ↑(c (x, y))

The symmetric c-transform of ψ is the largest potential on the source that is dual feasible against ψ.

theorem TauCeti.cTransform_galoisConnection {X : Type u} {Y : Type v} (c : X × Y → ℝ) : GaloisConnection (fun (φ : X → EReal) => OrderDual.toDual (cTransform c φ)) fun (ψ : (Y → EReal)ᵒᵈ) => cTransformSymm c (OrderDual.ofDual ψ)

The two c-transforms form an antitone Galois connection between the potentials on the two factors: ψ ≤ cTransform c φ and φ ≤ cTransformSymm c ψ each say that the pair (φ, ψ) is dual feasible. Order reversal, the double-transform inequalities and the triple-transform identities below are its standard consequences.

theorem TauCeti.cTransform_antitone {X : Type u} {Y : Type v} (c : X × Y → ℝ) : Antitone (cTransform c)

The c-transform reverses the order of potentials.

theorem TauCeti.cTransformSymm_antitone {X : Type u} {Y : Type v} (c : X × Y → ℝ) : Antitone (cTransformSymm c)

The symmetric c-transform reverses the order of potentials.

theorem TauCeti.le_cTransformSymm_cTransform {X : Type u} {Y : Type v} (c : X × Y → ℝ) (φ : X → EReal) : φ ≤ cTransformSymm c (cTransform c φ)

A potential is dominated by its double c-transform. Transforming a dual feasible pair twice therefore improves it.

theorem TauCeti.le_cTransform_cTransformSymm {X : Type u} {Y : Type v} (c : X × Y → ℝ) (ψ : Y → EReal) : ψ ≤ cTransform c (cTransformSymm c ψ)

A potential on the target is dominated by its double c-transform.

@[simp]

theorem TauCeti.cTransform_cTransformSymm_cTransform {X : Type u} {Y : Type v} (c : X × Y → ℝ) (φ : X → EReal) : cTransform c (cTransformSymm c (cTransform c φ)) = cTransform c φ

A c-transform is unchanged by a further double transform: three transforms are one.

@[simp]

theorem TauCeti.cTransformSymm_cTransform_cTransformSymm {X : Type u} {Y : Type v} (c : X × Y → ℝ) (ψ : Y → EReal) : cTransformSymm c (cTransform c (cTransformSymm c ψ)) = cTransformSymm c ψ

A symmetric c-transform is unchanged by a further double transform.

theorem TauCeti.cTransform_mono_cost {X : Type u} {Y : Type v} {c c' : X × Y → ℝ} (h : c ≤ c') (φ : X → EReal) : cTransform c φ ≤ cTransform c' φ

The c-transform is monotone in the cost.

theorem TauCeti.cTransformSymm_mono_cost {X : Type u} {Y : Type v} {c c' : X × Y → ℝ} (h : c ≤ c') (ψ : Y → EReal) : cTransformSymm c ψ ≤ cTransformSymm c' ψ

The symmetric c-transform is monotone in the cost.

theorem TauCeti.cTransform_lt_top_of_ne_bot {X : Type u} {Y : Type v} {φ : X → EReal} {x : X} (c : X × Y → ℝ) (hx : φ x ≠ ⊥) (y : Y) : cTransform c φ y < ⊤

If the potential avoids -∞ at one source point, its c-transform avoids ⊤. In particular a real potential on a nonempty source has a transform valued in [-∞, ∞).

@[simp]

theorem TauCeti.cTransform_of_isEmpty {X : Type u} {Y : Type v} [IsEmpty X] (c : X × Y → ℝ) (φ : X → EReal) (y : Y) : cTransform c φ y = ⊤

The c-transform of a potential on an empty source is ⊤.

theorem TauCeti.cTransformSymm_lt_top_of_ne_bot {X : Type u} {Y : Type v} {ψ : Y → EReal} {y : Y} (c : X × Y → ℝ) (hy : ψ y ≠ ⊥) (x : X) : cTransformSymm c ψ x < ⊤

If the potential avoids -∞ at one target point, its symmetric c-transform avoids ⊤.

@[simp]

theorem TauCeti.cTransformSymm_of_isEmpty {X : Type u} {Y : Type v} [IsEmpty Y] (c : X × Y → ℝ) (ψ : Y → EReal) (x : X) : cTransformSymm c ψ x = ⊤

The symmetric c-transform of a potential on an empty target is ⊤.

theorem TauCeti.cTransform_coe {X : Type u} {Y : Type v} [Nonempty X] (c : X × Y → ℝ) (φ : X → ℝ) (y : Y) (hbdd : BddBelow (Set.range fun (x : X) => c (x, y) - φ x)) : cTransform c (fun (x : X) => ↑(φ x)) y = ↑(⨅ (x : X), c (x, y) - φ x)

The EReal-valued infimal transform TauCeti.cTransform of a real potential is a real-valued infimum whenever that infimum is bounded below.

theorem TauCeti.cTransformSymm_coe {X : Type u} {Y : Type v} [Nonempty Y] (c : X × Y → ℝ) (ψ : Y → ℝ) (x : X) (hbdd : BddBelow (Set.range fun (y : Y) => c (x, y) - ψ y)) : cTransformSymm c (fun (y : Y) => ↑(ψ y)) x = ↑(⨅ (y : Y), c (x, y) - ψ y)

The EReal-valued symmetric infimal transform TauCeti.cTransformSymm of a real potential is a real-valued infimum whenever that infimum is bounded below.

theorem TauCeti.uniformContinuous_iInf_sub {X : Type u} {Y : Type v} [PseudoMetricSpace Y] [Nonempty X] {c : X × Y → ℝ} {φ : X → ℝ} (hc : ∀ ε > 0, ∃ δ > 0, ∀ (x : X) (y y' : Y), dist y y' < δ → dist (c (x, y)) (c (x, y')) < ε) (hbdd : ∀ (y : Y), BddBelow (Set.range fun (x : X) => c (x, y) - φ x)) : UniformContinuous fun (y : Y) => ⨅ (x : X), c (x, y) - φ x

The infimal c-transform of a real potential inherits a uniform modulus of continuity from the target-variable sections of the cost.

theorem TauCeti.upperSemicontinuous_cTransform {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} [TopologicalSpace Y] (h : ∀ (x : X), UpperSemicontinuous fun (y : Y) => ↑(c (x, y)) - φ x) : UpperSemicontinuous (cTransform c φ)

A c-transform is upper semicontinuous when each function in its defining infimum is upper semicontinuous.

theorem TauCeti.upperSemicontinuous_cTransformSymm {X : Type u} {Y : Type v} {c : X × Y → ℝ} {ψ : Y → EReal} [TopologicalSpace X] (h : ∀ (y : Y), UpperSemicontinuous fun (x : X) => ↑(c (x, y)) - ψ y) : UpperSemicontinuous (cTransformSymm c ψ)

A symmetric c-transform is upper semicontinuous when each function in its defining infimum is upper semicontinuous.

theorem TauCeti.upperSemicontinuous_cTransform_of_upperSemicontinuous {X : Type u} {Y : Type v} {c : X × Y → ℝ} [TopologicalSpace Y] (hc : ∀ (x : X), UpperSemicontinuous fun (y : Y) => c (x, y)) (φ : X → EReal) : UpperSemicontinuous (cTransform c φ)

If every section y ↦ c (x, y) of the cost is upper semicontinuous, the c-transform is upper semicontinuous. No finiteness of the potential is needed.

theorem TauCeti.upperSemicontinuous_cTransform_of_continuous {X : Type u} {Y : Type v} {c : X × Y → ℝ} [TopologicalSpace Y] (hc : ∀ (x : X), Continuous fun (y : Y) => c (x, y)) (φ : X → EReal) : UpperSemicontinuous (cTransform c φ)

If every section y ↦ c (x, y) of the cost is continuous, the c-transform is upper semicontinuous.

theorem TauCeti.upperSemicontinuous_cTransformSymm_of_upperSemicontinuous {X : Type u} {Y : Type v} {c : X × Y → ℝ} [TopologicalSpace X] (hc : ∀ (y : Y), UpperSemicontinuous fun (x : X) => c (x, y)) (ψ : Y → EReal) : UpperSemicontinuous (cTransformSymm c ψ)

If every section x ↦ c (x, y) of the cost is upper semicontinuous, the symmetric c-transform is upper semicontinuous.

theorem TauCeti.upperSemicontinuous_cTransformSymm_of_continuous {X : Type u} {Y : Type v} {c : X × Y → ℝ} [TopologicalSpace X] (hc : ∀ (y : Y), Continuous fun (x : X) => c (x, y)) (ψ : Y → EReal) : UpperSemicontinuous (cTransformSymm c ψ)

If every section x ↦ c (x, y) of the cost is continuous, the symmetric c-transform is upper semicontinuous.

theorem TauCeti.measurable_cTransform_of_upperSemicontinuous {X : Type u} {Y : Type v} {c : X × Y → ℝ} [TopologicalSpace Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] (hc : ∀ (x : X), UpperSemicontinuous fun (y : Y) => c (x, y)) (φ : X → EReal) : Measurable (cTransform c φ)

A c-transform is Borel measurable whenever every section y ↦ c (x, y) of the cost is upper semicontinuous. No hypothesis on the source is needed in this regime.

theorem TauCeti.measurable_cTransformSymm_of_upperSemicontinuous {X : Type u} {Y : Type v} {c : X × Y → ℝ} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] (hc : ∀ (y : Y), UpperSemicontinuous fun (x : X) => c (x, y)) (ψ : Y → EReal) : Measurable (cTransformSymm c ψ)

A symmetric c-transform is Borel measurable whenever every section x ↦ c (x, y) of the cost is upper semicontinuous.

theorem TauCeti.cTransform_add_const {X : Type u} {Y : Type v} (c : X × Y → ℝ) (φ : X → EReal) (a : ℝ) (y : Y) : cTransform c (fun (x : X) => φ x + ↑a) y = cTransform c φ y - ↑a

Shifting a potential by a real constant shifts its c-transform by the opposite constant. This is the normalisation freedom of the Kantorovich dual problem: the pair (φ + a, φᶜ - a) satisfies the same dual constraint as (φ, φᶜ).

theorem TauCeti.cTransformSymm_add_const {X : Type u} {Y : Type v} (c : X × Y → ℝ) (ψ : Y → EReal) (a : ℝ) (x : X) : cTransformSymm c (fun (y : Y) => ψ y + ↑a) x = cTransformSymm c ψ x - ↑a

Shifting a potential on the target by a real constant shifts its symmetric c-transform by the opposite constant.

c-concave potentials

def TauCeti.IsCConcave {X : Type u} {Y : Type v} (c : X × Y → ℝ) (φ : X → EReal) : Prop

A potential on the source is c-concave when it is the symmetric c-transform of some potential on the target. By TauCeti.isCConcave_iff this happens exactly when it is fixed by the double transform.

Equations

• TauCeti.IsCConcave c φ = ∃ (ψ : Y → EReal), φ = TauCeti.cTransformSymm c ψ

def TauCeti.IsCConcaveSymm {X : Type u} {Y : Type v} (c : X × Y → ℝ) (ψ : Y → EReal) : Prop

A potential on the target is c-concave when it is the c-transform of some potential on the source. By TauCeti.isCConcaveSymm_iff this happens exactly when it is fixed by the double transform.

Equations

• TauCeti.IsCConcaveSymm c ψ = ∃ (φ : X → EReal), ψ = TauCeti.cTransform c φ

theorem TauCeti.isCConcave_cTransformSymm {X : Type u} {Y : Type v} (c : X × Y → ℝ) (ψ : Y → EReal) : IsCConcave c (cTransformSymm c ψ)

Every symmetric c-transform is c-concave.

theorem TauCeti.isCConcaveSymm_cTransform {X : Type u} {Y : Type v} (c : X × Y → ℝ) (φ : X → EReal) : IsCConcaveSymm c (cTransform c φ)

Every c-transform is c-concave.

theorem TauCeti.isCConcave_iff {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} : IsCConcave c φ ↔ cTransformSymm c (cTransform c φ) = φ

A potential on the source is c-concave exactly when it is fixed by the double c-transform.

theorem TauCeti.isCConcaveSymm_iff {X : Type u} {Y : Type v} {c : X × Y → ℝ} {ψ : Y → EReal} : IsCConcaveSymm c ψ ↔ cTransform c (cTransformSymm c ψ) = ψ

A potential on the target is c-concave exactly when it is fixed by the double c-transform.

theorem TauCeti.IsCConcave.cTransformSymm_cTransform {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} : IsCConcave c φ → cTransformSymm c (cTransform c φ) = φ

A c-concave potential is fixed by the double c-transform.

theorem TauCeti.IsCConcaveSymm.cTransform_cTransformSymm {X : Type u} {Y : Type v} {c : X × Y → ℝ} {ψ : Y → EReal} : IsCConcaveSymm c ψ → cTransform c (cTransformSymm c ψ) = ψ

A c-concave potential on the target is fixed by the double c-transform.

Contact sets and c-superdifferentials

def TauCeti.contactSet {X : Type u} {Y : Type v} (c : X × Y → ℝ) (φ : X → EReal) (ψ : Y → EReal) : Set (X × Y)

The contact set of a pair of potentials: the set where the dual constraint φ x + ψ y ≤ c (x, y) holds with equality. For a dual feasible pair this is the set that a complementary slackness condition refers to.

Equations

• TauCeti.contactSet c φ ψ = {z : X × Y | φ z.1 + ψ z.2 = ↑(c z)}

def TauCeti.cSuperdifferential {X : Type u} {Y : Type v} (c : X × Y → ℝ) (φ : X → EReal) : Set (X × Y)

The c-superdifferential of a potential: its contact set against its own c-transform.

Equations

• TauCeti.cSuperdifferential c φ = TauCeti.contactSet c φ (TauCeti.cTransform c φ)

@[simp]

theorem TauCeti.mem_contactSet_iff {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {ψ : Y → EReal} {z : X × Y} : z ∈ contactSet c φ ψ ↔ φ z.1 + ψ z.2 = ↑(c z)

Membership in the contact set, for a point of the product.

theorem TauCeti.mk_mem_contactSet_iff {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {ψ : Y → EReal} {x : X} {y : Y} : (x, y) ∈ contactSet c φ ψ ↔ φ x + ψ y = ↑(c (x, y))

Membership in the contact set, for an explicit pair.

theorem TauCeti.mk_mem_contactSet_coe_iff {X : Type u} {Y : Type v} (c : X × Y → ℝ) (φ : X → ℝ) (ψ : Y → ℝ) (x : X) (y : Y) : ((x, y) ∈ contactSet c (fun (x : X) => ↑(φ x)) fun (y : Y) => ↑(ψ y)) ↔ φ x + ψ y = c (x, y)

Membership in the contact set of two real-valued potentials, with all coercions to EReal eliminated.

theorem TauCeti.cSuperdifferential_def {X : Type u} {Y : Type v} (c : X × Y → ℝ) (φ : X → EReal) : cSuperdifferential c φ = contactSet c φ (cTransform c φ)

The c-superdifferential is the contact set against the c-transform.

@[simp]

theorem TauCeti.mem_cSuperdifferential_iff {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {z : X × Y} : z ∈ cSuperdifferential c φ ↔ φ z.1 + cTransform c φ z.2 = ↑(c z)

Membership in the c-superdifferential, for a point of the product.

theorem TauCeti.mk_mem_cSuperdifferential_iff {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {x : X} {y : Y} : (x, y) ∈ cSuperdifferential c φ ↔ φ x + cTransform c φ y = ↑(c (x, y))

Membership in the c-superdifferential, for an explicit pair.

theorem TauCeti.mk_mem_contactSet_swap_iff {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {ψ : Y → EReal} {x : X} {y : Y} : (y, x) ∈ contactSet (fun (p : Y × X) => c (p.2, p.1)) ψ φ ↔ (x, y) ∈ contactSet c φ ψ

The contact set is invariant under swapping the cost factors and the potentials.

theorem TauCeti.exists_coe_of_mem_contactSet {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {ψ : Y → EReal} {x : X} {y : Y} (hz : (x, y) ∈ contactSet c φ ψ) : ∃ (b : ℝ) (b' : ℝ), φ x = ↑b ∧ ψ y = ↑b' ∧ b + b' = c (x, y)

Both potentials are finite at a contact point: the dual constraint cannot hold with equality at an infinite value, because the cost is real.

theorem TauCeti.ne_bot_left_of_mem_contactSet {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {ψ : Y → EReal} {x : X} {y : Y} (hz : (x, y) ∈ contactSet c φ ψ) : φ x ≠ ⊥

The source potential avoids -∞ at a contact point.

theorem TauCeti.ne_top_left_of_mem_contactSet {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {ψ : Y → EReal} {x : X} {y : Y} (hz : (x, y) ∈ contactSet c φ ψ) : φ x ≠ ⊤

The source potential avoids ⊤ at a contact point.

theorem TauCeti.ne_bot_right_of_mem_contactSet {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {ψ : Y → EReal} {x : X} {y : Y} (hz : (x, y) ∈ contactSet c φ ψ) : ψ y ≠ ⊥

The target potential avoids -∞ at a contact point.

theorem TauCeti.ne_top_right_of_mem_contactSet {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {ψ : Y → EReal} {x : X} {y : Y} (hz : (x, y) ∈ contactSet c φ ψ) : ψ y ≠ ⊤

The target potential avoids ⊤ at a contact point.

theorem TauCeti.cTransform_eq_of_mem_contactSet {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {ψ : Y → EReal} {x : X} {y : Y} (hfeas : ∀ (x' : X), φ x' + ψ y ≤ ↑(c (x', y))) (hz : (x, y) ∈ contactSet c φ ψ) : cTransform c φ y = ψ y

At a contact point, if dual feasibility holds along the corresponding target section, the second potential already agrees with the c-transform of the first: the infimum defining that transform is attained there.

theorem TauCeti.cTransformSymm_eq_of_mem_contactSet {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {ψ : Y → EReal} {x : X} {y : Y} (hfeas : ∀ (y' : Y), φ x + ψ y' ≤ ↑(c (x, y'))) (hz : (x, y) ∈ contactSet c φ ψ) : cTransformSymm c ψ x = φ x

At a contact point, if dual feasibility holds along the corresponding source section, the first potential already agrees with the symmetric c-transform of the second.

theorem TauCeti.contactSet_subset_contactSet_cTransformSymm_cTransform {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {ψ : Y → EReal} (hfeas : ∀ (x : X) (y : Y), φ x + ψ y ≤ ↑(c (x, y))) : contactSet c φ ψ ⊆ contactSet c (cTransformSymm c (cTransform c φ)) (cTransform c φ)

Replacing first the target potential by the transform of the source and then the source by the symmetric transform of that new target only enlarges the contact set.

theorem TauCeti.contactSet_subset_cSuperdifferential {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {ψ : Y → EReal} (hfeas : ∀ (x : X) (y : Y), φ x + ψ y ≤ ↑(c (x, y))) : contactSet c φ ψ ⊆ cSuperdifferential c φ

The contact set of a potential against its own c-transform is the largest one available: every dual feasible pair with the same source potential has a smaller contact set.

theorem TauCeti.cTransform_eq_of_mem_cSuperdifferential {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {x : X} {y : Y} (hz : (x, y) ∈ cSuperdifferential c φ) : cTransform c φ y = ↑(c (x, y)) - φ x

On its c-superdifferential, the infimum defining the c-transform is attained.

theorem TauCeti.mem_cSuperdifferential_of_cTransform_eq {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {x : X} {y : Y} {b : ℝ} (hb : φ x = ↑b) (h : cTransform c φ y = ↑(c (x, y)) - φ x) : (x, y) ∈ cSuperdifferential c φ

A point where the infimum defining the c-transform is attained belongs to the c-superdifferential, provided the source potential is real at that point.

theorem TauCeti.cTransformSymm_cTransform_eq_of_mem_cSuperdifferential {X : Type u} {Y : Type v} {c : X × Y → ℝ} {φ : X → EReal} {x : X} {y : Y} (hz : (x, y) ∈ cSuperdifferential c φ) : cTransformSymm c (cTransform c φ) x = φ x

A potential agrees with its double c-transform at every point of its c-superdifferential, whether or not it is c-concave elsewhere.