FiniteCoupling.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.isCompact_finite_coupling_set line 15

Source documentation

The transportation polytope of two finite real-valued probability vectors is compact.

theorem isCompact_finite_coupling_set
    (a : I → ℝ) (b : J → ℝ)
    (ha : ∀ i, 0 ≤ a i) (hasum : ∑ i, a i = 1) :
    IsCompact {p : I → J → ℝ |
      (∀ i j, 0 ≤ p i j) ∧
      (∀ i, ∑ j, p i j = a i) ∧
      (∀ j, ∑ i, p i j = b j)} := by
…

theorem OAI.Problem358.exists_minimal_finite_coupling line 51

Source documentation

Every finite transportation problem with probability margins has a cost minimizer. No nonnegativity or metric assumptions on the finite cost matrix are needed.

theorem exists_minimal_finite_coupling
    (a : I → ℝ) (b : J → ℝ) (c : I → J → ℝ)
    (ha : ∀ i, 0 ≤ a i) (hb : ∀ j, 0 ≤ b j)
    (hasum : ∑ i, a i = 1) (hbsum : ∑ j, b j = 1) :
    ∃ p : I → J → ℝ,
      (∀ i j, 0 ≤ p i j) ∧
      (∀ i, ∑ j, p i j = a i) ∧
      (∀ j, ∑ i, p i j = b j) ∧
      ∀ q : I → J → ℝ,
        (∀ i j, 0 ≤ q i j) →
        (∀ i, ∑ j, q i j = a i) →
        (∀ j, ∑ i, q i j = b j) →
…

theorem OAI.Problem358.quadratic_swap_identity line 97

Source documentation

The exact decrease in quadratic cost obtained by swapping two target sites.

theorem quadratic_swap_identity (x₀ x₁ y₀ y₁ : V) :
    ‖x₀ - y₁‖ ^ 2 + ‖x₁ - y₀‖ ^ 2 -
      (‖x₀ - y₀‖ ^ 2 + ‖x₁ - y₁‖ ^ 2) =
        2 * ⟪x₀ - x₁, y₀ - y₁⟫_ℝ := by
…

theorem OAI.Problem358.inner_sub_nonneg_of_quadratic_swap line 105

Source documentation

Pairwise optimality of a quadratic matching implies monotonicity.

theorem inner_sub_nonneg_of_quadratic_swap
    (x₀ x₁ y₀ y₁ : V)
    (h : ‖x₀ - y₀‖ ^ 2 + ‖x₁ - y₁‖ ^ 2 ≤
      ‖x₀ - y₁‖ ^ 2 + ‖x₁ - y₀‖ ^ 2) :
    0 ≤ ⟪x₀ - x₁, y₀ - y₁⟫_ℝ := by
…

theorem OAI.Problem358.monotone_interpolation_ne_zero line 114

Source documentation

A monotone pair of displacements cannot cancel at an interior interpolation time.

theorem monotone_interpolation_ne_zero
    (a b : V) (hmono : 0 ≤ ⟪a, b⟫_ℝ)
    (hne : a ≠ 0 ∨ b ≠ 0) {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1) :
    (1 - t) • a + t • b ≠ 0 := by
…

theorem OAI.Problem358.monotone_interpolated_sites_ne line 135

Source documentation

Distinct endpoint pairs in a monotone relation remain distinct at interior times.

theorem monotone_interpolated_sites_ne
    (x₀ x₁ y₀ y₁ : V)
    (hmono : 0 ≤ ⟪x₀ - x₁, y₀ - y₁⟫_ℝ)
    (hne : (x₀, y₀) ≠ (x₁, y₁))
    {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1) :
    (1-t) • x₀ + t • y₀ ≠ (1-t) • x₁ + t • y₁ := by
…

def OAI.Problem358.FiniteCoupling.cost line 167
Source documentation
The cost of a finite real-valued transport matrix.
```
def cost (c w : ι → κ → ℝ) : ℝ := ∑ i, ∑ j, w i j * c i j
```
def OAI.Problem358.FiniteCoupling.IsOptimal line 170
Source documentation
Optimality among nonnegative matrices with the same two marginals.
```
def IsOptimal (c w : ι → κ → ℝ) : Prop :=
…
```
def OAI.Problem358.FiniteCoupling.rectangleSwap line 177
Source documentation
Transfer mass from the diagonal corners to the off-diagonal corners.
```
def rectangleSwap (w : ι → κ → ℝ) (ε : ℝ) (i k : ι) (j l : κ)
    (u : ι) (v : κ) : ℝ :=
…
```
lemma OAI.Problem358.FiniteCoupling.rectangleSwap_row line 183
lemma OAI.Problem358.FiniteCoupling.rectangleSwap_col line 188
lemma OAI.Problem358.FiniteCoupling.rectangleSwap_nonneg line 194
lemma OAI.Problem358.FiniteCoupling.rectangleSwap_cost line 203
lemma OAI.Problem358.FiniteCoupling.IsOptimal.cross_cost_le line 211
Source documentation
The two-point exchange inequality on the positive support of an optimal matrix.
```
lemma IsOptimal.cross_cost_le {c w : ι → κ → ℝ} (hopt : IsOptimal c w)
    {i k : ι} {j l : κ} (hij : 0 < w i j) (hkl : 0 < w k l) :
    c i j + c k l ≤ c i l + c k j := by
…
```
Mentions: OAI.Problem358.FiniteCoupling.IsOptimal

