The infimal c-transform in the compact lower semicontinuous regime

TauCeti.cTransform c φ y = ⨅ x, (c (x, y) - φ x) is an infimum over the source, so its regularity in y splits into two halves needing opposite hypotheses. An infimum of upper semicontinuous functions is upper semicontinuous with no hypothesis on the source at all, which is TauCeti.upperSemicontinuous_cTransform. The reverse half fails in general and needs the source to be compact: this file proves that on a compact source a lower semicontinuous integrand makes the transform lower semicontinuous, that the defining infimum is then attained, and hence that a continuous cost and a continuous real-valued potential give a continuous transform. With a lower semicontinuous cost section and an upper semicontinuous real-valued potential, attainment in turn makes the transform real-valued and the c-superdifferential meet every vertical fibre. Borel measurability of the transform is recorded as a corollary. The measurability corollaries of the opposite, upper semicontinuous regime need no compactness and live with that regime in TauCeti.MeasureTheory.OptimalTransport.CTransform.Basic.

The integrand of the transform is x ↦ (c (x, y) : EReal) - φ x, and the hypotheses below are stated on it rather than on c and φ separately, since the extended-real subtraction is what a lower bound has to survive. The _coe results specialize to a real-valued potential, where a lower semicontinuous cost and an upper semicontinuous potential do supply that hypothesis; the pointwise ones ask for lower semicontinuity of only the one section of the cost that their infimum ranges over.

No metrizability, separability or countability of the source is assumed: attainment and lower semicontinuity of a partial infimum need compactness alone, as TauCeti.exists_iInf_eq_of_lowerSemicontinuous and TauCeti.lowerSemicontinuous_iInf_of_compactSpace record.

Main results

• TauCeti.exists_cTransform_eq: on a nonempty compact source the infimum defining the transform is attained, and TauCeti.exists_cTransformSymm_eq on a nonempty compact target.
• TauCeti.lowerSemicontinuous_cTransform: on a compact source a jointly lower semicontinuous integrand makes the transform lower semicontinuous.
• TauCeti.exists_cTransform_coe_eq_coe, TauCeti.exists_cTransformSymm_coe_eq_coe, TauCeti.cTransform_coe_ne_bot, and TauCeti.cTransformSymm_coe_ne_bot: on a nonempty compact factor, a lower semicontinuous cost section and an upper semicontinuous real-valued potential make the transform real-valued.
• TauCeti.exists_mem_cSuperdifferential_coe and TauCeti.exists_mem_cSuperdifferentialSymm_coe: on a nonempty compact factor, a lower semicontinuous cost section and an upper semicontinuous real-valued potential supply a contact point in the corresponding fibre.
• TauCeti.continuous_cTransform_coe: on a compact source a continuous cost and a continuous real-valued potential make the transform continuous.
• TauCeti.measurable_cTransform_of_lowerSemicontinuous and TauCeti.measurable_cTransformSymm_of_lowerSemicontinuous: Borel measurability of the transform in the compact lower semicontinuous regime.

References

The regularity of the infimal transform under these hypotheses is Villani, Optimal Transport, Old and New, Chapter 5, and Santambrogio, Optimal Transport for Applied Mathematicians, §1.6.

Attainment of the defining infimum

theorem TauCeti.exists_cTransform_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {c : X × Y → ℝ} {φ : X → EReal} {y : Y} [CompactSpace X] [Nonempty X] (h : LowerSemicontinuous fun (x : X) => ↑(c (x, y)) - φ x) : ∃ (x : X), cTransform c φ y = ↑(c (x, y)) - φ x

On a nonempty compact source with a lower semicontinuous integrand, the infimum defining the c-transform is attained.

theorem TauCeti.exists_cTransformSymm_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace Y] {c : X × Y → ℝ} {ψ : Y → EReal} {x : X} [CompactSpace Y] [Nonempty Y] (h : LowerSemicontinuous fun (y : Y) => ↑(c (x, y)) - ψ y) : ∃ (y : Y), cTransformSymm c ψ x = ↑(c (x, y)) - ψ y

On a nonempty compact target with a lower semicontinuous integrand, the infimum defining the symmetric c-transform is attained.

Lower semicontinuity over a compact factor

