module public import Causalean.Mathlib.MeasureTheory.FiniteAtomicMeasure public import Causalean.Stat.Coupling.Basic public import Causalean.Stat.Minimax.SideInformation.Finite.Selector 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.Piecewise public import Mathlib.Algebra.BigOperators.Group.Finset.Sigma public import Mathlib.Algebra.BigOperators.Ring.Finset public import Mathlib.Algebra.Group.Basic public import Mathlib.Algebra.Group.Defs public import Mathlib.Algebra.GroupWithZero.Action.Defs public import Mathlib.Algebra.GroupWithZero.Defs public import Mathlib.Algebra.Module.Defs public import Mathlib.Algebra.Notation.Defs public import Mathlib.Algebra.Notation.Indicator public import Mathlib.Algebra.Notation.Pi.Defs public import Mathlib.Algebra.Order.BigOperators.Group.Finset public import Mathlib.Algebra.Order.Group.Abs public import Mathlib.Algebra.Order.Group.Unbundled.Abs 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.Ring.Defs public import Mathlib.Algebra.Ring.Nat public import Mathlib.Analysis.Normed.Field.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.Data.Countable.Defs public import Mathlib.Data.ENNReal.Basic public import Mathlib.Data.ENNReal.Real public import Mathlib.Data.Finite.Defs public import Mathlib.Data.Finset.Defs public import Mathlib.Data.Fintype.Basic public import Mathlib.Data.Fintype.BigOperators public import Mathlib.Data.Fintype.Card public import Mathlib.Data.Fintype.Defs public import Mathlib.Data.Fintype.EquivFin public import Mathlib.Data.Fintype.Prod public import Mathlib.Data.Fintype.Sets public import Mathlib.Data.FunLike.Basic public import Mathlib.Data.FunLike.Equiv 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.SProd public import Mathlib.Data.Set.Basic public import Mathlib.Data.Set.BooleanAlgebra 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.Range public import Mathlib.Data.Set.Image public import Mathlib.Data.Set.Insert public import Mathlib.Data.Set.Operations public import Mathlib.Data.SetLike.Basic public import Mathlib.Data.Subtype public import Mathlib.Logic.Basic public import Mathlib.Logic.Embedding.Basic public import Mathlib.Logic.Equiv.Defs public import Mathlib.Logic.IsEmpty.Basic public import Mathlib.Logic.IsEmpty.Defs public import Mathlib.Logic.Unique public import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic public import Mathlib.MeasureTheory.Constructions.BorelSpace.Metric 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.Integral.Lebesgue.Map public import Mathlib.MeasureTheory.MeasurableSpace.Basic public import Mathlib.MeasureTheory.MeasurableSpace.Constructions public import Mathlib.MeasureTheory.MeasurableSpace.Defs public import Mathlib.MeasureTheory.MeasurableSpace.Instances public import Mathlib.MeasureTheory.Measure.AEMeasurable 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.Prod public import Mathlib.MeasureTheory.Measure.Regular public import Mathlib.MeasureTheory.Measure.Typeclasses.Finite public import Mathlib.MeasureTheory.Measure.Typeclasses.Probability public import Mathlib.MeasureTheory.OuterMeasure.AE public import Mathlib.Order.Basic public import Mathlib.Order.BourbakiWitt public import Mathlib.Order.CompleteBooleanAlgebra public import Mathlib.Order.Defs.LinearOrder public import Mathlib.Order.Defs.PartialOrder public import Mathlib.Order.Filter.Basic public import Mathlib.Order.Filter.Defs public import Mathlib.Order.Lattice public import Mathlib.Order.SetNotation public import Mathlib.Probability.ConditionalProbability public import Mathlib.Tactic.NormNum.Basic public import Mathlib.Tactic.NormNum.Result 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.SigmaCompact public import Mathlib.Topology.Defs.Filter 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.Pseudo.Basic public import Mathlib.Topology.MetricSpace.Pseudo.Defs public import Mathlib.Topology.Metrizable.Basic 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 Toolkit.Foundations.MeasureTheory.Wasserstein /-! # Finite quantization of measures on compact metric spaces Finite quantization approximates a law on a compact metric space by finitely many atoms. This module provides: * reconstruction of a probability measure carried by a finite set as a weighted sum of Dirac measures (a specialization of Causalean's finite-atomic decomposition); * for every tolerance, a measurable map with finite range moving every point by at most that tolerance (its fibers form a measurable finite partition); * probability laws concentrated on the fibers of a finite measurable map whose mixture recovers the measure, including on fibers of zero mass; * the one-Wasserstein and Lipschitz-contrast bounds for quantization: the quantized law is within the tolerance in one-Wasserstein cost, any coupling of quantized laws lifts to the original laws at an extra cost of twice the tolerance, and Lipschitz contrasts move by at most twice the tolerance. The lifting is specific to deterministic finite quantization, not a general gluing theorem for couplings. -/ public section namespace Toolkit.Foundations.MeasureTheory open _root_.MeasureTheory open scoped BigOperators ENNReal section FiniteCarrier variable {X : Type*} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] /-- [A probability measure](hyp:hμ) giving [full mass to a finite set](hyp:hs) is [the sum, over the points of that set, of each point's mass times the Dirac measure at that point](goal). -/ theorem measure_eq_sum_dirac_of_finite_carrier (μ : Measure X) [hμ : IsProbabilityMeasure μ] (s : Finset X) (hs : μ (s : Set X) = 1) : μ = ∑ i : s, μ {i.val} • Measure.dirac i.val := by classical let cell : s ↪ X := ⟨Subtype.val, Subtype.val_injective⟩ apply Causalean.Mathlib.MeasureTheory.measure_eq_fin_sum_smul_dirac_of_range μ cell (fun _ => measurableSet_singleton _) simpa [cell] using hs end FiniteCarrier section Partition variable {X : Type*} [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] /-- For [every positive tolerance](hyp:hε), [a compact metric space admits a measurable self-map with finitely many values that moves each point by at most that tolerance](goal). The fibers of such a map form a measurable finite partition whose cells have diameter at most twice the tolerance. -/ theorem exists_measurable_finite_quantization {ε : ℝ} (hε : 0 < ε) : ∃ q : X → X, Measurable q ∧ (Set.range q).Finite ∧ ∀ x, dist x (q x) ≤ ε := by classical cases isEmpty_or_nonempty X with | inl hX => exact ⟨id, measurable_id, Set.finite_empty.subset (by simp), fun x => isEmptyElim x⟩ | inr hX => obtain ⟨t, _, ht, hcover⟩ := (isCompact_univ : IsCompact (Set.univ : Set X)).finite_cover_balls hε let := ht.fintype have hhit (x : X) : ∃ y : t, dist x y < ε := by have hx := hcover (Set.mem_univ x) simp only [Set.mem_iUnion] at hx obtain ⟨y, hy, hxy⟩ := hx exact ⟨⟨y, hy⟩, Metric.mem_ball.mp hxy⟩ have : Nonempty t := ⟨(hhit (Classical.choice hX)).choose⟩ let e := Fintype.equivFin t let center : Fin (Fintype.card t) → X := fun i => (e.symm i).val obtain ⟨select, hmeas, hselect⟩ := Causalean.Stat.Minimax.FiniteSideInformation.exists_measurable_finiteCoverSelector (Fintype.card t) Fintype.card_pos center (fun _ => ε) (fun _ => hε) refine ⟨center ∘ select, (measurable_of_finite center).comp hmeas, (Set.finite_range center).subset (Set.range_comp_subset_range _ _), ?_⟩ intro x apply le_of_lt (hselect x ?_) obtain ⟨y, hy⟩ := hhit x exact ⟨e y, by simpa [center] using hy⟩ end Partition section Fibers /-- For [a probability measure](hyp:hμ) and [a measurable map](hyp:q,hq) [onto a finite set](hyp:hqsurj), [there are probability laws, one per value and each concentrated on the fiber of that value, whose mixture weighted by the fiber probabilities recovers the original measure](goal). On fibers of positive mass these are the conditional laws; on fibers of zero mass a Dirac law at a point of the fiber is used. -/ theorem exists_finite_fiber_probabilities {Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι] [MeasurableSpace ι] [MeasurableSingletonClass ι] (μ : Measure Ω) [hμ : IsProbabilityMeasure μ] (q : Ω → ι) (hq : Measurable q) (hqsurj : Function.Surjective q) : ∃ ρ : ι → Measure Ω, (∀ i, IsProbabilityMeasure (ρ i)) ∧ (∀ i, ∀ᵐ x ∂ρ i, q x = i) ∧ μ = ∑ i, μ (q ⁻¹' {i}) • ρ i := by classical let ρ : ι → Measure Ω := fun i => if μ (q ⁻¹' {i}) = 0 then Measure.dirac (hqsurj i).choose else ProbabilityTheory.cond μ (q ⁻¹' {i}) refine ⟨ρ, ?_, ?_, ?_⟩ · intro i by_cases hi : μ (q ⁻¹' {i}) = 0 · simpa [ρ, hi] using (inferInstance : IsProbabilityMeasure (Measure.dirac (hqsurj i).choose)) · simpa [ρ, hi] using ProbabilityTheory.cond_isProbabilityMeasure hi · intro i have hf : MeasurableSet (q ⁻¹' {i}) := hq (measurableSet_singleton i) by_cases hi : μ (q ⁻¹' {i}) = 0 · simp only [ρ, if_pos hi] exact (ae_dirac_iff hf).2 (hqsurj i).choose_spec · simpa only [ρ, if_neg hi, Set.mem_preimage, Set.mem_singleton_iff] using ProbabilityTheory.ae_cond_mem (μ := μ) hf · calc μ = ∑ i, μ (q ⁻¹' {i}) • ProbabilityTheory.cond μ (q ⁻¹' {i}) := (ProbabilityTheory.sum_meas_smul_cond_fiber hq μ).symm _ = ∑ i, μ (q ⁻¹' {i}) • ρ i := by apply Finset.sum_congr rfl intro i _ by_cases hi : μ (q ⁻¹' {i}) = 0 <;> simp [ρ, hi] end Fibers section Transport variable {X : Type*} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] /-- Under [a probability measure](hyp:hμ), [a measurable quantizer](hyp:q,hq) that [moves every point by at most a given tolerance](hyp:hmesh) yields [a coupling of the measure with its quantized image, namely the law of a point paired with its quantization, whose expected distance is at most that tolerance](goal). -/ theorem quantization_graph_coupling (μ : Measure X) [hμ : IsProbabilityMeasure μ] (q : X → X) (hq : Measurable q) {ε : ℝ} (hmesh : ∀ x, dist x (q x) ≤ ε) : Causalean.Stat.IsCoupling (μ.map (fun x => (x, q x))) μ (μ.map q) ∧ (∫⁻ z, edist z.1 z.2 ∂(μ.map (fun x => (x, q x)))) ≤ ENNReal.ofReal ε := by have hg : Measurable (fun x => (x, q x)) := measurable_id.prodMk hq refine ⟨⟨Measure.isProbabilityMeasure_map hg.aemeasurable, ?_, ?_⟩, ?_⟩ · rw [Measure.map_map measurable_fst hg] rw [show Prod.fst ∘ (fun x => (x, q x)) = id from by funext x; rfl] exact Measure.map_id · rw [Measure.map_map measurable_snd hg] rfl · rw [lintegral_map (measurable_fst.edist measurable_snd) hg] calc (∫⁻ x, edist x (q x) ∂μ) ≤ ∫⁻ _, ENNReal.ofReal ε ∂μ := lintegral_mono fun x => by rw [edist_dist] exact ENNReal.ofReal_le_ofReal (hmesh x) _ = ENNReal.ofReal ε := by simp /-- Under [a probability measure](hyp:hμ), [a measurable quantizer](hyp:q,hq) that [moves every point by at most a given tolerance](hyp:hmesh) produces [a quantized law within that tolerance of the original measure in one-Wasserstein cost](goal). -/ theorem wasserstein1_quantization_le (μ : Measure X) [hμ : IsProbabilityMeasure μ] (q : X → X) (hq : Measurable q) {ε : ℝ} (hmesh : ∀ x, dist x (q x) ≤ ε) : wasserstein1 μ (μ.map q) ≤ ENNReal.ofReal ε := by obtain ⟨hcoupling, hcost⟩ := quantization_graph_coupling μ q hq hmesh exact (wasserstein1_le_cost hcoupling).trans hcost /-- For [two probability measures](hyp:hμ,hν), [measurable quantizers with finitely many values](hyp:q,r,hq,hr,hqfinite,hrfinite) that [move each point by at most a nonnegative tolerance](hyp:hε,hqmesh,hrmesh), and [any coupling of the two quantized laws](hyp:hθ), [there is a coupling of the original measures whose expected distance is at most that of the quantized coupling plus twice the tolerance](goal). -/ theorem lift_quantized_coupling (μ ν : Measure X) [hμ : IsProbabilityMeasure μ] [hν : IsProbabilityMeasure ν] (q r : X → X) (hq : Measurable q) (hr : Measurable r) (hqfinite : (Set.range q).Finite) (hrfinite : (Set.range r).Finite) {ε : ℝ} (hε : 0 ≤ ε) (hqmesh : ∀ x, dist x (q x) ≤ ε) (hrmesh : ∀ x, dist x (r x) ≤ ε) {θ : Measure (X × X)} (hθ : Causalean.Stat.IsCoupling θ (μ.map q) (ν.map r)) : ∃ π : Measure (X × X), Causalean.Stat.IsCoupling π μ ν ∧ (∫⁻ z, edist z.1 z.2 ∂π) ≤ (∫⁻ z, edist z.1 z.2 ∂θ) + ENNReal.ofReal (2 * ε) := by classical -- Taking the ranges as codomains makes both finite quantizers surjective. let I := Set.range q let J := Set.range r let : Fintype I := hqfinite.fintype let : Fintype J := hrfinite.fintype let Q : X → I := fun x => ⟨q x, Set.mem_range_self x⟩ let R : X → J := fun x => ⟨r x, Set.mem_range_self x⟩ have hQ : Measurable Q := hq.subtype_mk have hR : Measurable R := hr.subtype_mk have hQsurj : Function.Surjective Q := by rintro ⟨i, x, rfl⟩ exact ⟨x, rfl⟩ have hRsurj : Function.Surjective R := by rintro ⟨j, x, rfl⟩ exact ⟨x, rfl⟩ obtain ⟨ρ, hρ, hρfiber, hμsum⟩ := exists_finite_fiber_probabilities μ Q hQ hQsurj obtain ⟨σ, hσ, hσfiber, hνsum⟩ := exists_finite_fiber_probabilities ν R hR hRsurj let a : I → ℝ≥0∞ := fun i => μ (Q ⁻¹' {i}) let b : J → ℝ≥0∞ := fun j => ν (R ⁻¹' {j}) let p : I → J → ℝ≥0∞ := fun i j => θ {(i.val, j.val)} let : IsProbabilityMeasure θ := hθ.isProbabilityMeasure -- The marginals concentrate the atomic coupling on the product of the ranges. have hθq : ∀ᵐ z ∂θ, z.1 ∈ Set.range q := by apply ae_of_ae_map measurable_fst.aemeasurable rw [hθ.map_fst] exact (ae_map_iff hq.aemeasurable hqfinite.measurableSet).2 (Filter.Eventually.of_forall fun x => Set.mem_range_self x) have hθr : ∀ᵐ z ∂θ, z.2 ∈ Set.range r := by apply ae_of_ae_map measurable_snd.aemeasurable rw [hθ.map_snd] exact (ae_map_iff hr.aemeasurable hrfinite.measurableSet).2 (Filter.Eventually.of_forall fun x => Set.mem_range_self x) let cell : I × J ↪ X × X := ⟨fun ij => (ij.1.val, ij.2.val), by intro x y h exact Prod.ext (Subtype.ext (congrArg Prod.fst h)) (Subtype.ext (congrArg Prod.snd h))⟩ have hcellrange : Set.range cell = Set.range q ×ˢ Set.range r := by ext z constructor · rintro ⟨⟨i, j⟩, rfl⟩ exact ⟨i.property, j.property⟩ · rintro ⟨hi, hj⟩ exact ⟨(⟨z.1, hi⟩, ⟨z.2, hj⟩), rfl⟩ have hθsupport : θ (Set.range cell) = θ Set.univ := by rw [hcellrange, measure_univ] apply (mem_ae_iff_prob_eq_one (hqfinite.measurableSet.prod hrfinite.measurableSet)).1 filter_upwards [hθq, hθr] with z hzq hzr exact ⟨hzq, hzr⟩ have hθsum : θ = ∑ i, ∑ j, p i j • Measure.dirac (i.val, j.val) := by have hh := Causalean.Mathlib.MeasureTheory.measure_eq_fin_sum_smul_dirac_of_range θ cell (fun _ => measurableSet_singleton _) hθsupport rw [Fintype.sum_prod_type] at hh exact hh -- Evaluate each marginal on a singleton to recover the matrix sums. have hrow : ∀ i, ∑ j, p i j = a i := by intro i have hh := congrArg (fun m : Measure X => m {i.val}) hθ.map_fst rw [hθsum] at hh simp only [Measure.map_finset_sum measurable_fst.aemeasurable, Measure.map_smul, Measure.map_dirac' measurable_fst] at hh rw [Measure.map_apply hq (measurableSet_singleton _)] at hh have hf : q ⁻¹' {i.val} = Q ⁻¹' {i} := by ext x simp only [Set.mem_preimage, Set.mem_singleton_iff] exact (Subtype.ext_iff (a1 := Q x) (a2 := i)).symm rw [hf] at hh simpa [Measure.finsetSum_apply, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply', Set.indicator, Subtype.coe_inj, a] using hh have hcol : ∀ j, ∑ i, p i j = b j := by intro j have hh := congrArg (fun m : Measure X => m {j.val}) hθ.map_snd rw [hθsum] at hh simp only [Measure.map_finset_sum measurable_snd.aemeasurable, Measure.map_smul, Measure.map_dirac' measurable_snd] at hh rw [Measure.map_apply hr (measurableSet_singleton _)] at hh have hf : r ⁻¹' {j.val} = R ⁻¹' {j} := by ext x simp only [Set.mem_preimage, Set.mem_singleton_iff] exact (Subtype.ext_iff (a1 := R x) (a2 := j)).symm rw [hf] at hh rw [Finset.sum_comm] at hh simpa [Measure.finsetSum_apply, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply', Set.indicator, Subtype.coe_inj, b] using hh let (i : I) : IsProbabilityMeasure (ρ i) := hρ i let (j : J) : IsProbabilityMeasure (σ j) := hσ j have ha : ∑ i, a i = 1 := by have hh := congrArg (fun m : Measure X => m Set.univ) hμsum simpa [Measure.finsetSum_apply, Measure.smul_apply, smul_eq_mul, a] using hh.symm have hp : ∑ i, ∑ j, p i j = 1 := by simp_rw [hrow]; exact ha refine ⟨∑ i, ∑ j, p i j • (ρ i).prod (σ j), ?_, ?_⟩ · simpa only [a, b, ← hμsum, ← hνsum] using finite_product_mixture_coupling ρ σ hρ hσ a b p ha hrow hcol · have hc : ∀ i j, (∫⁻ z, edist z.1 z.2 ∂(ρ i).prod (σ j)) ≤ edist i.val j.val + ENNReal.ofReal (2 * ε) := by intro i j apply lintegral_edist_prod_le_of_ae_dist_le (ρ i) (σ j) i.val j.val hε · filter_upwards [hρfiber i] with x hx have hx' : q x = i.val := congrArg Subtype.val hx simpa only [hx'] using hqmesh x · filter_upwards [hσfiber j] with x hx have hx' : r x = j.val := congrArg Subtype.val hx simpa only [hx'] using hrmesh x -- Atomic reconstruction identifies the reference-distance part of the cost. have hcost : (∫⁻ z, edist z.1 z.2 ∂θ) = ∑ i, ∑ j, p i j * edist i.val j.val := by rw [hθsum] simp [lintegral_finsetSum_measure, lintegral_smul_measure, smul_eq_mul, lintegral_dirac] simp only [lintegral_finsetSum_measure, lintegral_smul_measure, smul_eq_mul] calc (∑ i, ∑ j, p i j * ∫⁻ z, edist z.1 z.2 ∂(ρ i).prod (σ j)) ≤ ∑ i, ∑ j, p i j * (edist i.val j.val + ENNReal.ofReal (2 * ε)) := by apply Finset.sum_le_sum intro i _ apply Finset.sum_le_sum intro j _ gcongr exact hc i j _ = (∑ i, ∑ j, p i j * edist i.val j.val) + ENNReal.ofReal (2 * ε) := by simp_rw [mul_add, Finset.sum_add_distrib] simp_rw [← Finset.sum_mul] rw [hp, one_mul] _ = (∫⁻ z, edist z.1 z.2 ∂θ) + ENNReal.ofReal (2 * ε) := by rw [hcost] omit [SecondCountableTopology X] in /-- For [two probability measures](hyp:hμ,hν) on [a compact metric space](hyp:hcompact), [a measurable quantizer](hyp:q,hq) that [moves each point by at most a given tolerance](hyp:hmesh) changes [the expectation contrast of any one-Lipschitz function](hyp:hf) by [at most twice that tolerance](goal). -/ theorem lipschitzContrast_quantization_bound [hcompact : CompactSpace X] (μ ν : Measure X) [hμ : IsProbabilityMeasure μ] [hν : IsProbabilityMeasure ν] (q : X → X) (hq : Measurable q) {ε : ℝ} (hmesh : ∀ x, dist x (q x) ≤ ε) {f : X → ℝ} (hf : LipschitzWith 1 f) : |lipschitzContrast μ ν f - lipschitzContrast (μ.map q) (ν.map q) f| ≤ 2 * ε := by have hchange : ∀ (ρ : Measure X) [IsProbabilityMeasure ρ], |(∫ x, f x ∂ρ) - ∫ x, f x ∂(ρ.map q)| ≤ ε := by intro ρ hρ have : IsProbabilityMeasure (ρ.map q) := Measure.isProbabilityMeasure_map hq.aemeasurable have hfρ : Integrable f ρ := hf.continuous.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace f) have hfq : Integrable f (ρ.map q) := hf.continuous.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace f) rw [integral_map hq.aemeasurable hfq.aestronglyMeasurable] have hfcomp : Integrable (fun x => f (q x)) ρ := by simpa only [Function.comp_def] using hfq.comp_measurable hq rw [← integral_sub hfρ hfcomp] have hb : ∀ᵐ x ∂ρ, ‖f x - f (q x)‖ ≤ ε := by filter_upwards [] with x calc ‖f x - f (q x)‖ ≤ dist x (q x) := by simpa only [Real.norm_eq_abs, ← Real.dist_eq, NNReal.coe_one, one_mul] using hf.dist_le_mul x (q x) _ ≤ ε := hmesh x simpa [Real.norm_eq_abs, measureReal_def] using norm_integral_le_of_norm_le_const hb unfold lipschitzContrast calc |(∫ x, f x ∂μ) - (∫ x, f x ∂ν) - ((∫ x, f x ∂(μ.map q)) - ∫ x, f x ∂(ν.map q))| = |((∫ x, f x ∂μ) - ∫ x, f x ∂(μ.map q)) - ((∫ x, f x ∂ν) - ∫ x, f x ∂(ν.map q))| := by congr 1; ring _ ≤ |(∫ x, f x ∂μ) - ∫ x, f x ∂(μ.map q)| + |(∫ x, f x ∂ν) - ∫ x, f x ∂(ν.map q)| := abs_sub _ _ _ ≤ ε + ε := add_le_add (hchange μ) (hchange ν) _ = 2 * ε := by ring end Transport end Toolkit.Foundations.MeasureTheory