Contact partners for strictly convex displacement costs

Let h : E → ℝ be convex on a real normed space and consider the displacement cost c (x, y) = h (x - y). Such an h need not be differentiable, so the twist theorem TauCeti.subsingleton_setOf_mem_contactSet, which compares x-derivatives of the cost, does not apply. Gangbo and McCann replace the derivative of h by its subgradients.

Let (φ, ψ) satisfy the dual constraint φ x' + ψ y ≤ h (x' - y) near x, with equality at x, and let φ be differentiable at x. Then x' ↦ h (x' - y) - φ x' has a local minimum at x, so the derivative φ' of φ at x is a subgradient of h at x - y:

h (x - y) + φ' (w - (x - y)) ≤ h w for every w.

If h is strictly convex, distinct points have disjoint subdifferentials, so x - y, and hence the contact partner y, is determined by φ'. The pointwise statements use no differentiability, growth or nonnegativity of h. On a real inner product space, conjugate-subgradient reciprocity then gives x - y ∈ ∂h⋆(∇φ x), and where the Legendre–Fenchel conjugate h⋆ is differentiable this is the Gangbo–McCann formula y = x - ∇h⋆(∇φ x).

When φ is differentiable μ-almost everywhere, almost every contact fibre is therefore a subsingleton. A finite coupling concentrated on the contact set is then the graph plan of a measurable map T whose increments x - T x carry the derivative of φ as a subgradient of h, and it is the only coupling of its source marginal concentrated on that contact set.

Main statements

• TauCeti.add_le_of_mem_contactSet_sub — at a contact point of a convex displacement cost, the derivative of the potential is a subgradient of h at x - y, with TauCeti.mem_subdifferential_of_mem_contactSet_sub its form for an arbitrary pairing;
• TauCeti.subsingleton_setOf_mem_contactSet_of_strictConvexOn — for strictly convex h, a point where the potential is differentiable has at most one contact partner;
• TauCeti.gradient_fenchelConjugate_eq_sub_of_mem_contactSet — the formula x - y = ∇h⋆(∇φ x) at a contact point;
• TauCeti.ae_subsingleton_setOf_mem_contactSet_of_strictConvexOn — almost every contact fibre is a subsingleton when the potential is differentiable almost everywhere;
• TauCeti.IsCoupling.exists_graphPlan_of_ae_mem_contactSet_of_strictConvexOn and TauCeti.IsCoupling.eq_of_ae_mem_contactSet_of_strictConvexOn — a coupling concentrated on the contact set is induced by a measurable map, and is unique;
• TauCeti.IsDualCertificate.eq_of_isOptimalCoupling_of_strictConvexOn — uniqueness of the optimal plan for a certified nonnegative strictly convex displacement cost.

References

• W. Gangbo and R. J. McCann, The geometry of optimal transportation, Acta Math. 177 (1996), 113--161, for the subgradient form of the twist condition for strictly convex costs h (x - y).
• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Chapter 10.

The first-order condition

