Transport costs on compact spaces

This file records finiteness of the transport cost for a continuous real-valued cost on a compact product. Compactness bounds the cost by a finite constant, so any feasible pair of finite marginals has finite primal value.

theorem TauCeti.transportCost_ne_top_of_continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [CompactSpace X] [MeasurableSpace X] [TopologicalSpace Y] [CompactSpace Y] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {c : X × Y → ℝ} [MeasureTheory.IsFiniteMeasure μ] (hπ : ∃ (π : MeasureTheory.Measure (X × Y)), IsCoupling π μ ν) (hc : Continuous c) : transportCost (fun (z : X × Y) => ENNReal.ofReal (c z)) μ ν ≠ ⊤

A continuous cost on a product of compact spaces is bounded, so any feasible transport problem with a finite first marginal has finite value.