Coupling.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.IsCoupling.map line 13

Source documentation

Mapping both coordinates of a coupling gives a coupling of the mapped marginals.

theorem IsCoupling.map {d : ℕ} {μ ν : Measure (E d)}
    {π : Measure (E d × E d)} (hπ : IsCoupling μ ν π)
    {Q R : E d → E d} (hQ : Measurable Q) (hR : Measurable R) :
    IsCoupling (Measure.map Q μ) (Measure.map R ν)
      (Measure.map (Prod.map Q R) π) := by
…

theorem OAI.Problem358.quadraticPlanCost_map line 30

Source documentation

Change of variables for the quadratic cost of a mapped coupling.

theorem quadraticPlanCost_map {d : ℕ} (π : Measure (E d × E d))
    {Q R : E d → E d} (hQ : Measurable Q) (hR : Measurable R) :
    quadraticPlanCost (Measure.map (Prod.map Q R) π) =
      ∫⁻ p, ENNReal.ofReal (‖Q p.1 - R p.2‖ ^ 2) ∂π := by
…

theorem OAI.Problem358.IsCoupling.ae_pair line 41

Source documentation

Almost-everywhere statements about either marginal pull back along a coupling.

theorem IsCoupling.ae_pair {d : ℕ} {μ ν : Measure (E d)}
    {π : Measure (E d × E d)} (hπ : IsCoupling μ ν π)
    {P Q : E d → Prop} (hP : ∀ᵐ x ∂μ, P x) (hQ : ∀ᵐ y ∂ν, Q y) :
    ∀ᵐ p ∂π, P p.1 ∧ Q p.2 := by
…

theorem OAI.Problem358.sqrt_lintegral_norm_sq_eq_lpNorm line 51
theorem OAI.Problem358.lpNorm_two_le_of_ae_bound line 61

theorem OAI.Problem358.sqrt_quadraticPlanCost_eq_lpNorm line 74

Source documentation

The square root of a quadratic plan cost is the real-valued L² norm.

theorem sqrt_quadraticPlanCost_eq_lpNorm {d : ℕ} (π : Measure (E d × E d)) :
    Real.sqrt (quadraticPlanCost π).toReal =
      lpNorm (fun p : E d × E d => p.1 - p.2) 2 π := by
…

theorem OAI.Problem358.quadraticPlanCost_ne_top_iff_memLp line 80

Source documentation

A plan has finite quadratic cost exactly when its displacement belongs to L².

theorem quadraticPlanCost_ne_top_iff_memLp {d : ℕ}
    (π : Measure (E d × E d)) :
    quadraticPlanCost π ≠ ∞ ↔
      MemLp (fun p : E d × E d => p.1 - p.2) 2 π := by
…

theorem OAI.Problem358.sqrt_quadraticPlanCost_map_le_of_memLp line 90

Source documentation

Perturbing the two coordinates by uniformly bounded errors changes root cost by at most the sum of those errors. Only the original displacement needs an L² bound.

theorem sqrt_quadraticPlanCost_map_le_of_memLp {d : ℕ} {μ ν : Measure (E d)}
    {π : Measure (E d × E d)} (hπ : IsCoupling μ ν π)
    {Q R : E d → E d} (hQ : Measurable Q) (hR : Measurable R)
    {ε η : ℝ} (hε : 0 ≤ ε) (hη : 0 ≤ η)
    (hQerr : ∀ᵐ x ∂μ, ‖Q x - x‖ ≤ ε)
    (hRerr : ∀ᵐ y ∂ν, ‖R y - y‖ ≤ η)
    (hfinite : MemLp (fun p : E d × E d => p.1 - p.2) 2 π) :
    Real.sqrt (quadraticPlanCost (Measure.map (Prod.map Q R) π)).toReal ≤
      Real.sqrt (quadraticPlanCost π).toReal + ε + η := by
…

theorem OAI.Problem358.quadraticPlanCost_map_ne_top line 119

Source documentation

Uniformly bounded changes of coordinates preserve finite quadratic cost.

theorem quadraticPlanCost_map_ne_top {d : ℕ} {μ ν : Measure (E d)}
    {π : Measure (E d × E d)} (hπ : IsCoupling μ ν π)
    {Q R : E d → E d} (hQ : Measurable Q) (hR : Measurable R)
    {ε η : ℝ}
    (hQerr : ∀ᵐ x ∂μ, ‖Q x - x‖ ≤ ε)
    (hRerr : ∀ᵐ y ∂ν, ‖R y - y‖ ≤ η)
    (hfinite : quadraticPlanCost π ≠ ∞) :
    quadraticPlanCost (Measure.map (Prod.map Q R) π) ≠ ∞ := by
…

theorem OAI.Problem358.sqrt_quadraticPlanCost_map_le line 148

Source documentation

Finite-cost version of sqrt_quadraticPlanCost_map_le_of_memLp.

theorem sqrt_quadraticPlanCost_map_le {d : ℕ} {μ ν : Measure (E d)}
    {π : Measure (E d × E d)} (hπ : IsCoupling μ ν π)
    {Q R : E d → E d} (hQ : Measurable Q) (hR : Measurable R)
    {ε η : ℝ} (hε : 0 ≤ ε) (hη : 0 ≤ η)
    (hQerr : ∀ᵐ x ∂μ, ‖Q x - x‖ ≤ ε)
    (hRerr : ∀ᵐ y ∂ν, ‖R y - y‖ ≤ η)
    (hfinite : quadraticPlanCost π ≠ ∞) :
    Real.sqrt (quadraticPlanCost (Measure.map (Prod.map Q R) π)).toReal ≤
      Real.sqrt (quadraticPlanCost π).toReal + ε + η :=
…