OAI/Analysis/Brenier/CompactTransport.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.IsCoupling.ae_mem line 14

   Source documentation

   A coupling inherits almost-everywhere support from each marginal.

   theorem IsCoupling.ae_mem {d : ℕ} {μ ν : Measure (E d)}
       {π : Measure (E d × E d)} {K Y : Set (E d)}
       (hπ : IsCoupling μ ν π) (hμ : IsSupported μ K) (hν : IsSupported ν Y) :
       ∀ᵐ p ∂π, p.1 ∈ K ∧ p.2 ∈ Y := by
   …

2. theorem OAI.Problem358.IsCoupling.integrable_sqDist_of_compact line 33

   Source documentation

   Finite second cost for a coupling whose two marginals have compact support.

   theorem IsCoupling.integrable_sqDist_of_compact {d : ℕ} {μ ν : Measure (E d)}
       {π : Measure (E d × E d)} {K Y : Set (E d)}
       (hπ : IsCoupling μ ν π) (hK : IsCompact K) (hY : IsCompact Y)
       (hμ : IsSupported μ K) (hν : IsSupported ν Y) :
       Integrable (fun p : E d × E d => ‖p.1 - p.2‖ ^ 2) π := by
   …

3. theorem OAI.Problem358.IsCoupling.quadraticPlanCost_ne_top_of_compact line 49

   Source documentation

   On compact marginal supports every coupling has finite ENNReal quadratic cost.

   theorem IsCoupling.quadraticPlanCost_ne_top_of_compact {d : ℕ} {μ ν : Measure (E d)}
       {π : Measure (E d × E d)} {K Y : Set (E d)}
       (hπ : IsCoupling μ ν π) (hK : IsCompact K) (hY : IsCompact Y)
       (hμ : IsSupported μ K) (hν : IsSupported ν Y) :
       quadraticPlanCost π ≠ ∞ := by
   …

4. theorem OAI.Problem358.IsCoupling.quadraticPlanCost_le_of_norm_le line 59

   Source documentation

   An explicit uniform cost bound from bounds on the marginal supports.

   theorem IsCoupling.quadraticPlanCost_le_of_norm_le {d : ℕ} {μ ν : Measure (E d)}
       {π : Measure (E d × E d)} {K Y : Set (E d)} {R S : ℝ}
       (hπ : IsCoupling μ ν π) (hμ : IsSupported μ K) (hν : IsSupported ν Y)
       (hK : ∀ x ∈ K, ‖x‖ ≤ R) (hY : ∀ y ∈ Y, ‖y‖ ≤ S) :
       quadraticPlanCost π ≤ ENNReal.ofReal ((R + S) ^ 2) := by
   …

5. def OAI.Problem358.probabilityCouplings line 88

   Source documentation

   The closed set of probability measures with two specified marginals.

   def probabilityCouplings (μ : ProbabilityMeasure X) (ν : ProbabilityMeasure Y) :
       Set (ProbabilityMeasure (X × Y)) :=
   …

6. theorem OAI.Problem358.probabilityCouplings_nonempty line 92
7. theorem OAI.Problem358.isClosed_probabilityCouplings line 111
8. theorem OAI.Problem358.isCompact_probabilityCouplings line 122
9. theorem OAI.Problem358.exists_probabilityCoupling_minimizer line 127

   Source documentation

   Every continuous real cost attains its minimum over compact-space probability couplings.

   theorem exists_probabilityCoupling_minimizer (μ : ProbabilityMeasure X)
       (ν : ProbabilityMeasure Y) (c : X × Y → ℝ) (hc : Continuous c) :
       ∃ π ∈ probabilityCouplings μ ν,
         ∀ η ∈ probabilityCouplings μ ν,
           (∫ p, c p ∂(π : Measure (X × Y))) ≤ ∫ p, c p ∂(η : Measure (X × Y)) := by
   …

   Mentions: OAI.Problem358.probabilityCouplings

