OAI/Analysis/Brenier/AtomicTransport.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.quadraticPlanCost_atomicMatchingPlan_ofReal_toReal line 15

   Source documentation

   Real-valued finite matrix weights have the expected real quadratic cost.

   theorem quadraticPlanCost_atomicMatchingPlan_ofReal_toReal
       {d : ℕ} {ι κ : Type*} [Fintype ι] [Fintype κ]
       (p : ι → κ → ℝ) (hp : ∀ i j, 0 ≤ p i j) (y : ι → E d) (z : κ → E d) :
       (quadraticPlanCost (atomicMatchingPlan
         (fun q : ι × κ => ENNReal.ofReal (p q.1 q.2))
         (fun q => y q.1) (fun q => z q.2))).toReal =
         ∑ i, ∑ j, p i j * ‖y i - z j‖ ^ 2 := by
   …

   Mentions: OAI.Problem358.atomicMatchingPlan

2. theorem OAI.Problem358.atomicMatchingPlan_minimal_of_matrix_minimal line 30

   Source documentation

   Criterion turning any real matrix minimizer into a minimum among arbitrary couplings, without changing the chosen matrix.

   theorem atomicMatchingPlan_minimal_of_matrix_minimal
       {d : ℕ} {ι κ : Type*} [Fintype ι] [Fintype κ]
       (w : ι → ℝ≥0∞) (v : κ → ℝ≥0∞) (y : ι → E d) (z : κ → E d)
       (hy : Function.Injective y) (hz : Function.Injective z)
       (p : ι → κ → ℝ) (hp : ∀ i j, 0 ≤ p i j)
       (hcoupling : IsCoupling (∑ i, w i • Measure.dirac (y i))
         (∑ j, v j • Measure.dirac (z j))
         (atomicMatchingPlan (fun q : ι × κ => ENNReal.ofReal (p q.1 q.2))
           (fun q => y q.1) (fun q => z q.2)))
       (hmin : ∀ q : ι → κ → ℝ, (∀ i j, 0 ≤ q i j) →
         (∀ i, ∑ j, q i j = (w i).toReal) →
         (∀ j, ∑ i, q i j = (v j).toReal) →
   …

   Mentions: OAI.Problem358.atomicMatchingPlan

3. theorem OAI.Problem358.exists_optimal_atomic_matrix line 59

   Source documentation

   A minimizing transportation matrix also minimizes over every measure-valued coupling of the two injectively indexed finite atomic laws.

   theorem exists_optimal_atomic_matrix
       {d : ℕ} {ι κ : Type*} [Fintype ι] [Fintype κ]
       (w : ι → ℝ≥0∞) (v : κ → ℝ≥0∞) (y : ι → E d) (z : κ → E d)
       (hw : ∑ i, w i = 1) (hv : ∑ j, v j = 1)
       (hy : Function.Injective y) (hz : Function.Injective z) :
       ∃ p : ι → κ → ℝ,
         (∀ i j, 0 ≤ p i j) ∧
         (∀ i, ∑ j, p i j = (w i).toReal) ∧
         (∀ j, ∑ i, p i j = (v j).toReal) ∧
         IsCoupling (∑ i, w i • Measure.dirac (y i))
           (∑ j, v j • Measure.dirac (z j))
           (atomicMatchingPlan (fun q : ι × κ => ENNReal.ofReal (p q.1 q.2))
   …

   Mentions: OAI.Problem358.atomicMatchingPlan

4. theorem OAI.Problem358.exists_optimal_atomic_coupling line 107

   Source documentation

   Existence of a globally optimal coupling for two finite atomic probability laws.

   theorem exists_optimal_atomic_coupling
       {d : ℕ} {ι κ : Type*} [Fintype ι] [Fintype κ]
       (w : ι → ℝ≥0∞) (v : κ → ℝ≥0∞) (y : ι → E d) (z : κ → E d)
       (hw : ∑ i, w i = 1) (hv : ∑ j, v j = 1)
       (hy : Function.Injective y) (hz : Function.Injective z) :
       ∃ π, IsCoupling (∑ i, w i • Measure.dirac (y i))
           (∑ j, v j • Measure.dirac (z j)) π ∧
         ∀ σ, IsCoupling (∑ i, w i • Measure.dirac (y i))
             (∑ j, v j • Measure.dirac (z j)) σ →
           quadraticPlanCost π ≤ quadraticPlanCost σ := by
   …

5. theorem OAI.Problem358.wasserstein2_sq_eq_planCost_of_minimal line 121

   Source documentation

   Any actual minimum realizes the infimum in the challenge's Wasserstein definition.

   theorem wasserstein2_sq_eq_planCost_of_minimal {d : ℕ}
       {μ ν : Measure (E d)} {π : Measure (E d × E d)}
       (hπ : IsCoupling μ ν π)
       (hmin : ∀ σ, IsCoupling μ ν σ → quadraticPlanCost π ≤ quadraticPlanCost σ) :
       wasserstein2 μ ν ^ 2 = (quadraticPlanCost π).toReal := by
   …

6. theorem OAI.Problem358.exists_atomic_coupling_matrix_with_wasserstein_cost line 136

   Source documentation

   The finite minimizing matrix has squared speed exactly equal to W₂².

   theorem exists_atomic_coupling_matrix_with_wasserstein_cost
       {d : ℕ} {ι κ : Type*} [Fintype ι] [Fintype κ]
       (w : ι → ℝ≥0∞) (v : κ → ℝ≥0∞) (y : ι → E d) (z : κ → E d)
       (hw : ∑ i, w i = 1) (hv : ∑ j, v j = 1)
       (hy : Function.Injective y) (hz : Function.Injective z) :
       ∃ p : ι → κ → ℝ,
         (∀ i j, 0 ≤ p i j) ∧
         (∀ i, ∑ j, p i j = (w i).toReal) ∧
         (∀ j, ∑ i, p i j = (v j).toReal) ∧
         (∑ i, ∑ j, p i j * ‖y i - z j‖ ^ 2) =
           wasserstein2 (∑ i, w i • Measure.dirac (y i))
             (∑ j, v j • Measure.dirac (z j)) ^ 2 := by
   …

7. theorem OAI.Problem358.sum_ofReal_smul_positive_support line 159

   Source documentation

   Removing the zero weights also preserves finite sums of weighted measures.

   theorem sum_ofReal_smul_positive_support {X ι : Type*} [MeasurableSpace X] [Fintype ι]
       (w : ι → ℝ) (μ : ι → Measure X) (hw : ∀ i, 0 ≤ w i) :
       (∑ i : PositiveFiniteCoupling.Support w, ENNReal.ofReal (w i) • μ i) =
         ∑ i, ENNReal.ofReal (w i) • μ i := by
   …

   Mentions: OAI.Problem358.PositiveFiniteCoupling.Support

8. theorem OAI.Problem358.real_atomic_matrix_isCoupling line 175

   Source documentation

   A nonnegative real matrix with probability margins induces a coupling of those atomic probability laws.

   theorem real_atomic_matrix_isCoupling
       {d : ℕ} {ι κ : Type*} [Fintype ι] [Fintype κ]
       (m : ι → ℝ) (n : κ → ℝ) (y : ι → E d) (z : κ → E d)
       (hm : ∀ i, 0 ≤ m i) (hm1 : ∑ i, m i = 1)
       (p : ι → κ → ℝ) (hp : ∀ i j, 0 ≤ p i j)
       (hrow : ∀ i, ∑ j, p i j = m i) (hcol : ∀ j, ∑ i, p i j = n j) :
       IsCoupling (∑ i, ENNReal.ofReal (m i) • Measure.dirac (y i))
         (∑ j, ENNReal.ofReal (n j) • Measure.dirac (z j))
         (atomicMatchingPlan (fun q : ι × κ => ENNReal.ofReal (p q.1 q.2))
           (fun q => y q.1) (fun q => z q.2)) := by
   …

   Mentions: OAI.Problem358.atomicMatchingPlan

9. theorem OAI.Problem358.FiniteCoupling.IsOptimal.wasserstein_cost line 195

   Source documentation

   The cost of any chosen optimal real matrix is exactly the squared Wasserstein quantity of its two atomic laws.

   theorem FiniteCoupling.IsOptimal.wasserstein_cost
       {d : ℕ} {ι κ : Type*} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ]
       {m : ι → ℝ} {n : κ → ℝ} {y : ι → E d} {z : κ → E d}
       (hm : ∀ i, 0 ≤ m i) (hn : ∀ j, 0 ≤ n j) (hm1 : ∑ i, m i = 1)
       (hy : Function.Injective y) (hz : Function.Injective z)
       {p : ι → κ → ℝ} (hopt : FiniteCoupling.IsOptimal (fun i j => ‖y i - z j‖ ^ 2) p)
       (hrow : ∀ i, ∑ j, p i j = m i) (hcol : ∀ j, ∑ i, p i j = n j) :
       (∑ i, ∑ j, p i j * ‖y i - z j‖ ^ 2) =
         wasserstein2 (∑ i, ENNReal.ofReal (m i) • Measure.dirac (y i))
           (∑ j, ENNReal.ofReal (n j) • Measure.dirac (z j)) ^ 2 := by
   …

   Mentions: OAI.Problem358.FiniteCoupling.IsOptimal

10. theorem OAI.Problem358.positive_atomic_plan_eq_full line 221

    Source documentation

    The positive-pair family has the same explicit joint law as the whole matrix.

    theorem positive_atomic_plan_eq_full
        {d : ℕ} {ι κ : Type*} [Fintype ι] [Fintype κ]
        (p : ι → κ → ℝ) (hp : ∀ i j, 0 ≤ p i j) (y : ι → E d) (z : κ → E d) :
        atomicMatchingPlan
          (fun q : PositiveFiniteCoupling.Pairs p => ENNReal.ofReal (p q.1.1 q.1.2))
          (fun q => y q.1.1) (fun q => z q.1.2) =
        atomicMatchingPlan (fun q : ι × κ => ENNReal.ofReal (p q.1 q.2))
          (fun q => y q.1) (fun q => z q.2) := by
    …

    Mentions: OAI.Problem358.atomicMatchingPlan, OAI.Problem358.PositiveFiniteCoupling.Pairs

11. theorem OAI.Problem358.positive_atomic_marginal_laws line 233

    Source documentation

    Endpoint atomic laws survive removal of the zero matrix entries.

    theorem positive_atomic_marginal_laws
        {d : ℕ} {ι κ : Type*} [Fintype ι] [Fintype κ]
        (m : ι → ℝ) (n : κ → ℝ) (y : ι → E d) (z : κ → E d)
        (hm : ∀ i, 0 ≤ m i) (hm1 : ∑ i, m i = 1)
        (p : ι → κ → ℝ) (hp : ∀ i j, 0 ≤ p i j)
        (hrow : ∀ i, ∑ j, p i j = m i) (hcol : ∀ j, ∑ i, p i j = n j) :
        (∑ q : PositiveFiniteCoupling.Pairs p,
          ENNReal.ofReal (p q.1.1 q.1.2) • Measure.dirac (y q.1.1)) =
            ∑ i, ENNReal.ofReal (m i) • Measure.dirac (y i) ∧
        (∑ q : PositiveFiniteCoupling.Pairs p,
          ENNReal.ofReal (p q.1.1 q.1.2) • Measure.dirac (z q.1.2)) =
            ∑ j, ENNReal.ofReal (n j) • Measure.dirac (z j) := by
    …

    Mentions: OAI.Problem358.PositiveFiniteCoupling.Pairs

12. theorem OAI.Problem358.exists_positive_atomic_coupling_data line 253

    Source documentation

    Fully semantic positive-pair input for the moving-site stability argument: positive normalized weights, the original endpoint laws, exact W₂ speed, and no site collisions at interior interpolation times.

    theorem exists_positive_atomic_coupling_data
        {d : ℕ} {ι κ : Type*} [Fintype ι] [Fintype κ]
        (m : ι → ℝ) (n : κ → ℝ) (y : ι → E d) (z : κ → E d)
        (hm : ∀ i, 0 ≤ m i) (hn : ∀ j, 0 ≤ n j)
        (hm1 : ∑ i, m i = 1) (hn1 : ∑ j, n j = 1)
        (hy : Function.Injective y) (hz : Function.Injective z) :
        ∃ p : ι → κ → ℝ,
          (∀ q : PositiveFiniteCoupling.Pairs p, 0 < p q.1.1 q.1.2) ∧
          (∑ q : PositiveFiniteCoupling.Pairs p, p q.1.1 q.1.2) = 1 ∧
          (∑ q : PositiveFiniteCoupling.Pairs p,
            ENNReal.ofReal (p q.1.1 q.1.2) • Measure.dirac (y q.1.1)) =
              (∑ i, ENNReal.ofReal (m i) • Measure.dirac (y i)) ∧
    …

    Mentions: OAI.Problem358.PositiveFiniteCoupling.Pairs

13. theorem OAI.Problem358.exists_finite_atomic_motion line 291

    Source documentation

    Two finitely supported probabilities admit a common strictly positive finite weight family. Its paired sites give the original laws, exact Wasserstein energy, and an injective moving family at every interior interpolation time.

    theorem exists_finite_atomic_motion
        {d : ℕ} {μ ν : Measure (E d)} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
        {F G : Set (E d)} (hF : F.Finite) (hG : G.Finite)
        (hμ : IsSupported μ F) (hν : IsSupported ν G) :
        ∃ N : ℕ, 0 < N ∧ ∃ (w : Fin N → ℝ) (y z : Fin N → E d),
          (∀ i, 0 < w i) ∧ (∑ i, w i) = 1 ∧
          (∀ i, y i ∈ F) ∧ (∀ i, z i ∈ G) ∧
          μ = (∑ i, ENNReal.ofReal (w i) • Measure.dirac (y i)) ∧
          ν = (∑ i, ENNReal.ofReal (w i) • Measure.dirac (z i)) ∧
          Function.Injective (fun i => (y i, z i)) ∧
          (∑ i, w i * ‖y i - z i‖ ^ 2) = wasserstein2 μ ν ^ 2 ∧
          ∀ t : ℝ, 0 < t → t < 1 →
    …

14. theorem OAI.Problem358.wasserstein2_interpolated_atomic_le line 340

    Source documentation

    Synchronous linear interpolation has Wasserstein speed at most its weighted root-mean-square site velocity. No injectivity or optimality is needed here.

    theorem wasserstein2_interpolated_atomic_le
        {d : ℕ} {ι : Type*} [Fintype ι]
        (w : ι → ℝ) (y z : ι → E d) (hw : ∀ i, 0 ≤ w i)
        (hw1 : ∑ i, w i = 1) (s t : ℝ) :
        wasserstein2
          (∑ i, ENNReal.ofReal (w i) • Measure.dirac ((1-s) • y i + s • z i))
          (∑ i, ENNReal.ofReal (w i) • Measure.dirac ((1-t) • y i + t • z i)) ≤
            |s-t| * Real.sqrt (∑ i, w i * ‖y i - z i‖ ^ 2) := by
    …

15. theorem OAI.Problem358.wasserstein2_interpolated_atomic_le_of_energy line 371

    Source documentation

    In particular, an optimal endpoint pairing gives a constant upper speed in terms of the exact endpoint Wasserstein distance.

    theorem wasserstein2_interpolated_atomic_le_of_energy
        {d : ℕ} {ι : Type*} [Fintype ι]
        (w : ι → ℝ) (y z : ι → E d) (hw : ∀ i, 0 ≤ w i)
        (hw1 : ∑ i, w i = 1) {μ ν : Measure (E d)}
        (henergy : (∑ i, w i * ‖y i-z i‖ ^ 2) = wasserstein2 μ ν ^ 2)
        (s t : ℝ) :
        wasserstein2
          (∑ i, ENNReal.ofReal (w i) • Measure.dirac ((1-s) • y i + s • z i))
          (∑ i, ENNReal.ofReal (w i) • Measure.dirac ((1-t) • y i + t • z i)) ≤
            |s-t| * wasserstein2 μ ν := by
    …

16. theorem OAI.Problem358.interpolated_atomic_isProbability line 385

    Source documentation

    Those interpolated laws remain probabilities for every real time.

    theorem interpolated_atomic_isProbability
        {d : ℕ} {ι : Type*} [Fintype ι]
        (w : ι → ℝ) (y z : ι → E d) (hw : ∀ i, 0 ≤ w i)
        (hw1 : ∑ i, w i = 1) (t : ℝ) :
        IsProbabilityMeasure
          (∑ i, ENNReal.ofReal (w i) • Measure.dirac ((1-t) • y i + t • z i)) := by
    …

17. theorem OAI.Problem358.interpolated_atomic_supported line 399

    Source documentation

    On the unit time interval, the whole atomic motion stays in any convex set containing both endpoint site families.

    theorem interpolated_atomic_supported
        {d : ℕ} {ι : Type*} [Fintype ι]
        (w : ι → ℝ) (y z : ι → E d) {Y : Set (E d)} (hY : Convex ℝ Y)
        (hy : ∀ i, y i ∈ Y) (hz : ∀ i, z i ∈ Y)
        {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) :
        IsSupported
          (∑ i, ENNReal.ofReal (w i) • Measure.dirac ((1-t) • y i + t • z i)) Y := by
    …