lemma OAI.Problem358.inner_sub_nonneg_of_quadratic_cross line 233

Source documentation

The quadratic exchange inequality is exactly two-point monotonicity.

lemma inner_sub_nonneg_of_quadratic_cross {x x' y y' : F}
    (h : ‖x - y‖ ^ 2 + ‖x' - y'‖ ^ 2 ≤
      ‖x - y'‖ ^ 2 + ‖x' - y‖ ^ 2) :
    0 ≤ ⟪x - x', y - y'⟫ := by
…

lemma OAI.Problem358.FiniteCoupling.IsOptimal.inner_nonneg line 242

Source documentation

Positive entries of a finite quadratic optimal coupling are monotone.

lemma FiniteCoupling.IsOptimal.inner_nonneg
    {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ]
    {x : ι → F} {y : κ → F} {w : ι → κ → ℝ}
    (hopt : FiniteCoupling.IsOptimal (fun i j => ‖x i - y j‖ ^ 2) w)
    {i k : ι} {j l : κ} (hij : 0 < w i j) (hkl : 0 < w k l) :
    0 ≤ ⟪x i - x k, y j - y l⟫ :=
…

Mentions: OAI.Problem358.FiniteCoupling.IsOptimal

lemma OAI.Problem358.eq_zero_of_pos_smul_add_smul_eq_zero line 252
Source documentation
A positive linear combination of two vectors with nonnegative inner product can vanish only when both vectors vanish.
```
lemma eq_zero_of_pos_smul_add_smul_eq_zero {x y : F} {a b : ℝ}
    (ha : 0 < a) (hb : 0 < b) (hxy : 0 ≤ ⟪x, y⟫)
    (h : a • x + b • y = 0) : x = 0 ∧ y = 0 := by
…
```

lemma OAI.Problem358.interpolate_ne_of_inner_nonneg line 268

Source documentation

Distinct endpoint pairs on a monotone relation cannot collide at interior time.

lemma interpolate_ne_of_inner_nonneg {x x' y y' : F} {t : ℝ}
    (ht0 : 0 < t) (ht1 : t < 1)
    (hxy : 0 ≤ ⟪x - x', y - y'⟫) (hne : (x, y) ≠ (x', y')) :
    (1 - t) • x + t • y ≠ (1 - t) • x' + t • y' := by
…

theorem OAI.Problem358.FiniteCoupling.exists_optimal_with_marginals line 298

Source documentation

A finite optimal coupling exists with any prescribed probability marginals.

theorem exists_optimal_with_marginals
    (a : I → ℝ) (b : J → ℝ) (c : I → J → ℝ)
    (ha : ∀ i, 0 ≤ a i) (hb : ∀ j, 0 ≤ b j)
    (hasum : ∑ i, a i = 1) (hbsum : ∑ j, b j = 1) :
    ∃ p : I → J → ℝ,
      (∀ i, ∑ j, p i j = a i) ∧
      (∀ j, ∑ i, p i j = b j) ∧ IsOptimal c p := by
…

Mentions: OAI.Problem358.FiniteCoupling.IsOptimal

theorem OAI.Problem358.FiniteCoupling.IsOptimal.interpolated_support_injective line 317

Source documentation

The positive support of an optimal quadratic finite coupling has distinct interpolated sites at every interior time, even when either endpoint marginal contains repeated images across different coupling pairs.