theorem TauCeti.lowerSemicontinuous_cTransform {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {c : X × Y → ℝ} {φ : X → EReal} [CompactSpace X] (h : LowerSemicontinuous fun (p : X × Y) => ↑(c p) - φ p.1) : LowerSemicontinuous (cTransform c φ)

A c-transform over a compact source is lower semicontinuous when the integrand of its defining infimum is jointly lower semicontinuous.

Compactness of the source cannot be dropped: an arbitrary infimum of lower semicontinuous functions need not be lower semicontinuous.

theorem TauCeti.lowerSemicontinuous_cTransformSymm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {c : X × Y → ℝ} {ψ : Y → EReal} [CompactSpace Y] (h : LowerSemicontinuous fun (p : X × Y) => ↑(c p) - ψ p.2) : LowerSemicontinuous (cTransformSymm c ψ)

A symmetric c-transform over a compact target is lower semicontinuous when the integrand of its defining infimum is jointly lower semicontinuous.

Real-valued potentials

theorem TauCeti.lowerSemicontinuous_cTransform_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {c : X × Y → ℝ} {f : X → ℝ} [CompactSpace X] (hc : LowerSemicontinuous c) (hf : UpperSemicontinuous f) : LowerSemicontinuous (cTransform c fun (x : X) => ↑(f x))

A lower semicontinuous cost and an upper semicontinuous real-valued potential give a lower semicontinuous c-transform over a compact source.

theorem TauCeti.lowerSemicontinuous_cTransformSymm_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {c : X × Y → ℝ} {g : Y → ℝ} [CompactSpace Y] (hc : LowerSemicontinuous c) (hg : UpperSemicontinuous g) : LowerSemicontinuous (cTransformSymm c fun (y : Y) => ↑(g y))

A lower semicontinuous cost and an upper semicontinuous real-valued potential give a lower semicontinuous symmetric c-transform over a compact target.

theorem TauCeti.exists_cTransform_coe_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {c : X × Y → ℝ} {f : X → ℝ} {y : Y} [CompactSpace X] [Nonempty X] (hc : LowerSemicontinuous fun (x : X) => c (x, y)) (hf : UpperSemicontinuous f) : ∃ (x : X), cTransform c (fun (x : X) => ↑(f x)) y = ↑(c (x, y)) - ↑(f x)

On a nonempty compact source, a cost whose section at y is lower semicontinuous and an upper semicontinuous real-valued potential make the infimum defining the c-transform attained. Only that one section of the cost is used, so no topology on the target is needed.

theorem TauCeti.exists_cTransformSymm_coe_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace Y] {c : X × Y → ℝ} {g : Y → ℝ} {x : X} [CompactSpace Y] [Nonempty Y] (hc : LowerSemicontinuous fun (y : Y) => c (x, y)) (hg : UpperSemicontinuous g) : ∃ (y : Y), cTransformSymm c (fun (y : Y) => ↑(g y)) x = ↑(c (x, y)) - ↑(g y)

On a nonempty compact target, a cost whose section at x is lower semicontinuous and an upper semicontinuous real-valued potential make the infimum defining the symmetric c-transform attained.

Finiteness and contact points

theorem TauCeti.exists_cTransform_coe_eq_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {c : X × Y → ℝ} {f : X → ℝ} {y : Y} [CompactSpace X] [Nonempty X] (hc : LowerSemicontinuous fun (x : X) => c (x, y)) (hf : UpperSemicontinuous f) : ∃ (b : ℝ), cTransform c (fun (x : X) => ↑(f x)) y = ↑b

On a nonempty compact source, a lower semicontinuous cost section and an upper semicontinuous real-valued potential make the c-transform real-valued: the infimum is attained, and its value at a minimiser is a difference of reals. The general bridge TauCeti.cTransform_coe instead assumes that the corresponding real infimum is bounded below; compactness and semicontinuity here supply both that bound and attainment.

theorem TauCeti.exists_cTransformSymm_coe_eq_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace Y] {c : X × Y → ℝ} {g : Y → ℝ} {x : X} [CompactSpace Y] [Nonempty Y] (hc : LowerSemicontinuous fun (y : Y) => c (x, y)) (hg : UpperSemicontinuous g) : ∃ (b : ℝ), cTransformSymm c (fun (y : Y) => ↑(g y)) x = ↑b

On a nonempty compact target, a lower semicontinuous cost section and an upper semicontinuous real-valued potential make the symmetric c-transform real-valued.

