BoundedCouplingDual.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Optimality from local dual potentials on bounded endpoint supports

theorem OAI.RegularPointCoordinates.bounded_pair_cost_integrable line 13
theorem OAI.RegularPointCoordinates.bounded_pair_transportCost line 21

theorem OAI.RegularPointCoordinates.bounded_coupling_optimal_of_dual line 30

Source documentation

Dual feasibility is needed only on the support of the endpoint marginals.

theorem bounded_coupling_optimal_of_dual {n : ℕ} {B : ℝ} (hB : 0≤B)
    (Q : ProbabilityMeasure (Euclidean n × Euclidean n))
    (hQ : ∀ᵐ z ∂(Q : Measure (Euclidean n × Euclidean n)),
      z∈closedBall (0:Euclidean n) B ×ˢ closedBall (0:Euclidean n) B)
    {f g : Euclidean n → ℝ} {L M : ℝ≥0}
    (hf : LipschitzWith L f) (hg : LipschitzWith M g)
    (had : ∀ x∈closedBall 0 B, ∀ y∈closedBall 0 B, f x+g y≤dist x y^2/2)
    (hc : (∫ z, f z.1+g z.2 ∂(Q : Measure (Euclidean n × Euclidean n)))=
      (∫ z, dist z.1 z.2^2 ∂(Q : Measure (Euclidean n × Euclidean n)))/2) :
    IsOptimalCoupling ((Q : Measure (Euclidean n × Euclidean n)).map Prod.fst)
      ((Q : Measure (Euclidean n × Euclidean n)).map Prod.snd) Q := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.IsOptimalCoupling