The twist condition and uniqueness of contact partners

Let φ, ψ be a dual feasible pair for a real cost c on E × Y, where E is a real normed space, so that φ x' + ψ y ≤ c (x', y) everywhere, and let (x, y) lie in their contact set, where this is an equality. Then x' ↦ c (x', y) - φ x' attains its minimum at x. If both φ and the section c (·, y) are differentiable at x, the first-order condition for that minimum says that the derivative of the potential at x is the x-derivative of the cost at (x, y):

D φ (x) = Dₓ c (x, y).

The right-hand side depends on y and the left-hand side does not. So if the cost satisfies the twist condition — for each x, the map y ↦ Dₓ c (x, y) is injective — then at every point where φ is differentiable there is at most one contact partner y. When φ is differentiable μ-almost everywhere, almost every contact fibre is therefore a subsingleton.

A plan concentrated on the contact set then has deterministic conditional laws: together with TauCeti.IsCoupling.ae_exists_condKernel_eq_dirac, the conditional kernel of such a coupling is, for μ-almost every x, the Dirac mass at the unique contact partner of x. Once a dual optimizer exists, every optimal plan is concentrated on its contact set (TauCeti.IsDualCertificate.of_isOptimalCoupling), so this gives uniqueness of the optimal plan, TauCeti.IsDualCertificate.eq_of_isOptimalCoupling. This gives deterministic conditional laws and uniqueness of optimal plans for twisted costs under the stated nonnegativity and almost-everywhere differentiability hypotheses. The Euclidean quadratic cost satisfies the twist condition since Dₓ c (x, y) = x - y up to the Riesz identification. Differentiable, strictly convex displacement costs c (x, y) = h (x - y) also fit when h is nonnegative, its sections are differentiable at contact partners, and the potential is differentiable μ-almost everywhere; then Dₓ c (x, y) = D h (x - y). For strictly convex h that need not be differentiable, TauCeti.subsingleton_setOf_mem_contactSet_of_strictConvexOn replaces D h by the subgradients of h.

The potential φ is extended-real valued, as the c-concave potentials of TauCeti.cTransformSymm are. It is differentiated through EReal.toReal, and the statements ask that φ not take the value ⊥ near the point, since the dual constraint carries no information where φ = ⊥. The value ⊤ is excluded automatically wherever the constraint holds against a contact partner.

The pointwise statements, TauCeti.hasFDerivAt_eq_of_mem_contactSet and TauCeti.subsingleton_setOf_mem_contactSet, use only local feasibility and differentiability of the cost sections at the contact partners, with twist asked for on the set where the x-derivative of the cost exists. The measure-level statements require these hypotheses only μ-almost everywhere. Nothing about semiconcavity of the cost is assumed; the differentiability of φ is a hypothesis, to be supplied by a Rademacher-type theorem for the potentials at hand.

Main statements

• TauCeti.isLocalMin_sub_toReal_of_mem_contactSet — at a contact point (x, y), the function x' ↦ c (x', y) - φ x' has a local minimum at x;
• TauCeti.hasFDerivAt_eq_of_mem_contactSet — the first-order condition D φ (x) = Dₓ c (x, y) at a contact point, and TauCeti.fderiv_eq_of_mem_contactSet its fderiv form;
• TauCeti.subsingleton_setOf_mem_contactSet — under the twist condition, a point where the potential is differentiable has at most one contact partner;
• TauCeti.fderiv_norm_sub_sq_div_two and TauCeti.fderiv_norm_sub_sq_div_two_injective — the quadratic cost ‖x - y‖ ^ 2 / 2 on a real inner product space has x-derivative ⟪x - y, ·⟫, and is therefore twisted;
• TauCeti.fderiv_sqrt_one_add_norm_sub_sq, TauCeti.neg_fderiv_sqrt_one_add_norm_sub_sq, TauCeti.toDual_symm_neg_fderiv_sqrt_one_add_norm_sub_sq and TauCeti.fderiv_sqrt_one_add_norm_sub_sq_injective — the cost √(1 + ‖x - y‖ ^ 2) on a real inner product space has momentum ⟪(y - x) / √(1 + ‖y - x‖ ^ 2), ·⟫ at x, and is therefore twisted;
• TauCeti.ae_subsingleton_setOf_mem_contactSet — the contact fibres are almost all subsingletons when the potential is differentiable almost everywhere;
• TauCeti.IsDualCertificate.ae_exists_condKernel_eq_dirac — optimal couplings have almost everywhere Dirac conditional laws at contact partners;
• TauCeti.IsDualCertificate.eq_of_isOptimalCoupling — under the same hypotheses, a coupling certified by a dual pair is the only optimal coupling.