theorem IsOptimal.interpolated_support_injective
    {x : I → V} {y : J → V} {p : I → J → ℝ}
    (hp : IsOptimal (fun i j => ‖x i - y j‖ ^ 2) p)
    (hx : Function.Injective x) (hy : Function.Injective y)
    {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1) :
    Function.Injective (fun q : {q : I × J // 0 < p q.1 q.2} =>
      (1-t) • x q.val.1 + t • y q.val.2) := by
…

Mentions: OAI.Problem358.FiniteCoupling.IsOptimal

theorem OAI.Problem358.FiniteCoupling.exists_optimal_noncolliding_path line 336

Source documentation

Finite quadratic transport admits a positive-support path with no collisions. This packages the finite compactness and two-point exchange steps together.

theorem exists_optimal_noncolliding_path
    (a : I → ℝ) (b : J → ℝ) (x : I → V) (y : J → V)
    (ha : ∀ i, 0 ≤ a i) (hb : ∀ j, 0 ≤ b j)
    (hasum : ∑ i, a i = 1) (hbsum : ∑ j, b j = 1)
    (hx : Function.Injective x) (hy : Function.Injective y) :
    ∃ p : I → J → ℝ,
      (∀ i, ∑ j, p i j = a i) ∧
      (∀ j, ∑ i, p i j = b j) ∧
      IsOptimal (fun i j => ‖x i - y j‖ ^ 2) p ∧
      ∀ t : ℝ, 0 < t → t < 1 →
        Function.Injective (fun q : {q : I × J // 0 < p q.1 q.2} =>
          (1-t) • x q.val.1 + t • y q.val.2) := by
…

Mentions: OAI.Problem358.FiniteCoupling.IsOptimal

abbrev OAI.Problem358.PositiveFiniteCoupling.Support line 368
Source documentation
Retain only the strictly positive entries of a finite nonnegative weight family.
```
abbrev Support (w : ι → ℝ) := {i : ι // 0 < w i}
```
instance OAI.Problem358.PositiveFiniteCoupling.supportFintype line 370
theorem OAI.Problem358.PositiveFiniteCoupling.sum_support_mul line 374
Source documentation
Removing zero weights preserves every weighted real sum.
```
theorem sum_support_mul (w f : ι → ℝ) (hw : ∀ i, 0 ≤ w i) :
    (∑ i : Support w, w i * f i) = ∑ i, w i * f i := by
…
```
Mentions: OAI.Problem358.PositiveFiniteCoupling.Support
theorem OAI.Problem358.PositiveFiniteCoupling.sum_support line 386
theorem OAI.Problem358.PositiveFiniteCoupling.support_nonempty line 390
abbrev OAI.Problem358.PositiveFiniteCoupling.Pairs line 403
theorem OAI.Problem358.PositiveFiniteCoupling.sum_pairs_mul line 405
theorem OAI.Problem358.PositiveFiniteCoupling.sum_pairs_eq_one line 411

theorem OAI.Problem358.PositiveFiniteCoupling.endpoint_pairs_injective line 423

Source documentation

Injective endpoint site families give distinct positive coupling pairs.

theorem endpoint_pairs_injective {x : ι → F} {y : κ → F}
    (hx : Function.Injective x) (hy : Function.Injective y) (w : ι → κ → ℝ) :
    Function.Injective (fun p : Pairs w => (x p.1.1, y p.1.2)) := by
…

Mentions: OAI.Problem358.PositiveFiniteCoupling.Pairs

theorem OAI.Problem358.PositiveFiniteCoupling.interpolated_sites_injective line 431

Source documentation

The positive pairs of an optimal quadratic matrix remain distinct at interior times.

theorem interpolated_sites_injective [DecidableEq ι] [DecidableEq κ]
    {x : ι → F} {y : κ → F} {w : ι → κ → ℝ}
    (hx : Function.Injective x) (hy : Function.Injective y)
    (hopt : FiniteCoupling.IsOptimal (fun i j => ‖x i - y j‖ ^ 2) w)
    {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1) :
    Function.Injective
      (fun p : Pairs w => (1-t) • x p.1.1 + t • y p.1.2) := by
…

Mentions: OAI.Problem358.FiniteCoupling.IsOptimal, OAI.Problem358.PositiveFiniteCoupling.Pairs

theorem OAI.Problem358.PositiveFiniteCoupling.exists_optimal_positive_pairs line 446

Source documentation

A finite quadratic optimal coupling, with zero entries removed, has positive normalized weights and pairwise distinct interpolated sites for every interior time.

theorem exists_optimal_positive_pairs [DecidableEq ι] [DecidableEq κ]
    (a : ι → ℝ) (b : κ → ℝ) (x : ι → F) (y : κ → F)
    (ha : ∀ i, 0 ≤ a i) (hb : ∀ j, 0 ≤ b j)
    (hasum : ∑ i, a i = 1) (hbsum : ∑ j, b j = 1)
    (hx : Function.Injective x) (hy : Function.Injective y) :
    ∃ w : ι → κ → ℝ,
      (∀ i, ∑ j, w i j = a i) ∧
      (∀ j, ∑ i, w i j = b j) ∧
      FiniteCoupling.IsOptimal (fun i j => ‖x i - y j‖ ^ 2) w ∧
      (∑ p : Pairs w, w p.1.1 p.1.2) = 1 ∧
      ∀ t : ℝ, 0 < t → t < 1 → Function.Injective
        (fun p : Pairs w => (1-t) • x p.1.1 + t • y p.1.2) := by
…

Mentions: OAI.Problem358.FiniteCoupling.IsOptimal, OAI.Problem358.PositiveFiniteCoupling.Pairs