10. theorem OAI.Problem358.exists_compact_coupling_minimizer line 139

    Source documentation

    Unbundled continuous-cost minimization, for direct use with measure-valued plans.

    theorem exists_compact_coupling_minimizer (μ : Measure X) (ν : Measure Y)
        [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
        (c : X × Y → ℝ) (hc : Continuous c) :
        ∃ π : Measure (X × Y), IsProbabilityMeasure π ∧
          Measure.map Prod.fst π = μ ∧ Measure.map Prod.snd π = ν ∧
          ∀ η : Measure (X × Y), IsProbabilityMeasure η →
            Measure.map Prod.fst η = μ → Measure.map Prod.snd η = ν →
            (∫ p, c p ∂π) ≤ ∫ p, c p ∂η := by
    …

11. theorem OAI.Problem358.isCompact_probability_supported line 169

    Source documentation

    Fixed compact support determines a compact set of probability measures.

    theorem isCompact_probability_supported {X : Type*} [MetricSpace X]
        [MeasurableSpace X] [BorelSpace X] {K : Set X} (hK : IsCompact K) :
        IsCompact {μ : ProbabilityMeasure X | (μ : Measure X) Kᶜ = 0} := by
    …

12. theorem OAI.Problem358.probabilityCouplings_ae_mem_prod line 179

    Source documentation

    Couplings of supported marginals are concentrated on the product of their supports.

    theorem probabilityCouplings_ae_mem_prod {d : ℕ}
        {μ ν : ProbabilityMeasure (E d)} {K Y : Set (E d)}
        (hμ : (μ : Measure (E d)) Kᶜ = 0) (hν : (ν : Measure (E d)) Yᶜ = 0)
        {π : ProbabilityMeasure (E d × E d)} (hπ : π ∈ probabilityCouplings μ ν) :
        ∀ᵐ p ∂(π : Measure (E d × E d)), p ∈ K ×ˢ Y := by
    …

    Mentions: OAI.Problem358.probabilityCouplings

13. theorem OAI.Problem358.isCompact_probabilityCouplings_of_supported line 196

    Source documentation

    Compactly supported marginals have a compact set of couplings in the weak topology.

    theorem isCompact_probabilityCouplings_of_supported {d : ℕ}
        {μ ν : ProbabilityMeasure (E d)} {K Y : Set (E d)}
        (hK : IsCompact K) (hY : IsCompact Y)
        (hμ : (μ : Measure (E d)) Kᶜ = 0) (hν : (ν : Measure (E d)) Yᶜ = 0) :
        IsCompact (probabilityCouplings μ ν) := by
    …

    Mentions: OAI.Problem358.probabilityCouplings

14. def OAI.Problem358.boundedQuadraticCost line 207

    Source documentation

    A conveniently clipped quadratic cost, bounded and continuous on the full product space.

    def boundedQuadraticCost (d : ℕ) (M : ℝ) (hM : 0 ≤ M) :
        BoundedContinuousFunction (E d × E d) ℝ where
    …

15. theorem OAI.Problem358.exists_quadraticOptimalPlan_of_compact_support line 226

    Source documentation

    Compactly supported probabilities have a minimizing quadratic transport plan.

    theorem exists_quadraticOptimalPlan_of_compact_support {d : ℕ}
        (μ ν : Measure (E d)) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
        {K Y : Set (E d)} (hK : IsCompact K) (hY : IsCompact Y)
        (hμ : IsSupported μ K) (hν : IsSupported ν Y) :
        ∃ π : Measure (E d × E d), IsCoupling μ ν π ∧
          quadraticPlanCost π ≠ ∞ ∧
          ∀ η : Measure (E d × E d), IsCoupling μ ν η →
            quadraticPlanCost π ≤ quadraticPlanCost η := by
    …

16. theorem OAI.Problem358.exists_finite_cost_coupling_of_compact_support line 281

    Source documentation

    In particular, a finite-cost plan is available for any compactly supported probabilities.

    theorem exists_finite_cost_coupling_of_compact_support {d : ℕ}
        (μ ν : Measure (E d)) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
        {K Y : Set (E d)} (hK : IsCompact K) (hY : IsCompact Y)
        (hμ : IsSupported μ K) (hν : IsSupported ν Y) :
        ∃ π : Measure (E d × E d), IsCoupling μ ν π ∧ quadraticPlanCost π ≠ ∞ := by
    …

17. theorem OAI.Problem358.wasserstein2_attained_of_compact_support line 303

    Source documentation

    The infimum in the exact Wasserstein definition is attained for compact supports.

    theorem wasserstein2_attained_of_compact_support {d : ℕ}
        (μ ν : Measure (E d)) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
        {K Y : Set (E d)} (hK : IsCompact K) (hY : IsCompact Y)
        (hμ : IsSupported μ K) (hν : IsSupported ν Y) :
        ∃ π : Measure (E d × E d), IsCoupling μ ν π ∧ quadraticPlanCost π ≠ ∞ ∧
          wasserstein2 μ ν = Real.sqrt (quadraticPlanCost π).toReal := by
    …

18. theorem OAI.Problem358.wasserstein2_eq_zero_iff_of_compact_support line 314

    Source documentation

    Zero distance separates compactly supported probabilities.

    theorem wasserstein2_eq_zero_iff_of_compact_support {d : ℕ}
        (μ ν : Measure (E d)) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
        {K Y : Set (E d)} (hK : IsCompact K) (hY : IsCompact Y)
        (hμ : IsSupported μ K) (hν : IsSupported ν Y) :
        wasserstein2 μ ν = 0 ↔ μ = ν := by
    …

19. theorem OAI.Problem358.wasserstein2_pos_iff_of_compact_support line 326

    Source documentation

    Distinct compactly supported probabilities have strictly positive distance.

    theorem wasserstein2_pos_iff_of_compact_support {d : ℕ}
        (μ ν : Measure (E d)) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
        {K Y : Set (E d)} (hK : IsCompact K) (hY : IsCompact Y)
        (hμ : IsSupported μ K) (hν : IsSupported ν Y) :
        0 < wasserstein2 μ ν ↔ μ ≠ ν := by
    …

20. theorem OAI.Problem358.integral_test_le_wasserstein2_of_compact_support line 336

    Source documentation

    Compact support discharges both the finite-cost and integrability hypotheses in the Lipschitz testing inequality.

    theorem integral_test_le_wasserstein2_of_compact_support {d : ℕ}
        (μ ν : Measure (E d)) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
        {K Y : Set (E d)} (hK : IsCompact K) (hY : IsCompact Y)
        (hμ : IsSupported μ K) (hν : IsSupported ν Y)
        {L : ℝ≥0} {f : E d → ℝ} (hf : LipschitzWith L f) :
        |(∫ x, f x ∂μ) - ∫ y, f y ∂ν| ≤ L * wasserstein2 μ ν := by
    …

21. theorem OAI.Problem358.tendsto_probabilityMeasure_of_compact_wasserstein2_tendsto_zero line 349

    Source documentation

    On compact supports, Wasserstein convergence implies weak convergence without an additional finite-cost hypothesis; the compact supports may vary with the index.

    theorem tendsto_probabilityMeasure_of_compact_wasserstein2_tendsto_zero
        {d : ℕ} {ι : Type*} {l : Filter ι} [l.IsCountablyGenerated]
        {μs : ι → ProbabilityMeasure (E d)} {ν : ProbabilityMeasure (E d)}
        {Ks : ι → Set (E d)} {Y : Set (E d)}
        (hKs : ∀ i, IsCompact (Ks i)) (hY : IsCompact Y)
        (hμs : ∀ i, IsSupported (μs i : Measure (E d)) (Ks i))
        (hν : IsSupported (ν : Measure (E d)) Y)
        (hW : Tendsto (fun i => wasserstein2 (μs i : Measure (E d)) (ν : Measure (E d)))
          l (𝓝 0)) : Tendsto μs l (𝓝 ν) := by
    …