Wasserstein.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.wasserstein2_nonneg line 15
Source documentation
The real-valued transport distance is nonnegative.
```
theorem wasserstein2_nonneg (μ ν : Measure (E d)) :
    0 ≤ wasserstein2 μ ν :=
…
```

theorem OAI.Problem358.wasserstein2_le_of_coupling line 20

Source documentation

Any finite-cost coupling supplies an upper bound for the transport distance.

theorem wasserstein2_le_of_coupling {μ ν : Measure (E d)}
    {π : Measure (E d × E d)} (hπ : IsCoupling μ ν π)
    (hfin : quadraticPlanCost π ≠ ∞) :
    wasserstein2 μ ν ≤ Real.sqrt (quadraticPlanCost π).toReal := by
…

theorem OAI.Problem358.wasserstein2_eq_of_minimizing_coupling line 29

Source documentation

A coupling which minimizes the extended cost computes the defined distance.

theorem wasserstein2_eq_of_minimizing_coupling {μ ν : Measure (E d)}
    {π : Measure (E d × E d)} (hπ : IsCoupling μ ν π)
    (hmin : ∀ π', IsCoupling μ ν π' → quadraticPlanCost π ≤ quadraticPlanCost π') :
    wasserstein2 μ ν = Real.sqrt (quadraticPlanCost π).toReal := by
…

theorem OAI.Problem358.swap_isCoupling line 43

theorem OAI.Problem358.quadraticPlanCost_swap line 54

Source documentation

Swapping both variables in a plan preserves quadratic cost.

theorem quadraticPlanCost_swap (π : Measure (E d × E d)) :
    quadraticPlanCost (π.map Prod.swap) = quadraticPlanCost π := by
…

theorem OAI.Problem358.wasserstein2_symm line 64
Source documentation
The transport distance is symmetric, including for arbitrary input measures.
```
theorem wasserstein2_symm (μ ν : Measure (E d)) :
    wasserstein2 μ ν = wasserstein2 ν μ := by
…
```
theorem OAI.Problem358.wasserstein2_self line 80
Source documentation
Every probability measure has zero distance from itself.
```
theorem wasserstein2_self (μ : Measure (E d)) [IsProbabilityMeasure μ] :
    wasserstein2 μ μ = 0 := by
…
```

theorem OAI.Problem358.exists_coupling_sqrt_cost_lt line 103

Source documentation

The infimum defining wasserstein2 can be approximated by finite-cost plans. This does not require existence of an optimal coupling.

theorem exists_coupling_sqrt_cost_lt {μ ν : Measure (E d)}
    {π₀ : Measure (E d × E d)} (hπ₀ : IsCoupling μ ν π₀)
    (hfinite : quadraticPlanCost π₀ ≠ ∞) {ε : ℝ} (hε : 0 < ε) :
    ∃ π : Measure (E d × E d), IsCoupling μ ν π ∧
      quadraticPlanCost π ≠ ∞ ∧
      Real.sqrt (quadraticPlanCost π).toReal < wasserstein2 μ ν + ε := by
…

lemma OAI.Problem358.coordinate_sq_le_norm_sq line 131
Source documentation
A single Euclidean coordinate is dominated by the Euclidean norm.
```
lemma coordinate_sq_le_norm_sq {d : ℕ} (x : E d) (j : Fin d) :
    (x j) ^ 2 ≤ ‖x‖ ^ 2 := by
…
```
lemma OAI.Problem358.coordinate_sq_le_displacement_sq line 138
Source documentation
If the source coordinate vanishes, displacement controls the target coordinate.
```
lemma coordinate_sq_le_displacement_sq {d : ℕ} (x y : E d) (j : Fin d)
    (hx : x j = 0) :
    (y j) ^ 2 ≤ ‖x - y‖ ^ 2 := by
…
```

lemma OAI.Problem358.coordinate_moment_le_quadraticPlanCost line 145

Source documentation

Every coupling pays at least the target coordinate second moment when the source is concentrated on the zero coordinate hyperplane.

lemma coordinate_moment_le_quadraticPlanCost {d : ℕ}
    {μ ν : Measure (E d)} {π : Measure (E d × E d)} (j : Fin d)
    (hμ : ∀ᵐ x ∂μ, x j = 0) (hπ : IsCoupling μ ν π) :
    (∫⁻ y, ENNReal.ofReal ((y j) ^ 2) ∂ν) ≤ quadraticPlanCost π := by
…

lemma OAI.Problem358.coordinate_moment_le_sInf_cost line 159

Source documentation

The same lower bound passes to the infimum of all coupling costs.

lemma coordinate_moment_le_sInf_cost {d : ℕ}
    {μ ν : Measure (E d)} (j : Fin d) (hμ : ∀ᵐ x ∂μ, x j = 0) :
    (∫⁻ y, ENNReal.ofReal ((y j) ^ 2) ∂ν) ≤
      sInf {r : ℝ≥0∞ | ∃ π : Measure (E d × E d),
        IsCoupling μ ν π ∧ quadraticPlanCost π = r} := by
…

lemma OAI.Problem358.sqrt_coordinate_moment_le_wasserstein2 line 171

Source documentation

A finite-cost coupling makes the coordinate-moment bound valid after taking toReal and square roots. The finiteness hypothesis is essential because ENNReal.toReal ∞ = 0.

lemma sqrt_coordinate_moment_le_wasserstein2 {d : ℕ}
    {μ ν : Measure (E d)} {π : Measure (E d × E d)} (j : Fin d)
    (hμ : ∀ᵐ x ∂μ, x j = 0) (hπ : IsCoupling μ ν π)
    (hfinite : quadraticPlanCost π < ∞) :
    Real.sqrt (ENNReal.toReal (∫⁻ y, ENNReal.ofReal ((y j) ^ 2) ∂ν)) ≤
      wasserstein2 μ ν := by
…

lemma OAI.Problem358.wasserstein2_eq_sqrt_coordinate_moment line 186

Source documentation

A coupling attaining the coordinate lower bound computes the Wasserstein quantity exactly; in particular this applies to the central-atom matching plan.

lemma wasserstein2_eq_sqrt_coordinate_moment {d : ℕ}
    {μ ν : Measure (E d)} {π : Measure (E d × E d)} (j : Fin d)
    (hμ : ∀ᵐ x ∂μ, x j = 0) (hπ : IsCoupling μ ν π)
    (hcost : quadraticPlanCost π = ∫⁻ y, ENNReal.ofReal ((y j) ^ 2) ∂ν) :
    wasserstein2 μ ν =
      Real.sqrt (ENNReal.toReal (∫⁻ y, ENNReal.ofReal ((y j) ^ 2) ∂ν)) := by
…

lemma OAI.Problem358.wasserstein2_pos_of_coordinate_moment_pos line 200

Source documentation

A positive target coordinate moment separates the measures in Wasserstein quantity whenever a finite-cost coupling exists.

lemma wasserstein2_pos_of_coordinate_moment_pos {d : ℕ}
    {μ ν : Measure (E d)} {π : Measure (E d × E d)} (j : Fin d)
    (hμ : ∀ᵐ x ∂μ, x j = 0) (hπ : IsCoupling μ ν π)
    (hfinite : quadraticPlanCost π < ∞)
    (hpos : 0 < ∫⁻ y, ENNReal.ofReal ((y j) ^ 2) ∂ν) :
    0 < wasserstein2 μ ν := by
…

theorem OAI.Problem358.testing_integral_sq_le line 224

Source documentation

The second-moment inequality for a real random variable on a probability space.

theorem testing_integral_sq_le {X : Type*} [MeasurableSpace X]
    {ρ : Measure X} [IsProbabilityMeasure ρ] {f : X → ℝ} (hf : MemLp f 2 ρ) :
    (∫ x, f x ∂ρ) ^ 2 ≤ ∫ x, (f x) ^ 2 ∂ρ := by
…

theorem OAI.Problem358.integral_test_le_sqrt_cost line 232

Source documentation

A finite-cost coupling controls the difference of Lipschitz test integrals.

theorem integral_test_le_sqrt_cost {d : ℕ} {μ ν : Measure (E d)}
    {π : Measure (E d × E d)} (hπ : IsCoupling μ ν π)
    (hc : quadraticPlanCost π ≠ ∞) {L : ℝ≥0} {f : E d → ℝ}
    (hf : LipschitzWith L f) (hfμ : Integrable f μ) (hfν : Integrable f ν) :
    |(∫ x, f x ∂μ) - ∫ y, f y ∂ν| ≤
      L * Real.sqrt (quadraticPlanCost π).toReal := by
…

theorem OAI.Problem358.testing_sqrt_sInf_bound line 266

Source documentation

A nonnegative square-root lower bound passes to the infimum of extended costs.

theorem testing_sqrt_sInf_bound (S : Set ℝ≥0∞)
    (hfinite : ∃ r ∈ S, r ≠ ∞) {D L : ℝ} (hD : 0 ≤ D) (hL : 0 ≤ L)
    (hbound : ∀ r ∈ S, r ≠ ∞ → D ≤ L * Real.sqrt r.toReal) :
    D ≤ L * Real.sqrt (sInf S).toReal := by
…

theorem OAI.Problem358.integral_test_le_wasserstein2 line 292

Source documentation

Lipschitz testing is controlled by the problem's Wasserstein distance whenever a finite-cost coupling exists. Compact support is not required in this interface.

theorem integral_test_le_wasserstein2 {d : ℕ} {μ ν : Measure (E d)}
    (hfinite : ∃ π : Measure (E d × E d),
      IsCoupling μ ν π ∧ quadraticPlanCost π ≠ ∞)
    {L : ℝ≥0} {f : E d → ℝ} (hf : LipschitzWith L f)
    (hfμ : Integrable f μ) (hfν : Integrable f ν) :
    |(∫ x, f x ∂μ) - ∫ y, f y ∂ν| ≤ L * wasserstein2 μ ν := by
…

theorem OAI.Problem358.integral_test_eq_of_wasserstein2_eq_zero line 307

Source documentation

A zero-Wasserstein pair agrees on every integrable Lipschitz test.

theorem integral_test_eq_of_wasserstein2_eq_zero {d : ℕ} {μ ν : Measure (E d)}
    (hfinite : ∃ π : Measure (E d × E d),
      IsCoupling μ ν π ∧ quadraticPlanCost π ≠ ∞)
    (hzero : wasserstein2 μ ν = 0) {L : ℝ≥0} {f : E d → ℝ}
    (hf : LipschitzWith L f) (hfμ : Integrable f μ) (hfν : Integrable f ν) :
    (∫ x, f x ∂μ) = ∫ y, f y ∂ν := by
…

theorem OAI.Problem358.tendsto_probabilityMeasure_of_wasserstein2_tendsto_zero line 318

Source documentation

Wasserstein convergence with finite-cost couplings implies weak convergence.

theorem tendsto_probabilityMeasure_of_wasserstein2_tendsto_zero
    {d : ℕ} {ι : Type*} {l : Filter ι} [l.IsCountablyGenerated]
    {μs : ι → ProbabilityMeasure (E d)} {ν : ProbabilityMeasure (E d)}
    (hfinite : ∀ i, ∃ π : Measure (E d × E d),
      IsCoupling (μs i : Measure (E d)) (ν : Measure (E d)) π ∧ quadraticPlanCost π ≠ ∞)
    (hW : Tendsto (fun i => wasserstein2 (μs i : Measure (E d)) (ν : Measure (E d))) l (𝓝 0)) :
    Tendsto μs l (𝓝 ν) := by
…

theorem OAI.Problem358.measure_eq_of_wasserstein2_eq_zero line 343

Source documentation

Finite-cost probability measures at zero Wasserstein distance are equal.

theorem measure_eq_of_wasserstein2_eq_zero {d : ℕ} {μ ν : Measure (E d)}
    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (hfinite : ∃ π : Measure (E d × E d),
      IsCoupling μ ν π ∧ quadraticPlanCost π ≠ ∞)
    (hzero : wasserstein2 μ ν = 0) : μ = ν := by
…

theorem OAI.Problem358.wasserstein2_pos_of_ne_of_finite_coupling line 359

Source documentation

Distinct probabilities with a finite-cost coupling have positive Wasserstein distance.

theorem wasserstein2_pos_of_ne_of_finite_coupling {d : ℕ} {μ ν : Measure (E d)}
    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (hfinite : ∃ π : Measure (E d × E d),
      IsCoupling μ ν π ∧ quadraticPlanCost π ≠ ∞) (hne : μ ≠ ν) :
    0 < wasserstein2 μ ν := by
…

theorem OAI.Problem358.le_of_le_all_coupling_sqrt_cost line 383

Source documentation

A continuous nondecreasing function of root cost commutes with the transport infimum for purposes of universal lower estimates. No minimizing plan is required.

theorem le_of_le_all_coupling_sqrt_cost {μ ν : Measure (E d)}
    {π₀ : Measure (E d × E d)} (hπ₀ : IsCoupling μ ν π₀)
    (hfinite : quadraticPlanCost π₀ ≠ ∞) {F : ℝ → ℝ}
    (hmono : MonotoneOn F (Set.Ici 0))
    (hcont : ContinuousAt F (wasserstein2 μ ν)) {a : ℝ}
    (hbound : ∀ π : Measure (E d × E d), IsCoupling μ ν π →
      quadraticPlanCost π ≠ ∞ → a ≤ F (Real.sqrt (quadraticPlanCost π).toReal)) :
    a ≤ F (wasserstein2 μ ν) := by
…

theorem OAI.Problem358.le_mul_rpow_wasserstein2_of_coupling_bound line 406

Source documentation

Power-type estimates valid for every finite-cost coupling descend to the exact transport distance, including at zero distance.

theorem le_mul_rpow_wasserstein2_of_coupling_bound {μ ν : Measure (E d)}
    {π₀ : Measure (E d × E d)} (hπ₀ : IsCoupling μ ν π₀)
    (hfinite : quadraticPlanCost π₀ ≠ ∞) {a C α : ℝ}
    (hC : 0 ≤ C) (hα : 0 ≤ α)
    (hbound : ∀ π : Measure (E d × E d), IsCoupling μ ν π →
      quadraticPlanCost π ≠ ∞ →
      a ≤ C * Real.rpow (Real.sqrt (quadraticPlanCost π).toReal) α) :
    a ≤ C * Real.rpow (wasserstein2 μ ν) α := by
…