module public import Causalean.Stat.Coupling.Basic public import Mathlib.Algebra.Algebra.Defs public import Mathlib.Algebra.BigOperators.Group.Finset.Basic public import Mathlib.Algebra.BigOperators.Group.Finset.Defs public import Mathlib.Algebra.BigOperators.Group.Finset.Sigma public import Mathlib.Algebra.BigOperators.Pi public import Mathlib.Algebra.CharZero.Defs public import Mathlib.Algebra.Field.Defs public import Mathlib.Algebra.Group.Action.Defs public import Mathlib.Algebra.Group.Action.Pi public import Mathlib.Algebra.Group.Basic public import Mathlib.Algebra.Group.Defs public import Mathlib.Algebra.Group.Pi.Basic public import Mathlib.Algebra.GroupWithZero.Action.Defs public import Mathlib.Algebra.GroupWithZero.Basic public import Mathlib.Algebra.GroupWithZero.Defs public import Mathlib.Algebra.Module.Defs public import Mathlib.Algebra.NeZero public import Mathlib.Algebra.Notation.Indicator public import Mathlib.Algebra.Notation.Pi.Defs public import Mathlib.Algebra.Order.Archimedean.Basic public import Mathlib.Algebra.Order.Archimedean.Real.Basic public import Mathlib.Algebra.Order.BigOperators.Group.Finset public import Mathlib.Algebra.Order.Field.Basic public import Mathlib.Algebra.Order.Floor.Defs public import Mathlib.Algebra.Order.Group.Unbundled.Abs public import Mathlib.Algebra.Order.Group.Unbundled.Basic public import Mathlib.Algebra.Order.GroupWithZero.Basic public import Mathlib.Algebra.Order.GroupWithZero.Defs public import Mathlib.Algebra.Order.Monoid.Defs public import Mathlib.Algebra.Order.Monoid.Unbundled.Basic public import Mathlib.Algebra.Order.Monoid.Unbundled.Defs public import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE public import Mathlib.Algebra.Order.Ring.Defs public import Mathlib.Algebra.Ring.Defs public import Mathlib.Algebra.Ring.Nat public import Mathlib.Analysis.InnerProductSpace.Basic public import Mathlib.Analysis.InnerProductSpace.Defs public import Mathlib.Analysis.Normed.Field.Basic public import Mathlib.Analysis.Normed.Group.Basic public import Mathlib.Analysis.Normed.Group.Continuity public import Mathlib.Analysis.Normed.Group.Defs public import Mathlib.Analysis.Normed.Group.Real public import Mathlib.Analysis.Normed.Module.Basic public import Mathlib.Analysis.Normed.Ring.Basic public import Mathlib.Analysis.RCLike.Basic public import Mathlib.Data.ENNReal.Action public import Mathlib.Data.ENNReal.Basic public import Mathlib.Data.ENNReal.BigOperators public import Mathlib.Data.ENNReal.Operations public import Mathlib.Data.ENNReal.Real public import Mathlib.Data.Finite.Defs public import Mathlib.Data.Finset.Attach public import Mathlib.Data.Finset.BooleanAlgebra public import Mathlib.Data.Finset.Defs public import Mathlib.Data.Finset.Empty public import Mathlib.Data.Fintype.Defs public import Mathlib.Data.Fintype.EquivFin public import Mathlib.Data.Fintype.Sets public import Mathlib.Data.FunLike.Basic public import Mathlib.Data.Int.Cast.Defs public import Mathlib.Data.NNReal.Defs public import Mathlib.Data.Nat.Cast.Defs public import Mathlib.Data.Nat.Init public import Mathlib.Data.Real.Basic public import Mathlib.Data.Set.CoeSort public import Mathlib.Data.Set.Defs public import Mathlib.Data.Set.Finite.Basic public import Mathlib.Data.Set.Finite.Lattice public import Mathlib.Data.Set.Finite.Range public import Mathlib.Data.Set.Image public import Mathlib.Data.Set.Operations public import Mathlib.Data.SetLike.Basic public import Mathlib.Logic.IsEmpty.Basic public import Mathlib.Logic.IsEmpty.Defs public import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic public import Mathlib.MeasureTheory.Constructions.Polish.Basic public import Mathlib.MeasureTheory.Function.L1Space.Integrable public import Mathlib.MeasureTheory.Function.LocallyIntegrable public import Mathlib.MeasureTheory.Integral.Bochner.Basic public import Mathlib.MeasureTheory.Integral.Lebesgue.Basic public import Mathlib.MeasureTheory.Integral.Lebesgue.Countable public import Mathlib.MeasureTheory.MeasurableSpace.Constructions public import Mathlib.MeasureTheory.MeasurableSpace.Defs public import Mathlib.MeasureTheory.Measure.Comap public import Mathlib.MeasureTheory.Measure.Dirac public import Mathlib.MeasureTheory.Measure.Map public import Mathlib.MeasureTheory.Measure.MeasureSpace public import Mathlib.MeasureTheory.Measure.MeasureSpaceDef public import Mathlib.MeasureTheory.Measure.Regular public import Mathlib.MeasureTheory.Measure.Typeclasses.Finite public import Mathlib.MeasureTheory.Measure.Typeclasses.Probability public import Mathlib.Order.Basic public import Mathlib.Order.BoundedOrder.Basic public import Mathlib.Order.Bounds.Defs public import Mathlib.Order.CompleteBooleanAlgebra public import Mathlib.Order.CompleteLattice.Basic public import Mathlib.Order.CompleteLattice.Defs public import Mathlib.Order.ConditionallyCompleteLattice.Basic public import Mathlib.Order.ConditionallyCompleteLattice.Defs public import Mathlib.Order.ConditionallyCompleteLattice.Indexed public import Mathlib.Order.ConditionallyCompletePartialOrder.Defs public import Mathlib.Order.Defs.LinearOrder public import Mathlib.Order.Defs.PartialOrder public import Mathlib.Order.Lattice public import Mathlib.Order.Notation public import Mathlib.Order.SetNotation public import Mathlib.Tactic.Linarith.Lemmas public import Mathlib.Tactic.NormNum.Basic public import Mathlib.Tactic.NormNum.Ineq public import Mathlib.Tactic.NormNum.Inv public import Mathlib.Tactic.NormNum.Result public import Mathlib.Tactic.Positivity.Core public import Mathlib.Tactic.Ring.Basic public import Mathlib.Tactic.Ring.Common public import Mathlib.Topology.Algebra.Support public import Mathlib.Topology.Bases public import Mathlib.Topology.Compactness.Compact public import Mathlib.Topology.Compactness.Lindelof public import Mathlib.Topology.Compactness.SigmaCompact public import Mathlib.Topology.Defs.Filter public import Mathlib.Topology.Defs.Induced public import Mathlib.Topology.EMetricSpace.Defs public import Mathlib.Topology.EMetricSpace.Lipschitz public import Mathlib.Topology.GDelta.MetrizableSpace public import Mathlib.Topology.MetricSpace.Basic public import Mathlib.Topology.MetricSpace.Defs public import Mathlib.Topology.MetricSpace.Lipschitz public import Mathlib.Topology.MetricSpace.Polish public import Mathlib.Topology.MetricSpace.ProperSpace public import Mathlib.Topology.MetricSpace.Pseudo.Constructions public import Mathlib.Topology.MetricSpace.Pseudo.Defs public import Mathlib.Topology.Metrizable.Basic public import Mathlib.Topology.Metrizable.CompletelyMetrizable public import Mathlib.Topology.Metrizable.Uniformity public import Mathlib.Topology.Separation.GDelta public import Mathlib.Topology.Separation.Regular public import Mathlib.Topology.UniformSpace.Defs public import Mathlib.Topology.UniformSpace.Real public import Toolkit.Foundations.MeasureTheory.Quantization public import Toolkit.Foundations.MeasureTheory.Wasserstein public import Toolkit.Foundations.Optimization.Convex.FiniteTransport /-! # Kantorovich–Rubinstein duality Strong duality for the one-Wasserstein cost: for probability measures on a compact metric space, the coupling infimum `wasserstein1 μ ν` equals the supremum, over one-Lipschitz real functions, of the positive part of the expectation contrast `lipschitzContrast μ ν f`. The proof proceeds in three steps. * Finite support (any metric space): a minimizing finite transport plan and an approximate dual certificate (`Toolkit.Foundations.Optimization.Convex`) are turned into a coupling and, via a distance envelope, a single globally one-Lipschitz potential. * Compact spaces: finite measurable quantization (`Toolkit.Foundations.MeasureTheory.Quantization`) reduces to finite support, with an explicit lifting of quantized couplings; no general triangle inequality for the Wasserstein cost is needed. * Compact subsets: laws carried by a compact subset of an arbitrary metric space are transferred to that subset, giving the identity with test functions that are one-Lipschitz on the subset only. Reference: C. Villani, *Topics in Optimal Transportation*, AMS GSM 58 (2003), Theorem 1.14; R. M. Dudley, *Real Analysis and Probability* (2002), Theorem 11.8.2. -/ public section namespace Toolkit.Foundations.MeasureTheory open _root_.MeasureTheory open scoped BigOperators ENNReal NNReal section Potential variable {X : Type*} [MetricSpace X] {ι κ : Type*} /-- For [two lists of locations](hyp:x,y), the second indexed by [a finite nonempty set](hyp:hfinite,hκ), [source and target potentials](hyp:u,v) whose [sum never exceeds the distance between the corresponding locations](hyp:hdual) admit [a one-Lipschitz function lying above the source potentials at the source locations and below the negated target potentials at the target locations](goal). The function is the lower envelope of the shifted distance functions to the target locations. -/ theorem exists_lipschitz_potential [hfinite : Finite κ] [hκ : Nonempty κ] (x : ι → X) (y : κ → X) (u : ι → ℝ) (v : κ → ℝ) (hdual : ∀ i j, u i + v j ≤ dist (x i) (y j)) : ∃ f : X → ℝ, LipschitzWith 1 f ∧ (∀ i, u i ≤ f (x i)) ∧ (∀ j, f (y j) ≤ -v j) := by let f : X → ℝ := fun z => ⨅ j, dist z (y j) - v j have hbounded (z : X) : BddBelow (Set.range fun j => dist z (y j) - v j) := (Set.finite_range _).bddBelow refine ⟨f, LipschitzWith.of_le_add (fun z w => ?_), ?_, ?_⟩ · rw [← sub_le_iff_le_add] refine le_ciInf fun j => ?_ rw [sub_le_iff_le_add] calc f z ≤ dist z (y j) - v j := ciInf_le (hbounded z) j _ ≤ dist w (y j) - v j + dist z w := by rw [sub_add_eq_add_sub, add_comm (dist w (y j))] exact sub_le_sub_right (dist_triangle z w (y j)) (v j) · intro i exact le_ciInf fun j => le_sub_iff_add_le.mpr (hdual i j) · intro j simpa only [dist_self, zero_sub] using ciInf_le (hbounded (y j)) j end Potential section Finite variable {X : Type*} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] variable {ι κ : Type*} [Fintype ι] [Fintype κ] /-- For [row masses summing to one](hyp:ha), [a finite transport plan](hyp:hp) between [those masses and some column masses](hyp:a,b), and [two finite lists of locations](hyp:x,y), [there is a probability coupling of the two weighted Dirac mixtures whose expected distance equals the plan's total distance cost](goal). Repeated locations and zero weights are allowed, and no separability of the metric space is required. -/ theorem finiteTransportPlan_coupling (a : ι → ℝ≥0) (b : κ → ℝ≥0) (ha : ∑ i, (a i : ℝ) = 1) (x : ι → X) (y : κ → X) (p : ι → κ → ℝ) (hp : Optimization.Convex.IsFiniteTransportPlan a b p) : ∃ π : Measure (X × X), Causalean.Stat.IsCoupling π (∑ i, (a i : ℝ≥0∞) • Measure.dirac (x i)) (∑ j, (b j : ℝ≥0∞) • Measure.dirac (y j)) ∧ (∫⁻ z, edist z.1 z.2 ∂π) = ENNReal.ofReal (∑ i, ∑ j, dist (x i) (y j) * p i j) := by classical have hrow (i : ι) : ∑ j, ENNReal.ofReal (p i j) = (a i : ℝ≥0∞) := by rw [← ENNReal.ofReal_sum_of_nonneg (fun j _ => hp.1 i j), hp.2.1 i] simp have hcol (j : κ) : ∑ i, ENNReal.ofReal (p i j) = (b j : ℝ≥0∞) := by rw [← ENNReal.ofReal_sum_of_nonneg (fun i _ => hp.1 i j), hp.2.2 j] simp have hmass : ∑ i, (a i : ℝ≥0∞) = 1 := by have h := congrArg ENNReal.ofReal ha simpa only [ENNReal.ofReal_sum_of_nonneg (fun i _ => (a i).coe_nonneg), ENNReal.ofReal_coe_nnreal, ENNReal.ofReal_one] using h let π : Measure (X × X) := ∑ i, ∑ j, ENNReal.ofReal (p i j) • Measure.dirac (x i, y j) refine ⟨π, ⟨?_, ?_, ?_⟩, ?_⟩ · constructor simpa [π, Measure.coe_finsetSum, hrow] using hmass · ext s hs simp only [Measure.map_apply measurable_fst hs, π, Measure.coe_finsetSum, Finset.sum_apply, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply, Set.indicator_apply, Set.mem_preimage, Pi.one_apply] apply Finset.sum_congr rfl intro i _ by_cases hi : x i ∈ s <;> simp [hi, hrow] · ext s hs simp only [Measure.map_apply measurable_snd hs, π, Measure.coe_finsetSum, Finset.sum_apply, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply, Set.indicator_apply, Set.mem_preimage, Pi.one_apply] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro j _ by_cases hj : y j ∈ s <;> simp [hj, hcol] · simp only [π, lintegral_finsetSum_measure, lintegral_smul_measure, lintegral_dirac, smul_eq_mul] rw [ENNReal.ofReal_sum_of_nonneg (fun i _ => Finset.sum_nonneg fun j _ => mul_nonneg dist_nonneg (hp.1 i j))] apply Finset.sum_congr rfl intro i _ rw [ENNReal.ofReal_sum_of_nonneg (fun j _ => mul_nonneg dist_nonneg (hp.1 i j))] apply Finset.sum_congr rfl intro j _ rw [ENNReal.ofReal_mul dist_nonneg, edist_dist, mul_comm] /-- **Kantorovich–Rubinstein duality for finitely many atoms.** For [two finite lists of locations](hyp:x,y) in a metric space carrying [nonnegative weights each summing to one](hyp:a,b,ha,hb), [the one-Wasserstein cost between the two weighted Dirac mixtures equals the supremum, over all one-Lipschitz functions, of the positive part of their expectation contrast](goal). -/ theorem wasserstein1_atomic_eq_iSup (a : ι → ℝ≥0) (b : κ → ℝ≥0) (ha : ∑ i, (a i : ℝ) = 1) (hb : ∑ j, (b j : ℝ) = 1) (x : ι → X) (y : κ → X) : wasserstein1 (∑ i, (a i : ℝ≥0∞) • Measure.dirac (x i)) (∑ j, (b j : ℝ≥0∞) • Measure.dirac (y j)) = ⨆ f : {f : X → ℝ // LipschitzWith 1 f}, ENNReal.ofReal (lipschitzContrast (∑ i, (a i : ℝ≥0∞) • Measure.dirac (x i)) (∑ j, (b j : ℝ≥0∞) • Measure.dirac (y j)) f.val) := by -- Weak duality gives one inequality. For the other, take a minimizing plan, -- near-optimal dual potentials and their Lipschitz envelope, and let the -- LP tolerance vanish. classical have hintμ (f : X → ℝ) : Integrable f (∑ i, (a i : ℝ≥0∞) • Measure.dirac (x i)) := by apply integrable_finsetSum_measure.mpr intro i _ exact (integrable_dirac (by simp)).smul_measure ENNReal.coe_ne_top have hintν (f : X → ℝ) : Integrable f (∑ j, (b j : ℝ≥0∞) • Measure.dirac (y j)) := by apply integrable_finsetSum_measure.mpr intro j _ exact (integrable_dirac (by simp)).smul_measure ENNReal.coe_ne_top have hint_eqμ (f : X → ℝ) : (∫ q, f q ∂(∑ i, (a i : ℝ≥0∞) • Measure.dirac (x i))) = ∑ i, (a i : ℝ) * f (x i) := by rw [integral_finsetSum_measure (fun i _ => (integrable_dirac (by simp)).smul_measure ENNReal.coe_ne_top)] simp [NNReal.smul_def, smul_eq_mul] have hint_eqν (f : X → ℝ) : (∫ q, f q ∂(∑ j, (b j : ℝ≥0∞) • Measure.dirac (y j))) = ∑ j, (b j : ℝ) * f (y j) := by rw [integral_finsetSum_measure (fun j _ => (integrable_dirac (by simp)).smul_measure ENNReal.coe_ne_top)] simp [NNReal.smul_def, smul_eq_mul] let μ := ∑ i, (a i : ℝ≥0∞) • Measure.dirac (x i) let ν := ∑ j, (b j : ℝ≥0∞) • Measure.dirac (y j) let S := ⨆ f : {f : X → ℝ // LipschitzWith 1 f}, ENNReal.ofReal (lipschitzContrast μ ν f.val) have hweak : S ≤ wasserstein1 μ ν := by exact iSup_le fun f => lipschitzContrast_le_wasserstein1 f.property (hintμ f.val) (hintν f.val) obtain ⟨p, hp, hmin⟩ := Optimization.Convex.exists_minimal_finiteTransportPlan a b ha hb (fun i j => dist (x i) (y j)) obtain ⟨π, hπ, hcost⟩ := finiteTransportPlan_coupling a b ha x y p hp have hupper : wasserstein1 μ ν ≤ ENNReal.ofReal (∑ i, ∑ j, dist (x i) (y j) * p i j) := by exact hcost ▸ wasserstein1_le_cost hπ have hSfinite : S ≠ ⊤ := ne_top_of_le_ne_top ENNReal.ofReal_ne_top (hweak.trans hupper) have : Nonempty κ := by by_contra h have : IsEmpty κ := not_nonempty_iff.mp h simp at hb have hreverse : ENNReal.ofReal (∑ i, ∑ j, dist (x i) (y j) * p i j) ≤ S := by apply (ENNReal.ofReal_le_iff_le_toReal hSfinite).mpr apply le_of_forall_pos_le_add intro ε hε obtain ⟨u, v, huv, hnear⟩ := Optimization.Convex.finiteTransport_dual_certificate a b (fun i j => dist (x i) (y j)) p hp hmin hε obtain ⟨f, hf, hsource, htarget⟩ := exists_lipschitz_potential x y u v huv have hcontrast : (∑ i, (a i : ℝ) * u i) + (∑ j, (b j : ℝ) * v j) ≤ lipschitzContrast μ ν f := by have hleft := Finset.sum_le_sum (fun i (_ : i ∈ Finset.univ) => mul_le_mul_of_nonneg_left (hsource i) (a i).coe_nonneg) have hright := Finset.sum_le_sum (fun j (_ : j ∈ Finset.univ) => mul_le_mul_of_nonneg_left (htarget j) (b j).coe_nonneg) simp only [mul_neg, Finset.sum_neg_distrib] at hright rw [lipschitzContrast, hint_eqμ, hint_eqν] linarith have htest : lipschitzContrast μ ν f ≤ S.toReal := by apply (ENNReal.ofReal_le_iff_le_toReal hSfinite).mp exact le_iSup (fun g : {g : X → ℝ // LipschitzWith 1 g} => ENNReal.ofReal (lipschitzContrast μ ν g.val)) ⟨f, hf⟩ linarith [hcontrast.trans htest] exact le_antisymm (hupper.trans hreverse) hweak /-- For [two probability measures](hyp:hμ,hν) [carried by finite sets](hyp:s,t,hs,ht) in a metric space, [their one-Wasserstein cost equals the supremum, over all one-Lipschitz functions, of the positive part of their expectation contrast](goal). -/ theorem wasserstein1_eq_iSup_of_finite_carrier (μ ν : Measure X) [hμ : IsProbabilityMeasure μ] [hν : IsProbabilityMeasure ν] (s t : Finset X) (hs : μ (s : Set X) = 1) (ht : ν (t : Set X) = 1) : wasserstein1 μ ν = ⨆ f : {f : X → ℝ // LipschitzWith 1 f}, ENNReal.ofReal (lipschitzContrast μ ν f.val) := by classical let a : s → ℝ≥0 := fun i => (μ {i.val}).toNNReal let b : t → ℝ≥0 := fun j => (ν {j.val}).toNNReal have hμdec := measure_eq_sum_dirac_of_finite_carrier μ s hs have hνdec := measure_eq_sum_dirac_of_finite_carrier ν t ht have hμmass : ∑ i : s, μ {i.val} = 1 := by have h := congrArg (fun m : Measure X => m Set.univ) hμdec simpa [Measure.coe_finsetSum] using h.symm have hνmass : ∑ j : t, ν {j.val} = 1 := by have h := congrArg (fun m : Measure X => m Set.univ) hνdec simpa [Measure.coe_finsetSum] using h.symm have ha : ∑ i, (a i : ℝ) = 1 := by have h := congrArg ENNReal.toReal hμmass rw [ENNReal.toReal_sum (fun (i : s) _ => measure_ne_top μ {i.val})] at h change (∑ i : s, (μ {i.val}).toReal) = 1 simpa only [ENNReal.toReal_one] using h have hb : ∑ j, (b j : ℝ) = 1 := by have h := congrArg ENNReal.toReal hνmass rw [ENNReal.toReal_sum (fun (j : t) _ => measure_ne_top ν {j.val})] at h change (∑ j : t, (ν {j.val}).toReal) = 1 simpa only [ENNReal.toReal_one] using h have hμeq : μ = ∑ i : s, (a i : ℝ≥0∞) • Measure.dirac i.val := by simpa only [a, ENNReal.coe_toNNReal (measure_ne_top μ _)] using hμdec have hνeq : ν = ∑ j : t, (b j : ℝ≥0∞) • Measure.dirac j.val := by simpa only [b, ENNReal.coe_toNNReal (measure_ne_top ν _)] using hνdec rw [hμeq, hνeq] exact wasserstein1_atomic_eq_iSup a b ha hb (fun i => i.val) (fun j => j.val) end Finite section Compact variable {X : Type*} [MetricSpace X] [CompactSpace X] [SecondCountableTopology X] [MeasurableSpace X] [BorelSpace X] /-- **Kantorovich–Rubinstein duality.** For [two probability measures](hyp:hμ,hν) on a compact metric space, [the one-Wasserstein cost (the infimum over couplings of the expected distance) equals the supremum, over all one-Lipschitz real functions, of the positive part of their expectation contrast](goal). -/ theorem wasserstein1_eq_iSup_lipschitz (μ ν : Measure X) [hμ : IsProbabilityMeasure μ] [hν : IsProbabilityMeasure ν] : wasserstein1 μ ν = ⨆ f : {f : X → ℝ // LipschitzWith 1 f}, ENNReal.ofReal (lipschitzContrast μ ν f.val) := by -- Quantize at a quarter of the target error: lifting quantized couplings -- and moving Lipschitz contrasts each cost at most twice the mesh. apply le_antisymm · classical apply ENNReal.le_of_forall_pos_le_add intro η hη _ let δ : ℝ := (η : ℝ) / 4 have hδ : 0 < δ := by dsimp [δ] exact div_pos (NNReal.coe_pos.mpr hη) (by norm_num) obtain ⟨q, hq, hqfinite, hmesh⟩ := exists_measurable_finite_quantization (X := X) hδ let : IsProbabilityMeasure (μ.map q) := Measure.isProbabilityMeasure_map hq.aemeasurable let : IsProbabilityMeasure (ν.map q) := Measure.isProbabilityMeasure_map hq.aemeasurable have hμcarrier : (μ.map q) (hqfinite.toFinset : Set X) = 1 := by rw [hqfinite.coe_toFinset, Measure.map_apply hq hqfinite.measurableSet] have hpre : q ⁻¹' Set.range q = Set.univ := by ext x simp rw [hpre, measure_univ] have hνcarrier : (ν.map q) (hqfinite.toFinset : Set X) = 1 := by rw [hqfinite.coe_toFinset, Measure.map_apply hq hqfinite.measurableSet] have hpre : q ⁻¹' Set.range q = Set.univ := by ext x simp rw [hpre, measure_univ] have hlift : wasserstein1 μ ν ≤ wasserstein1 (μ.map q) (ν.map q) + ENNReal.ofReal (2 * δ) := by unfold wasserstein1 rw [ENNReal.iInf_add] refine le_iInf fun θ => ?_ rw [ENNReal.iInf_add] refine le_iInf fun hθ => ?_ obtain ⟨π, hπ, hcost⟩ := lift_quantized_coupling μ ν q q hq hq hqfinite hqfinite hδ.le hmesh hmesh hθ exact (wasserstein1_le_cost hπ).trans hcost have hdual : wasserstein1 (μ.map q) (ν.map q) ≤ (⨆ f : {f : X → ℝ // LipschitzWith 1 f}, ENNReal.ofReal (lipschitzContrast μ ν f.val)) + ENNReal.ofReal (2 * δ) := by rw [wasserstein1_eq_iSup_of_finite_carrier (μ.map q) (ν.map q) hqfinite.toFinset hqfinite.toFinset hμcarrier hνcarrier] refine iSup_le fun f => ?_ have hbound := lipschitzContrast_quantization_bound μ ν q hq hmesh f.property rw [abs_sub_comm] at hbound have hcontrast : lipschitzContrast (μ.map q) (ν.map q) f.val ≤ lipschitzContrast μ ν f.val + 2 * δ := by linarith [le_abs_self (lipschitzContrast (μ.map q) (ν.map q) f.val - lipschitzContrast μ ν f.val)] exact (ENNReal.ofReal_le_ofReal hcontrast).trans (ENNReal.ofReal_add_le.trans (add_le_add (le_iSup (fun g : {g : X → ℝ // LipschitzWith 1 g} => ENNReal.ofReal (lipschitzContrast μ ν g.val)) f) le_rfl)) have herror : ENNReal.ofReal (2 * δ) + ENNReal.ofReal (2 * δ) = (η : ℝ≥0∞) := by rw [← ENNReal.ofReal_add (by positivity : 0 ≤ 2 * δ) (by positivity : 0 ≤ 2 * δ)] have heq : 2 * δ + 2 * δ = (η : ℝ) := by dsimp [δ]; ring rw [heq, ENNReal.ofReal_coe_nnreal] calc wasserstein1 μ ν ≤ wasserstein1 (μ.map q) (ν.map q) + ENNReal.ofReal (2 * δ) := hlift _ ≤ ((⨆ f : {f : X → ℝ // LipschitzWith 1 f}, ENNReal.ofReal (lipschitzContrast μ ν f.val)) + ENNReal.ofReal (2 * δ)) + ENNReal.ofReal (2 * δ) := add_le_add hdual le_rfl _ = (⨆ f : {f : X → ℝ // LipschitzWith 1 f}, ENNReal.ofReal (lipschitzContrast μ ν f.val)) + (η : ℝ≥0∞) := by rw [add_assoc, herror] · refine iSup_le fun f => ?_ exact lipschitzContrast_le_wasserstein1 f.property (f.property.continuous.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace f.val)) (f.property.continuous.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace f.val)) /-- For [two probability measures](hyp:hμ,hν) on a compact metric space and [a fixed reference point](hyp:x₀), [their one-Wasserstein cost equals the supremum of the positive part of their expectation contrast over one-Lipschitz functions vanishing at that point](goal). -/ theorem wasserstein1_eq_iSup_lipschitz_normalized (μ ν : Measure X) [hμ : IsProbabilityMeasure μ] [hν : IsProbabilityMeasure ν] (x₀ : X) : wasserstein1 μ ν = ⨆ f : {f : X → ℝ // LipschitzWith 1 f ∧ f x₀ = 0}, ENNReal.ofReal (lipschitzContrast μ ν f.val) := by rw [wasserstein1_eq_iSup_lipschitz μ ν] apply le_antisymm · refine iSup_le fun f => ?_ let g : X → ℝ := fun x => f.val x - f.val x₀ have hg : LipschitzWith 1 g := by intro x y simpa only [g, edist_dist, Real.dist_eq, sub_sub_sub_cancel_right] using f.property x y have hgzero : g x₀ = 0 := sub_self _ have hcontrast : lipschitzContrast μ ν g = lipschitzContrast μ ν f.val := by have hfμ : Integrable f.val μ := f.property.continuous.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace f.val) have hfν : Integrable f.val ν := f.property.continuous.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace f.val) simp only [lipschitzContrast, g, integral_sub hfμ (integrable_const (f.val x₀)), integral_sub hfν (integrable_const (f.val x₀)), integral_const, probReal_univ, one_smul] ring rw [← hcontrast] exact le_iSup_of_le ⟨g, hg, hgzero⟩ le_rfl · refine iSup_le fun f => ?_ exact le_iSup_of_le ⟨f.val, f.property.1⟩ le_rfl end Compact section Subset variable {X : Type*} [MetricSpace X] [MeasurableSpace X] /-- For [two probability laws](hyp:hμ,hν) giving [full mass to the same measurable set](hyp:K,hK,hμK,hνK), [the supremum of the positive part of their expectation contrast over functions one-Lipschitz on that set equals the same supremum for their laws on that set over one-Lipschitz functions there](goal). -/ theorem iSup_lipschitzOn_eq_subtype (μ ν : Measure X) [hμ : IsProbabilityMeasure μ] [hν : IsProbabilityMeasure ν] (K : Set X) (hK : MeasurableSet K) (hμK : μ K = 1) (hνK : ν K = 1) : (⨆ f : {f : X → ℝ // LipschitzOnWith 1 f K}, ENNReal.ofReal (lipschitzContrast μ ν f.val)) = ⨆ f : {f : K → ℝ // LipschitzWith 1 f}, ENNReal.ofReal (lipschitzContrast (μ.comap ((↑) : K → X)) (ν.comap ((↑) : K → X)) f.val) := by classical apply le_antisymm · refine iSup_le fun f => ?_ rw [lipschitzContrast_eq_subtype_comap μ ν K hK hμK hνK] exact le_iSup_of_le ⟨fun x : K => f.val x.val, f.property.to_restrict⟩ le_rfl · refine iSup_le fun f => ?_ let g : X → ℝ := fun x => if hx : x ∈ K then f.val ⟨x, hx⟩ else 0 have hg : LipschitzOnWith 1 g K := by intro x hx y hy simpa only [g, dif_pos hx, dif_pos hy, edist_dist, Subtype.dist_eq] using f.property ⟨x, hx⟩ ⟨y, hy⟩ have heq : (fun x : K => g x.val) = f.val := by funext x simp only [g, dif_pos x.property] have hc := lipschitzContrast_eq_subtype_comap μ ν K hK hμK hνK g rw [heq] at hc rw [← hc] exact le_iSup_of_le ⟨g, hg⟩ le_rfl variable [BorelSpace X] /-- **Kantorovich–Rubinstein duality on a compact subset.** For [two probability measures](hyp:hμ,hν) on a metric space and [a compact subset](hyp:K,hK) [to which both give full mass](hyp:hμK,hνK), [their one-Wasserstein cost equals the supremum, over functions one-Lipschitz on that subset, of the positive part of their expectation contrast](goal). The ambient space need not be compact or separable, and the test functions need not be measurable off the subset. -/ theorem wasserstein1_eq_iSup_lipschitzOn (μ ν : Measure X) [hμ : IsProbabilityMeasure μ] [hν : IsProbabilityMeasure ν] (K : Set X) (hK : IsCompact K) (hμK : μ K = 1) (hνK : ν K = 1) : wasserstein1 μ ν = ⨆ f : {f : X → ℝ // LipschitzOnWith 1 f K}, ENNReal.ofReal (lipschitzContrast μ ν f.val) := by let : CompactSpace K := isCompact_iff_compactSpace.mp hK let : IsProbabilityMeasure (μ.comap ((↑) : K → X)) := (probability_comap_subtype μ K hK.measurableSet hμK).1 let : IsProbabilityMeasure (ν.comap ((↑) : K → X)) := (probability_comap_subtype ν K hK.measurableSet hνK).1 rw [wasserstein1_subtype_comap μ ν K hK.measurableSet hμK hνK, wasserstein1_eq_iSup_lipschitz, iSup_lipschitzOn_eq_subtype μ ν K hK.measurableSet hμK hνK] end Subset end Toolkit.Foundations.MeasureTheory