theorem TauCeti.cTransform_coe_ne_bot {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {c : X × Y → ℝ} {f : X → ℝ} {y : Y} [CompactSpace X] [Nonempty X] (hc : LowerSemicontinuous fun (x : X) => c (x, y)) (hf : UpperSemicontinuous f) : cTransform c (fun (x : X) => ↑(f x)) y ≠ ⊥

On a nonempty compact source, a lower semicontinuous cost section and an upper semicontinuous real-valued potential make the c-transform avoid -∞. The opposite bound needs no compactness and is TauCeti.cTransform_lt_top_of_ne_bot.

theorem TauCeti.cTransformSymm_coe_ne_bot {X : Type u_1} {Y : Type u_2} [TopologicalSpace Y] {c : X × Y → ℝ} {g : Y → ℝ} {x : X} [CompactSpace Y] [Nonempty Y] (hc : LowerSemicontinuous fun (y : Y) => c (x, y)) (hg : UpperSemicontinuous g) : cTransformSymm c (fun (y : Y) => ↑(g y)) x ≠ ⊥

On a nonempty compact target, a lower semicontinuous cost section and an upper semicontinuous real-valued potential make the symmetric c-transform avoid -∞.

theorem TauCeti.exists_mem_cSuperdifferential_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {c : X × Y → ℝ} {f : X → ℝ} {y : Y} [CompactSpace X] [Nonempty X] (hc : LowerSemicontinuous fun (x : X) => c (x, y)) (hf : UpperSemicontinuous f) : ∃ (x : X), (x, y) ∈ cSuperdifferential c fun (x : X) => ↑(f x)

On a nonempty compact source, a lower semicontinuous cost section and an upper semicontinuous real-valued potential make the c-superdifferential meet the vertical fibre over y. This is the complementary-slackness input that a dual optimizer supplies, and it is what fails without compactness, the infimum then being only approached.

theorem TauCeti.exists_mem_cSuperdifferentialSymm_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace Y] {c : X × Y → ℝ} {g : Y → ℝ} {x : X} [CompactSpace Y] [Nonempty Y] (hc : LowerSemicontinuous fun (y : Y) => c (x, y)) (hg : UpperSemicontinuous g) : ∃ (y : Y), (y, x) ∈ cSuperdifferential (fun (p : Y × X) => c (p.2, p.1)) fun (y : Y) => ↑(g y)

On a nonempty compact target, a lower semicontinuous cost section and an upper semicontinuous real-valued potential supply a contact point for the swapped cost in the fibre over x.

Continuity and measurability

theorem TauCeti.continuous_cTransform_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {c : X × Y → ℝ} {f : X → ℝ} [CompactSpace X] (hc : Continuous c) (hf : Continuous f) : Continuous (cTransform c fun (x : X) => ↑(f x))

On a compact source, a continuous cost and a continuous real-valued potential give a continuous c-transform: the compact-source argument supplies lower semicontinuity, and TauCeti.upperSemicontinuous_cTransform_of_continuous supplies upper semicontinuity.

theorem TauCeti.continuous_cTransformSymm_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {c : X × Y → ℝ} {g : Y → ℝ} [CompactSpace Y] (hc : Continuous c) (hg : Continuous g) : Continuous (cTransformSymm c fun (y : Y) => ↑(g y))

On a compact target, a continuous cost and a continuous real-valued potential give a continuous symmetric c-transform.

theorem TauCeti.measurable_cTransform_of_lowerSemicontinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {c : X × Y → ℝ} {φ : X → EReal} [CompactSpace X] [MeasurableSpace Y] [OpensMeasurableSpace Y] (h : LowerSemicontinuous fun (p : X × Y) => ↑(c p) - φ p.1) : Measurable (cTransform c φ)

A c-transform over a compact source is Borel measurable when the integrand of its defining infimum is jointly lower semicontinuous.

theorem TauCeti.measurable_cTransformSymm_of_lowerSemicontinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {c : X × Y → ℝ} {ψ : Y → EReal} [CompactSpace Y] [MeasurableSpace X] [OpensMeasurableSpace X] (h : LowerSemicontinuous fun (p : X × Y) => ↑(c p) - ψ p.2) : Measurable (cTransformSymm c ψ)

A symmetric c-transform over a compact target is Borel measurable when the integrand of its defining infimum is jointly lower semicontinuous.