References

• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer 2009, Chapter 10, the twist condition and the solution of the Monge problem for twisted costs;
• W. Gangbo and R. J. McCann, The geometry of optimal transportation, Acta Math. 177 (1996), 113--161;
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Progress in Nonlinear Differential Equations and their Applications 87, Birkhäuser 2015, §1.3.

The first-order condition at a contact point

theorem TauCeti.isLocalMin_sub_toReal_of_mem_contactSet {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {c : X × Y → ℝ} {φ : X → EReal} {ψ : Y → EReal} {x : X} {y : Y} (hfeas : ∀ᶠ (x' : X) in nhds x, φ x' + ψ y ≤ ↑(c (x', y))) (hfin : ∀ᶠ (x' : X) in nhds x, φ x' ≠ ⊥) (hxy : (x, y) ∈ contactSet c φ ψ) : IsLocalMin (fun (x' : X) => c (x', y) - (φ x').toReal) x

Contact points minimise the cost minus the potential. If the dual constraint φ x' + ψ y ≤ c (x', y) holds for x' near x and is an equality at x, and φ does not take the value ⊥ near x, then x' ↦ c (x', y) - (φ x').toReal has a local minimum at x.

theorem TauCeti.hasFDerivAt_eq_of_mem_contactSet {E : Type u_1} {Y : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : E × Y → ℝ} {φ : E → EReal} {ψ : Y → EReal} {x : E} {y : Y} {φ' c' : E →L[ℝ] ℝ} (hfeas : ∀ᶠ (x' : E) in nhds x, φ x' + ψ y ≤ ↑(c (x', y))) (hfin : ∀ᶠ (x' : E) in nhds x, φ x' ≠ ⊥) (hxy : (x, y) ∈ contactSet c φ ψ) (hφ : HasFDerivAt (fun (x' : E) => (φ x').toReal) φ' x) (hc : HasFDerivAt (fun (x' : E) => c (x', y)) c' x) : φ' = c'

The first-order condition at a contact point. If the dual constraint φ x' + ψ y ≤ c (x', y) holds for x' near x and is an equality at x, then the derivative of the potential at x is the x-derivative of the cost at (x, y). The potential is differentiated through EReal.toReal, and is asked not to take the value ⊥ near x.

theorem TauCeti.fderiv_eq_of_mem_contactSet {E : Type u_1} {Y : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : E × Y → ℝ} {φ : E → EReal} {ψ : Y → EReal} {x : E} {y : Y} (hfeas : ∀ᶠ (x' : E) in nhds x, φ x' + ψ y ≤ ↑(c (x', y))) (hfin : ∀ᶠ (x' : E) in nhds x, φ x' ≠ ⊥) (hxy : (x, y) ∈ contactSet c φ ψ) (hφ : DifferentiableAt ℝ (fun (x' : E) => (φ x').toReal) x) (hc : DifferentiableAt ℝ (fun (x' : E) => c (x', y)) x) : fderiv ℝ (fun (x' : E) => (φ x').toReal) x = fderiv ℝ (fun (x' : E) => c (x', y)) x

The fderiv form of TauCeti.hasFDerivAt_eq_of_mem_contactSet: at a contact point, the derivative of the potential is the x-derivative of the cost.

The twist condition

theorem TauCeti.subsingleton_setOf_mem_contactSet {E : Type u_1} {Y : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : E × Y → ℝ} {φ : E → EReal} {ψ : Y → EReal} {x : E} (hfeas : ∀ (y : Y), ∀ᶠ (x' : E) in nhds x, φ x' + ψ y ≤ ↑(c (x', y))) (hfin : ∀ᶠ (x' : E) in nhds x, φ x' ≠ ⊥) (hφ : DifferentiableAt ℝ (fun (x' : E) => (φ x').toReal) x) (hc : ∀ (y : Y), (x, y) ∈ contactSet c φ ψ → DifferentiableAt ℝ (fun (x' : E) => c (x', y)) x) (htwist : Set.InjOn (fun (y : Y) => fderiv ℝ (fun (x' : E) => c (x', y)) x) {y : Y | DifferentiableAt ℝ (fun (x' : E) => c (x', y)) x}) : {y : Y | (x, y) ∈ contactSet c φ ψ}.Subsingleton

The twist theorem at a point. Suppose the cost is twisted at x: the map y ↦ Dₓ c (x, y) is injective on the set of y for which the section c (·, y) is differentiable at x. If the potential is differentiable at x, finite near x, and satisfies the dual constraint near x, and the cost sections of the contact partners of x are differentiable at x, then x has at most one contact partner.

theorem TauCeti.fderiv_norm_sub_sq_div_two {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) : fderiv ℝ (fun (x' : F) => ‖x' - y‖ ^ 2 / 2) x = (innerSL ℝ) (x - y)

On a real inner product space, the x-derivative of the quadratic cost ‖x - y‖ ^ 2 / 2 at x is ⟪x - y, ·⟫.

theorem TauCeti.fderiv_norm_sub_sq_div_two_injective {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) : Function.Injective fun (y : F) => fderiv ℝ (fun (x' : F) => ‖x' - y‖ ^ 2 / 2) x

The quadratic cost is twisted. On a real inner product space, the x-derivative of the cost ‖x - y‖ ^ 2 / 2 at x is ⟪x - y, ·⟫, which determines y.

theorem TauCeti.fderiv_sqrt_one_add_norm_sub_sq {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) : fderiv ℝ (fun (x' : F) => √(1 + ‖x' - y‖ ^ 2)) x = (√(1 + ‖x - y‖ ^ 2))⁻¹ • (innerSL ℝ) (x - y)

The x-derivative of the cost √(1 + ‖x - y‖ ^ 2) is ⟪x - y, ·⟫ / √(1 + ‖x - y‖ ^ 2).

theorem TauCeti.neg_fderiv_sqrt_one_add_norm_sub_sq {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) : -fderiv ℝ (fun (x' : F) => √(1 + ‖x' - y‖ ^ 2)) x = (innerSL ℝ) (↑OpenPartialHomeomorph.univUnitBall (y - x))

The momentum -Dₓ c (x, y) of y at x for the cost √(1 + ‖x - y‖ ^ 2) is the inner product against the image (y - x) / √(1 + ‖y - x‖ ^ 2) of y - x in the unit ball.

theorem TauCeti.toDual_symm_neg_fderiv_sqrt_one_add_norm_sub_sq {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (x y : F) : (InnerProductSpace.toDual ℝ F).symm (-fderiv ℝ (fun (x' : F) => √(1 + ‖x' - y‖ ^ 2)) x) = ↑OpenPartialHomeomorph.univUnitBall (y - x)

On a real Hilbert space, the inverse Riesz isomorphism sends the momentum -Dₓ c (x, y) of y at x for the cost √(1 + ‖x - y‖ ^ 2) to the image (y - x) / √(1 + ‖y - x‖ ^ 2) of y - x in the unit ball.

theorem TauCeti.fderiv_sqrt_one_add_norm_sub_sq_injective {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) : Function.Injective fun (y : F) => fderiv ℝ (fun (x' : F) => √(1 + ‖x' - y‖ ^ 2)) x

The cost √(1 + ‖x - y‖ ^ 2) is twisted. On a real inner product space, its x-derivative determines y.

theorem TauCeti.ae_subsingleton_setOf_mem_contactSet {E : Type u_1} {Y : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : E × Y → ℝ} {φ : E → EReal} {ψ : Y → EReal} [MeasurableSpace E] (μ : MeasureTheory.Measure E) (hfeas : ∀ (x : E) (y : Y), φ x + ψ y ≤ ↑(c (x, y))) (hφ : ∀ᵐ (x : E) ∂μ, (∀ᶠ (x' : E) in nhds x, φ x' ≠ ⊥) ∧ DifferentiableAt ℝ (fun (x' : E) => (φ x').toReal) x) (hc : ∀ᵐ (x : E) ∂μ, ∀ (y : Y), (x, y) ∈ contactSet c φ ψ → DifferentiableAt ℝ (fun (x' : E) => c (x', y)) x) (htwist : ∀ᵐ (x : E) ∂μ, Set.InjOn (fun (y : Y) => fderiv ℝ (fun (x' : E) => c (x', y)) x) {y : Y | DifferentiableAt ℝ (fun (x' : E) => c (x', y)) x}) : ∀ᵐ (x : E) ∂μ, {y : Y | (x, y) ∈ contactSet c φ ψ}.Subsingleton

The twist theorem. If the cost is differentiable in its first variable at contact partners and y ↦ Dₓ c (x, y) is injective among differentiable sections at almost every x, and a dual feasible pair has a first potential finite near, and differentiable at, μ-almost every point, then the contact fibres {y | (x, y) ∈ contactSet c φ ψ} are subsingletons for μ-almost every x. Combined with TauCeti.IsCoupling.ae_exists_condKernel_eq_dirac, a finite coupling of μ concentrated on the contact set has, for μ-almost every x, the Dirac mass at the unique contact partner of x as its conditional law.

theorem TauCeti.IsDualCertificate.ae_subsingleton_dualContactSet {E : Type u_1} {Y : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : E × Y → ℝ} [MeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} {φ : E → ℝ} {ψ : Y → ℝ} {π : MeasureTheory.Measure (E × Y)} (hc₀ : ∀ (z : E × Y), 0 ≤ c z) (h : IsDualCertificate (fun (z : E × Y) => ENNReal.ofReal (c z)) π μ ν φ ψ) (hφ : ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ φ x) (hc : ∀ᵐ (x : E) ∂μ, ∀ (y : Y), ((x, y) ∈ contactSet c (fun (x : E) => ↑(φ x)) fun (y : Y) => ↑(ψ y)) → DifferentiableAt ℝ (fun (x' : E) => c (x', y)) x) (htwist : ∀ᵐ (x : E) ∂μ, Set.InjOn (fun (y : Y) => fderiv ℝ (fun (x' : E) => c (x', y)) x) {y : Y | DifferentiableAt ℝ (fun (x' : E) => c (x', y)) x}) : ∀ᵐ (x : E) ∂μ, {y : Y | (x, y) ∈ dualContactSet (fun (z : E × Y) => ENNReal.ofReal (c z)) φ ψ}.Subsingleton

A certified dual pair with an almost everywhere differentiable source potential has almost everywhere subsingleton contact fibres under the twist condition.

theorem TauCeti.IsDualCertificate.ae_exists_condKernel_eq_dirac {E : Type u_1} {Y : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : E × Y → ℝ} [MeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} {φ : E → ℝ} {ψ : Y → ℝ} {π σ : MeasureTheory.Measure (E × Y)} [StandardBorelSpace Y] [Nonempty Y] (hc₀ : ∀ (z : E × Y), 0 ≤ c z) (h : IsDualCertificate (fun (z : E × Y) => ENNReal.ofReal (c z)) π μ ν φ ψ) (hσ : IsOptimalCoupling (fun (z : E × Y) => ENNReal.ofReal (c z)) σ μ ν) [MeasureTheory.IsFiniteMeasure σ] (hcσ : AEMeasurable (fun (z : E × Y) => ENNReal.ofReal (c z)) σ) (hφ : ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ φ x) (hc : ∀ᵐ (x : E) ∂μ, ∀ (y : Y), ((x, y) ∈ contactSet c (fun (x : E) => ↑(φ x)) fun (y : Y) => ↑(ψ y)) → DifferentiableAt ℝ (fun (x' : E) => c (x', y)) x) (htwist : ∀ᵐ (x : E) ∂μ, Set.InjOn (fun (y : Y) => fderiv ℝ (fun (x' : E) => c (x', y)) x) {y : Y | DifferentiableAt ℝ (fun (x' : E) => c (x', y)) x}) : ∀ᵐ (x : E) ∂μ, ∃ (y : Y), (x, y) ∈ dualContactSet (fun (z : E × Y) => ENNReal.ofReal (c z)) φ ψ ∧ σ.condKernel x = MeasureTheory.Measure.dirac y

Every optimal coupling certified by the same dual pair has almost everywhere Dirac conditional laws at its contact partners.

theorem TauCeti.IsDualCertificate.eq_of_isOptimalCoupling {E : Type u_1} {Y : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : E × Y → ℝ} [MeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} {φ : E → ℝ} {ψ : Y → ℝ} {π σ : MeasureTheory.Measure (E × Y)} [StandardBorelSpace Y] [Nonempty Y] [MeasureTheory.IsFiniteMeasure μ] (hc₀ : ∀ (z : E × Y), 0 ≤ c z) (h : IsDualCertificate (fun (z : E × Y) => ENNReal.ofReal (c z)) π μ ν φ ψ) (hσ : IsOptimalCoupling (fun (z : E × Y) => ENNReal.ofReal (c z)) σ μ ν) (hcσ : AEMeasurable (fun (z : E × Y) => ENNReal.ofReal (c z)) σ) (hφ : ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ φ x) (hc : ∀ᵐ (x : E) ∂μ, ∀ (y : Y), ((x, y) ∈ contactSet c (fun (x : E) => ↑(φ x)) fun (y : Y) => ↑(ψ y)) → DifferentiableAt ℝ (fun (x' : E) => c (x', y)) x) (htwist : ∀ᵐ (x : E) ∂μ, Set.InjOn (fun (y : Y) => fderiv ℝ (fun (x' : E) => c (x', y)) x) {y : Y | DifferentiableAt ℝ (fun (x' : E) => c (x', y)) x}) : σ = π

Uniqueness of the optimal plan for a twisted cost. Let c be a nonnegative real cost, differentiable at contact partners, with y ↦ Dₓ c (x, y) injective on differentiable sections at almost every x. If π is certified optimal 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 π.