theorem TauCeti.add_le_of_mem_contactSet_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {h : E → ℝ} {φ ψ : E → EReal} {x y : E} {φ' : E →L[ℝ] ℝ} (hh : ConvexOn ℝ Set.univ h) (hfeas : ∀ᶠ (x' : E) in nhds x, φ x' + ψ y ≤ ↑(h (x' - y))) (hfin : ∀ᶠ (x' : E) in nhds x, φ x' ≠ ⊥) (hxy : (x, y) ∈ contactSet (fun (z : E × E) => h (z.1 - z.2)) φ ψ) (hφ : HasFDerivAt (fun (x' : E) => (φ x').toReal) φ' x) (w : E) : h (x - y) + φ' (w - (x - y)) ≤ h w

The first-order condition for a convex displacement cost. Let h be convex. If the dual constraint φ x' + ψ y ≤ h (x' - y) holds for x' near x and is an equality at x, φ does not take the value ⊥ near x, and its real representative has derivative φ' at x, then φ' is a subgradient of h at x - y. No differentiability of h is needed.

theorem TauCeti.mem_subdifferential_of_mem_contactSet_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {h : E → ℝ} {φ ψ : E → EReal} {x y : E} {F : Type u_2} [AddCommMonoid F] [Module ℝ F] (B : E →ₗ[ℝ] F →ₗ[ℝ] ℝ) {φ' : E →L[ℝ] ℝ} {p : F} (hh : ConvexOn ℝ Set.univ h) (hfeas : ∀ᶠ (x' : E) in nhds x, φ x' + ψ y ≤ ↑(h (x' - y))) (hfin : ∀ᶠ (x' : E) in nhds x, φ x' ≠ ⊥) (hxy : (x, y) ∈ contactSet (fun (z : E × E) => h (z.1 - z.2)) φ ψ) (hφ : HasFDerivAt (fun (x' : E) => (φ x').toReal) φ' x) (hp : ∀ (v : E), φ' v = (B v) p) : p ∈ subdifferential B (fun (z : E) => ↑(h z)) (x - y)

The form of TauCeti.add_le_of_mem_contactSet_sub for a pairing B: if p represents the derivative φ' of the potential at a contact point (x, y), then p ∈ ∂h(x - y).

Uniqueness of contact partners

theorem TauCeti.subsingleton_setOf_mem_contactSet_of_strictConvexOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {h : E → ℝ} {φ ψ : E → EReal} {x : E} (hh : StrictConvexOn ℝ Set.univ h) (hfeas : ∀ (y : E), ∀ᶠ (x' : E) in nhds x, φ x' + ψ y ≤ ↑(h (x' - y))) (hfin : ∀ᶠ (x' : E) in nhds x, φ x' ≠ ⊥) (hφ : DifferentiableAt ℝ (fun (x' : E) => (φ x').toReal) x) : {y : E | (x, y) ∈ contactSet (fun (z : E × E) => h (z.1 - z.2)) φ ψ}.Subsingleton

Contact partners for a strictly convex displacement cost. Let h be strictly convex. If the potential satisfies the dual constraint near x against every y, does not take the value ⊥ near x, and is differentiable at x, then x has at most one contact partner.

theorem TauCeti.ae_subsingleton_setOf_mem_contactSet_of_strictConvexOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {h : E → ℝ} {φ ψ : E → EReal} [MeasurableSpace E] (μ : MeasureTheory.Measure E) (hh : StrictConvexOn ℝ Set.univ h) (hfeas : ∀ (x y : E), φ x + ψ y ≤ ↑(h (x - y))) (hφ : ∀ᵐ (x : E) ∂μ, (∀ᶠ (x' : E) in nhds x, φ x' ≠ ⊥) ∧ DifferentiableAt ℝ (fun (x' : E) => (φ x').toReal) x) : ∀ᵐ (x : E) ∂μ, {y : E | (x, y) ∈ contactSet (fun (z : E × E) => h (z.1 - z.2)) φ ψ}.Subsingleton

Gangbo–McCann uniqueness of contact partners. For a strictly convex h and a dual feasible pair whose first potential is finite near, and differentiable at, μ-almost every point, the contact fibres of the cost h (x - y) are subsingletons for μ-almost every x.

theorem TauCeti.IsCoupling.exists_graphPlan_of_ae_mem_contactSet_of_strictConvexOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {h : E → ℝ} {φ ψ : E → EReal} [MeasurableSpace E] {μ ν : MeasureTheory.Measure E} [StandardBorelSpace E] {π : MeasureTheory.Measure (E × E)} [MeasureTheory.IsFiniteMeasure π] (hπ : IsCoupling π μ ν) (hh : StrictConvexOn ℝ Set.univ h) (hfeas : ∀ (x y : E), φ x + ψ y ≤ ↑(h (x - y))) (hφ : ∀ᵐ (x : E) ∂μ, (∀ᶠ (x' : E) in nhds x, φ x' ≠ ⊥) ∧ DifferentiableAt ℝ (fun (x' : E) => (φ x').toReal) x) (hcon : ∀ᵐ (z : E × E) ∂π, z ∈ contactSet (fun (z : E × E) => h (z.1 - z.2)) φ ψ) : ∃ (T : E → E), Measurable T ∧ ProbabilityTheory.HasLaw T ν μ ∧ π = graphPlan T μ ∧ ∀ᵐ (x : E) ∂μ, (x, T x) ∈ contactSet (fun (z : E × E) => h (z.1 - z.2)) φ ψ ∧ ∀ (w : E), h (x - T x) + (fderiv ℝ (fun (x' : E) => (φ x').toReal) x) (w - (x - T x)) ≤ h w

Couplings on a strictly convex contact set are induced by maps. Let h be strictly convex and let (φ, ψ) be a dual feasible pair for the cost h (x - y) whose first potential is finite near, and differentiable at, μ-almost every point. A finite coupling of μ and ν concentrated on the contact set is the graph plan of a measurable map T pushing μ to ν. For μ-almost every x, the pair (x, T x) is a contact point and the derivative of φ at x is a subgradient of h at x - T x.

theorem TauCeti.IsCoupling.eq_of_ae_mem_contactSet_of_strictConvexOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {h : E → ℝ} {φ ψ : E → EReal} [MeasurableSpace E] {μ ν : MeasureTheory.Measure E} [StandardBorelSpace E] {π : MeasureTheory.Measure (E × E)} [MeasureTheory.IsFiniteMeasure π] {π' : MeasureTheory.Measure (E × E)} {ν' : MeasureTheory.Measure E} (hπ : IsCoupling π μ ν) (hπ' : IsCoupling π' μ ν') (hh : StrictConvexOn ℝ Set.univ h) (hfeas : ∀ (x y : E), φ x + ψ y ≤ ↑(h (x - y))) (hφ : ∀ᵐ (x : E) ∂μ, (∀ᶠ (x' : E) in nhds x, φ x' ≠ ⊥) ∧ DifferentiableAt ℝ (fun (x' : E) => (φ x').toReal) x) (hcon : ∀ᵐ (z : E × E) ∂π, z ∈ contactSet (fun (z : E × E) => h (z.1 - z.2)) φ ψ) (hcon' : ∀ᵐ (z : E × E) ∂π', z ∈ contactSet (fun (z : E × E) => h (z.1 - z.2)) φ ψ) : π = π'

Uniqueness of couplings on a strictly convex contact set. Under the hypotheses of TauCeti.IsCoupling.exists_graphPlan_of_ae_mem_contactSet_of_strictConvexOn, two finite couplings of the same source marginal μ, both concentrated on the contact set, are equal. In particular their target marginals agree.

theorem TauCeti.IsDualCertificate.eq_of_isOptimalCoupling_of_strictConvexOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {h : E → ℝ} [MeasurableSpace E] {μ ν : MeasureTheory.Measure E} [StandardBorelSpace E] {π : MeasureTheory.Measure (E × E)} [MeasureTheory.IsFiniteMeasure μ] {φ ψ : E → ℝ} {σ : MeasureTheory.Measure (E × E)} (hh₀ : ∀ (z : E), 0 ≤ h z) (hh : StrictConvexOn ℝ Set.univ h) (hcert : IsDualCertificate (fun (z : E × E) => ENNReal.ofReal (h (z.1 - z.2))) π μ ν φ ψ) (hσ : IsOptimalCoupling (fun (z : E × E) => ENNReal.ofReal (h (z.1 - z.2))) σ μ ν) (hcσ : AEMeasurable (fun (z : E × E) => ENNReal.ofReal (h (z.1 - z.2))) σ) (hφ : ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ φ x) : σ = π

Uniqueness of the optimal plan for a strictly convex displacement cost. Let h be nonnegative and strictly convex. If π is certified optimal for the cost h (x - y) by a dual pair (φ, ψ) whose first potential is differentiable μ-almost everywhere, then every optimal coupling of μ and ν whose cost is almost everywhere measurable is equal to π.

theorem TauCeti.gradient_mem_subdifferential_of_mem_contactSet_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {h : E → ℝ} {φ ψ : E → EReal} {x y : E} (hh : ConvexOn ℝ Set.univ h) (hfeas : ∀ᶠ (x' : E) in nhds x, φ x' + ψ y ≤ ↑(h (x' - y))) (hfin : ∀ᶠ (x' : E) in nhds x, φ x' ≠ ⊥) (hxy : (x, y) ∈ contactSet (fun (z : E × E) => h (z.1 - z.2)) φ ψ) (hφ : DifferentiableAt ℝ (fun (x' : E) => (φ x').toReal) x) : gradient (fun (x' : E) => (φ x').toReal) x ∈ subdifferential (innerₗ E) (fun (z : E) => ↑(h z)) (x - y)

At a contact point of a convex displacement cost on a real inner product space, the gradient of the potential is a subgradient of h at x - y.

theorem TauCeti.gradient_fenchelConjugate_eq_sub_of_mem_contactSet {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {h : E → ℝ} {φ ψ : E → EReal} {x y : E} (hh : ConvexOn ℝ Set.univ h) (hfeas : ∀ᶠ (x' : E) in nhds x, φ x' + ψ y ≤ ↑(h (x' - y))) (hfin : ∀ᶠ (x' : E) in nhds x, φ x' ≠ ⊥) (hxy : (x, y) ∈ contactSet (fun (z : E × E) => h (z.1 - z.2)) φ ψ) (hφ : DifferentiableAt ℝ (fun (x' : E) => (φ x').toReal) x) (hdom : ∀ᶠ (q : E) in nhds (gradient (fun (x' : E) => (φ x').toReal) x), fenchelConjugate (innerₗ E) (fun (z : E) => ↑(h z)) q ≠ ⊤) (hconj : DifferentiableAt ℝ (fun (q : E) => (fenchelConjugate (innerₗ E) (fun (z : E) => ↑(h z)) q).toReal) (gradient (fun (x' : E) => (φ x').toReal) x)) : gradient (fun (q : E) => (fenchelConjugate (innerₗ E) (fun (z : E) => ↑(h z)) q).toReal) (gradient (fun (x' : E) => (φ x').toReal) x) = x - y

The Gangbo–McCann formula. Let h be convex on a real inner product space and let (x, y) be a contact point at which the potential is differentiable. If the Legendre–Fenchel conjugate h⋆ is finite near ∇φ x and differentiable there, then x - y = ∇h⋆(∇φ x), that is y = x - ∇h⋆(∇φ x).