OAI/Analysis/Brenier/Optimality.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.eq_graph_map_of_ae_on_graph line 13

   Source documentation

   A measure concentrated on the graph of a measurable function is determined by its first marginal. This is the last step in uniqueness of a transport plan.

   theorem eq_graph_map_of_ae_on_graph
       {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
       (π : Measure (X × Y)) {T : X → Y} (hT : Measurable T)
       (hgraph : ∀ᵐ p ∂π, p.2 = T p.1) :
       π = Measure.map (fun x => (x, T x)) (Measure.map Prod.fst π) := by
   …

2. theorem OAI.Problem358.eq_graph_map_of_fst_eq_and_ae_on_graph line 28

   Source documentation

   The same reconstruction statement with an explicitly prescribed marginal.

   theorem eq_graph_map_of_fst_eq_and_ae_on_graph
       {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
       {π : Measure (X × Y)} {ρ : Measure X} {T : X → Y}
       (hT : Measurable T) (hfst : Measure.map Prod.fst π = ρ)
       (hgraph : ∀ᵐ p ∂π, p.2 = T p.1) :
       π = Measure.map (fun x => (x, T x)) ρ := by
   …

3. theorem OAI.Problem358.integrable_sqdist_of_cost_ne_top line 50

   Source documentation

   A finite quadratic plan cost is an ordinary integrable squared distance.

   theorem integrable_sqdist_of_cost_ne_top
       (h : quadraticPlanCost π ≠ ∞) :
       Integrable (fun p : E d × E d => ‖p.1 - p.2‖ ^ 2) π := by
   …

4. theorem OAI.Problem358.quadraticPlanCost_eq_ofReal_integral line 58

   Source documentation

   Conversion between the extended and real quadratic costs.

   theorem quadraticPlanCost_eq_ofReal_integral
       (h : Integrable (fun p : E d × E d => ‖p.1 - p.2‖ ^ 2) π) :
       quadraticPlanCost π = ENNReal.ofReal (∫ p, ‖p.1 - p.2‖ ^ 2 ∂π) := by
   …

5. theorem OAI.Problem358.dual_integrable_sum line 65

   Source documentation

   Integrability of a separable dual potential under any coupling.

   theorem dual_integrable_sum (hπ : IsCoupling ρ μ π)
       {f g : E d → ℝ} (hf : Integrable f ρ) (hg : Integrable g μ) :
       Integrable (fun p : E d × E d => f p.1 + g p.2) π := by
   …

6. theorem OAI.Problem358.dual_integral_sum line 74

   Source documentation

   The integral of a separable dual potential depends only on the marginals.

   theorem dual_integral_sum (hπ : IsCoupling ρ μ π)
       {f g : E d → ℝ} (hf : Integrable f ρ) (hg : Integrable g μ) :
       (∫ p, f p.1 + g p.2 ∂π) = (∫ x, f x ∂ρ) + ∫ y, g y ∂μ := by
   …

7. theorem OAI.Problem358.dual_cost_lower_bound line 87

   Source documentation

   Weak Kantorovich duality for the problem's quadratic cost definition.

   theorem dual_cost_lower_bound (hπ : IsCoupling ρ μ π)
       {f g : E d → ℝ} (hf : Integrable f ρ) (hg : Integrable g μ)
       (hbound : ∀ᵐ p ∂π, f p.1 + g p.2 ≤ ‖p.1 - p.2‖ ^ 2) :
       ENNReal.ofReal ((∫ x, f x ∂ρ) + ∫ y, g y ∂μ) ≤ quadraticPlanCost π := by
   …

8. theorem OAI.Problem358.quadraticPlanCost_graph_eq_dual line 99

   Source documentation

   A graph saturating a separable dual bound has exactly the dual cost.

   theorem quadraticPlanCost_graph_eq_dual
       {T : E d → E d} (hT : Measurable T) (hpush : Measure.map T ρ = μ)
       {f g : E d → ℝ} (hf : Integrable f ρ) (hg : Integrable g μ)
       (heq : ∀ᵐ x ∂ρ, ‖x - T x‖ ^ 2 = f x + g (T x)) :
       quadraticPlanCost (graphPlan ρ T) =
         ENNReal.ofReal ((∫ x, f x ∂ρ) + ∫ y, g y ∂μ) := by
   …

9. theorem OAI.Problem358.isQuadraticOptimalMap_of_dual line 118

   Source documentation

   Dual attainment certifies optimality against every probability coupling.

   theorem isQuadraticOptimalMap_of_dual
       {T : E d → E d} (hT : Measurable T) (hpush : Measure.map T ρ = μ)
       {f g : E d → ℝ} (hf : Integrable f ρ) (hg : Integrable g μ)
       (hbound : ∀ π : Measure (E d × E d), IsCoupling ρ μ π →
         ∀ᵐ p ∂π, f p.1 + g p.2 ≤ ‖p.1 - p.2‖ ^ 2)
       (heq : ∀ᵐ x ∂ρ, ‖x - T x‖ ^ 2 = f x + g (T x)) :
       IsQuadraticOptimalMap ρ μ T := by
   …

10. theorem OAI.Problem358.coupling_dirac_eq_graphPlan_const line 140

    Source documentation

    There is only one coupling with a fixed first marginal and a Dirac second marginal.

    theorem coupling_dirac_eq_graphPlan_const {d : ℕ} {ρ : Measure (E d)}
        {π : Measure (E d × E d)} {y : E d}
        (hπ : IsCoupling ρ (Measure.dirac y) π) :
        π = graphPlan ρ (fun _ => y) := by
    …

11. theorem OAI.Problem358.isUniqueQuadraticOptimalMap_const line 151

    Source documentation

    The constant map to a point is the unique quadratic optimal map to its Dirac law. No moment assumption is necessary: every competing coupling is already the same graph.

    theorem isUniqueQuadraticOptimalMap_const {d : ℕ} (ρ : Measure (E d))
        [IsProbabilityMeasure ρ] (y : E d) :
        IsUniqueQuadraticOptimalMap ρ (Measure.dirac y) (fun _ => y) := by
    …

12. theorem OAI.Problem358.eq_dirac_of_supported_singleton line 163

    Source documentation

    A probability measure supported on a singleton is the corresponding Dirac law.

    theorem eq_dirac_of_supported_singleton {d : ℕ} (μ : Measure (E d))
        [IsProbabilityMeasure μ] (y : E d) (hμ : IsSupported μ {y}) :
        μ = Measure.dirac y := by
    …

13. theorem OAI.Problem358.eq_dirac_of_supported_subsingleton line 174

    Source documentation

    The same conclusion holds for any nonempty subsingleton support set.

    theorem eq_dirac_of_supported_subsingleton {d : ℕ} (μ : Measure (E d))
        [IsProbabilityMeasure μ] {Y : Set (E d)} (hY : Y.Subsingleton)
        {y : E d} (hy : y ∈ Y) (hμ : IsSupported μ Y) :
        μ = Measure.dirac y := by
    …

14. theorem OAI.Problem358.one_third_stability_of_subsingleton_target line 185

    Source documentation

    The singleton-target case of stability, for an arbitrary probability source.

    theorem one_third_stability_of_subsingleton_target {d : ℕ}
        (ρ : Measure (E d)) [IsProbabilityMeasure ρ]
        {Y : Set (E d)} (hY : Y.Subsingleton) (hYn : Y.Nonempty) :
        ∃ C : ℝ, 0 ≤ C ∧ ∀ (μ ν : Measure (E d)),
          IsProbabilityMeasure μ → IsProbabilityMeasure ν →
          IsSupported μ Y → IsSupported ν Y →
          ∃ Tμ Tν : E d → E d,
            IsUniqueQuadraticOptimalMap ρ μ Tμ ∧
            IsUniqueQuadraticOptimalMap ρ ν Tν ∧
            mapL2Dist ρ Tμ Tν ≤ C * Real.rpow (wasserstein2 μ ν) (1 / 3 : ℝ) := by
    …

15. theorem OAI.Problem358.dual_saturation_of_integral_eq line 220

    Source documentation

    Equality in the integral dual bound forces saturation almost everywhere.

    theorem dual_saturation_of_integral_eq
        (hπ : IsCoupling ρ μ π) {f g : E d → ℝ}
        (hf : Integrable f ρ) (hg : Integrable g μ)
        (hc : Integrable (fun p : E d × E d => ‖p.1 - p.2‖ ^ 2) π)
        (hbound : ∀ᵐ p ∂π, f p.1 + g p.2 ≤ ‖p.1 - p.2‖ ^ 2)
        (heq : (∫ p, ‖p.1 - p.2‖ ^ 2 ∂π) =
          (∫ x, f x ∂ρ) + ∫ y, g y ∂μ) :
        ∀ᵐ p ∂π, f p.1 + g p.2 = ‖p.1 - p.2‖ ^ 2 := by
    …

16. theorem OAI.Problem358.eq_graphPlan_of_dual_saturation line 233

    Source documentation

    A saturated dual bound whose equality locus is a graph identifies the full plan.

    theorem eq_graphPlan_of_dual_saturation
        {T : E d → E d} (hT : Measurable T)
        (hπ : IsCoupling ρ μ π) {f g : E d → ℝ}
        (hf : Integrable f ρ) (hg : Integrable g μ)
        (hc : Integrable (fun p : E d × E d => ‖p.1 - p.2‖ ^ 2) π)
        (hbound : ∀ᵐ p ∂π, f p.1 + g p.2 ≤ ‖p.1 - p.2‖ ^ 2)
        (heq : (∫ p, ‖p.1 - p.2‖ ^ 2 ∂π) =
          (∫ x, f x ∂ρ) + ∫ y, g y ∂μ)
        (hstrict : ∀ᵐ p ∂π,
          f p.1 + g p.2 = ‖p.1 - p.2‖ ^ 2 → p.2 = T p.1) :
        π = graphPlan ρ T := by
    …

17. theorem OAI.Problem358.dual_value_nonneg_of_graph line 250

    Source documentation

    A dual value attained by a graph is nonnegative.

    theorem dual_value_nonneg_of_graph
        {T : E d → E d} (hT : Measurable T) (hpush : Measure.map T ρ = μ)
        {f g : E d → ℝ} (hf : Integrable f ρ) (hg : Integrable g μ)
        (heq : ∀ᵐ x ∂ρ, ‖x - T x‖ ^ 2 = f x + g (T x)) :
        0 ≤ (∫ x, f x ∂ρ) + ∫ y, g y ∂μ := by
    …

18. theorem OAI.Problem358.isUniqueQuadraticOptimalMap_of_dual line 267

    Source documentation

    Strictness of a dual certificate identifies every optimal plan with its graph. The strictness premise is only required almost everywhere for each coupling, so null tie sets and support restrictions can be used directly.

    theorem isUniqueQuadraticOptimalMap_of_dual
        {T : E d → E d} (hT : Measurable T) (hpush : Measure.map T ρ = μ)
        {f g : E d → ℝ} (hf : Integrable f ρ) (hg : Integrable g μ)
        (hbound : ∀ π : Measure (E d × E d), IsCoupling ρ μ π →
          ∀ᵐ p ∂π, f p.1 + g p.2 ≤ ‖p.1 - p.2‖ ^ 2)
        (heq : ∀ᵐ x ∂ρ, ‖x - T x‖ ^ 2 = f x + g (T x))
        (hstrict : ∀ π : Measure (E d × E d), IsCoupling ρ μ π →
          ∀ᵐ p ∂π, f p.1 + g p.2 = ‖p.1 - p.2‖ ^ 2 → p.2 = T p.1) :
        IsUniqueQuadraticOptimalMap ρ μ T := by
    …