OAI/Analysis/Brenier/Atomic.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem358.finite_atomic_probability line 12
2. lemma OAI.Problem358.finite_atomic_supported line 18
3. lemma OAI.Problem358.HasExactlyThreeAtoms.isProbabilityMeasure line 26
4. lemma OAI.Problem358.HasExactlyThreeAtoms.isSupported line 32
5. lemma OAI.Problem358.finite_atomic_singleton line 38
6. lemma OAI.Problem358.finite_atomic_singleton_of_not_mem line 44
7. lemma OAI.Problem358.finite_atomic_ne_of_missing_atom line 54
8. def OAI.Problem358.atomicMatchingPlan line 70

   Source documentation

   The coupling which matches equally indexed atoms without splitting mass.

   def atomicMatchingPlan {d : ℕ} {ι : Type*} [Fintype ι]
       (w : ι → ℝ≥0∞) (y z : ι → E d) : Measure (E d × E d) :=
   …

9. theorem OAI.Problem358.atomicMatchingPlan_isProbability line 74
10. theorem OAI.Problem358.atomicMatchingPlan_fst line 80
11. theorem OAI.Problem358.atomicMatchingPlan_snd line 88
12. theorem OAI.Problem358.atomicMatchingPlan_isCoupling line 96
13. theorem OAI.Problem358.quadraticPlanCost_atomicMatchingPlan line 103
14. theorem OAI.Problem358.quadraticPlanCost_atomicMatchingPlan_ne_top line 110
15. theorem OAI.Problem358.wasserstein2_atomic_le line 120

    Source documentation

    Matching equally indexed atoms gives an explicit upper bound for the exact Wasserstein quantity used in the challenge.

    theorem wasserstein2_atomic_le {d : ℕ} {ι : Type*} [Fintype ι]
        (w : ι → ℝ≥0∞) (y z : ι → E d) (hw : ∑ i, w i = 1) :
        wasserstein2 (∑ i, w i • Measure.dirac (y i))
          (∑ i, w i • Measure.dirac (z i)) ≤
          Real.sqrt (∑ i, (w i).toReal * ‖y i - z i‖ ^ 2) := by
    …

16. theorem OAI.Problem358.eq_sum_dirac_of_ae_mem_range line 145

    Source documentation

    A measure concentrated on an injectively indexed finite set is the sum of its point masses.

    theorem eq_sum_dirac_of_ae_mem_range {X ι : Type*} [MeasurableSpace X]
        [MeasurableSingletonClass X] [Fintype ι] (μ : Measure X) (y : ι → X)
        (hy : Function.Injective y) (hμ : ∀ᵐ x ∂μ, x ∈ Set.range y) :
        μ = ∑ i, μ {y i} • Measure.dirac (y i) := by
    …

17. theorem OAI.Problem358.ae_mem_range_sum_dirac line 159

    Source documentation

    Every weighted finite atomic measure is concentrated on its listed atoms.

    theorem ae_mem_range_sum_dirac {X ι : Type*} [MeasurableSpace X]
        [MeasurableSingletonClass X] [Fintype ι] (w : ι → ℝ≥0∞) (y : ι → X) :
        ∀ᵐ x ∂(∑ i, w i • Measure.dirac (y i)), x ∈ Set.range y := by
    …

18. theorem OAI.Problem358.IsCoupling.ae_mem_atomic_pairs line 168

    Source documentation

    All mass of a coupling of finite atomic measures is carried by pairs of listed atoms.

    theorem IsCoupling.ae_mem_atomic_pairs {d : ℕ} {ι κ : Type*} [Fintype ι] [Fintype κ]
        {w : ι → ℝ≥0∞} {v : κ → ℝ≥0∞} {y : ι → E d} {z : κ → E d}
        {π : Measure (E d × E d)}
        (hπ : IsCoupling (∑ i, w i • Measure.dirac (y i))
          (∑ j, v j • Measure.dirac (z j)) π) :
        ∀ᵐ p ∂π, p ∈ Set.range (fun q : ι × κ => (y q.1, z q.2)) := by
    …

19. theorem OAI.Problem358.IsCoupling.atomic_decomposition line 189

    Source documentation

    A coupling of injectively indexed atomic measures has the usual finite matrix representation.

    theorem IsCoupling.atomic_decomposition {d : ℕ} {ι κ : Type*} [Fintype ι] [Fintype κ]
        {w : ι → ℝ≥0∞} {v : κ → ℝ≥0∞} {y : ι → E d} {z : κ → E d}
        {π : Measure (E d × E d)}
        (hπ : IsCoupling (∑ i, w i • Measure.dirac (y i))
          (∑ j, v j • Measure.dirac (z j)) π)
        (hy : Function.Injective y) (hz : Function.Injective z) :
        π = ∑ q : ι × κ, π {(y q.1, z q.2)} • Measure.dirac (y q.1, z q.2) := by
    …

20. theorem OAI.Problem358.finite_atomic_apply_atom line 201
21. theorem OAI.Problem358.IsCoupling.atomic_row_sum line 208
22. theorem OAI.Problem358.IsCoupling.atomic_col_sum line 223
23. theorem OAI.Problem358.IsCoupling.atomic_cost line 238
24. theorem OAI.Problem358.atomicMatchingPlan_isCoupling_of_marginal_sums line 250
25. theorem OAI.Problem358.IsCoupling.atomic_row_sum_toReal line 267
26. theorem OAI.Problem358.IsCoupling.atomic_col_sum_toReal line 278
27. theorem OAI.Problem358.IsCoupling.atomic_cost_ne_top line 289
28. theorem OAI.Problem358.IsCoupling.atomic_cost_toReal line 301