Analytic measurability of the infimal c-transform

For Polish source and target spaces, a Borel integrand (x, y) ↦ (c (x, y) : EReal) - φ x need not have a Borel infimum over x. Its strict sublevel sets are nevertheless analytic: each is the projection of the corresponding Borel strict sublevel set of the integrand. Lusin's universal-measurability theorem then makes every such sublevel measurable in the completion of each s-finite Borel measure. This is the precise measurability regime used to integrate general Kantorovich potentials without incorrectly claiming Borel measurability.

The symmetric transform is included with the same hypotheses on the transposed integrand.

Main results

• TauCeti.analyticSet_setOf_cTransform_lt: strict sublevels of the infimal transform are analytic;
• TauCeti.nullMeasurableSet_setOf_cTransform_lt: those sublevels are measurable after completing any s-finite Borel measure;
• TauCeti.nullMeasurable_cTransform: the transform itself is null-measurable for each s-finite Borel measure;
• the corresponding three results with cTransformSymm in their names.

References

• C. Villani, Optimal Transport: Old and New, Springer, 2009, Chapter 5.
• A. S. Kechris, Classical Descriptive Set Theory, Springer-Verlag, 1995, Theorem 29.7.

theorem TauCeti.analyticSet_setOf_cTransform_lt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {c : X × Y → ℝ} {φ : X → EReal} (a : EReal) (h : MeasurableSet {z : X × Y | ↑(c z) - φ z.1 < a}) : MeasureTheory.AnalyticSet {y : Y | cTransform c φ y < a}

If a strict sublevel of the defining integrand of a c-transform is Borel measurable, the corresponding strict sublevel of the transform is analytic. It is the second-coordinate projection of that integrand sublevel.

theorem TauCeti.analyticSet_setOf_cTransformSymm_lt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {c : X × Y → ℝ} {ψ : Y → EReal} (a : EReal) (h : MeasurableSet {z : X × Y | ↑(c z) - ψ z.2 < a}) : MeasureTheory.AnalyticSet {x : X | cTransformSymm c ψ x < a}

If a strict sublevel of the defining integrand of a symmetric c-transform is Borel measurable, the corresponding strict sublevel of the transform is analytic.

theorem TauCeti.nullMeasurableSet_setOf_cTransform_lt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {c : X × Y → ℝ} {φ : X → EReal} (μ : MeasureTheory.Measure Y) [MeasureTheory.SFinite μ] (a : EReal) (h : MeasurableSet {z : X × Y | ↑(c z) - φ z.1 < a}) : MeasureTheory.NullMeasurableSet {y : Y | cTransform c φ y < a} μ

A strict sublevel of a c-transform is measurable after completing any s-finite Borel measure on the target when the corresponding integrand sublevel is Borel measurable.

theorem TauCeti.nullMeasurableSet_setOf_cTransformSymm_lt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {c : X × Y → ℝ} {ψ : Y → EReal} (μ : MeasureTheory.Measure X) [MeasureTheory.SFinite μ] (a : EReal) (h : MeasurableSet {z : X × Y | ↑(c z) - ψ z.2 < a}) : MeasureTheory.NullMeasurableSet {x : X | cTransformSymm c ψ x < a} μ

A strict sublevel of a symmetric c-transform is measurable after completing any s-finite Borel measure on the source when the corresponding integrand sublevel is Borel measurable.

theorem TauCeti.nullMeasurable_cTransform {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {c : X × Y → ℝ} {φ : X → EReal} (μ : MeasureTheory.Measure Y) [MeasureTheory.SFinite μ] (h : Measurable fun (z : X × Y) => ↑(c z) - φ z.1) : MeasureTheory.NullMeasurable (cTransform c φ) μ

A c-transform with Borel defining integrand is measurable for the completion of every s-finite Borel measure on the target. This is deliberately NullMeasurable, not Borel Measurable.

theorem TauCeti.nullMeasurable_cTransformSymm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {c : X × Y → ℝ} {ψ : Y → EReal} (μ : MeasureTheory.Measure X) [MeasureTheory.SFinite μ] (h : Measurable fun (z : X × Y) => ↑(c z) - ψ z.2) : MeasureTheory.NullMeasurable (cTransformSymm c ψ) μ

A symmetric c-transform with Borel defining integrand is measurable for the completion of every s-finite Borel measure on the source.