Documentation

TauCeti.MeasureTheory.OptimalTransport.Cost.Quadratic

The quadratic transport cost and its cyclically monotone sets #

On a real inner product space E, the quadratic transport cost c (x, y) = ‖x - y‖ ^ 2 / 2 differs from the pairing cost -⟪x, y⟫ of TauCeti.MeasureTheory.OptimalTransport.Cost.Pairing by the split term ‖x‖ ^ 2 / 2 + ‖y‖ ^ 2 / 2. Split terms are invisible to cyclical monotonicity, so a set is c-cyclically monotone for the quadratic cost exactly when it is cyclically monotone in the classical sense ∑ i, ⟪x i, y (σ i)⟫ ≤ ∑ i, ⟪x i, y i⟫. The c-transform vocabulary of the quadratic cost is the Legendre–Fenchel vocabulary of the inner product; that dictionary is recorded in TauCeti.MeasureTheory.OptimalTransport.CTransform.Quadratic. Every statement in this file accounts for the factor 1 / 2 in the cost.

Main statements #

References #

theorem TauCeti.norm_sub_sq_div_two_eq_pairingCost_add_add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] :
(fun (p : E × E) => ‖p.1 - p.2‖ ^ 2 / 2) = fun (p : E × E) => pairingCost (innerₗ E) p + ‖p.1‖ ^ 2 / 2 + ‖p.2‖ ^ 2 / 2

The quadratic cost is the inner-product pairing cost plus the split term ‖x‖ ^ 2 / 2 + ‖y‖ ^ 2 / 2.

c-cyclical monotonicity for the quadratic cost is cyclical monotonicity for the inner-product pairing.

theorem TauCeti.isCyclicallyMonotone_norm_sub_sq_div_two_iff_forall_sum_inner_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {S : Set (E × E)} :
IsCyclicallyMonotone (fun (p : E × E) => ‖p.1 - p.2‖ ^ 2 / 2) S ↔ ∀ (n : ℕ) (x y : Fin n → E), (∀ (i : Fin n), (x i, y i) ∈ S) → ∀ (σ : Equiv.Perm (Fin n)), ∑ i : Fin n, inner ℝ (x i) (y (σ i)) ≤ ∑ i : Fin n, inner ℝ (x i) (y i)

c-cyclical monotonicity for the quadratic cost is the classical cyclical monotonicity condition: rearranging the targets of finitely many points of the set does not increase the total inner product.