Existence.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.exists_unique_optimal_map_uniform_atomic line 21

Source documentation

Existence and uniqueness among all quadratic transport plans for an arbitrary strictly positive finite atomic target, with the exact uniform source definition. The proof constructs the cell masses variationally rather than assuming them.

theorem exists_unique_optimal_map_uniform_atomic
    (K : Set (E d)) [IsProbabilityMeasure (uniformMeasure K)]
    (hK : IsCompact K) (y : ι → E d) (hinj : Function.Injective y)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1) :
    ∃ T : E d → E d,
      IsUniqueQuadraticOptimalMap (uniformMeasure K)
        (∑ i, ENNReal.ofReal (m i) • Measure.dirac (y i)) T := by
…

theorem OAI.Problem358.exists_unique_optimal_map_uniform_finite_supported line 44

Source documentation

The finite-target existence theorem in a presentation-free form.

theorem exists_unique_optimal_map_uniform_finite_supported
    (K : Set (E d)) (hK : IsCompact K) (hinterior : (interior K).Nonempty)
    (μ : Measure (E d)) [IsProbabilityMeasure μ]
    {F : Set (E d)} (hF : F.Finite) (hμ : IsSupported μ F) :
    ∃ T : E d → E d, IsUniqueQuadraticOptimalMap (uniformMeasure K) μ T := by
…

theorem OAI.Problem358.exists_uniform_atomic_map_and_potential line 65

Source documentation

Finite-target existence together with a globally convex normalized Lipschitz potential and its pointwise supporting-slope inequality.

theorem exists_uniform_atomic_map_and_potential
    (K : Set (E d)) [IsProbabilityMeasure (uniformMeasure K)]
    (hK : IsCompact K) (y : ι → E d) (hinj : Function.Injective y)
    (m : ι → ℝ) (hm : ∀ i, 0 < m i) (hsum : ∑ i, m i = 1)
    (L : NNReal) (hL : ∀ i, ‖y i‖ ≤ L) (x₀ : E d) :
    ∃ (u : E d → ℝ) (T : E d → E d),
      IsUniqueQuadraticOptimalMap (uniformMeasure K)
        (∑ i, ENNReal.ofReal (m i) • Measure.dirac (y i)) T ∧
      ConvexOn ℝ Set.univ u ∧ LipschitzWith L u ∧ u x₀ = 0 ∧
      (∀ x, T x ∈ Set.range y) ∧
      ∀ x z, u x + ⟪T x, z - x⟫ ≤ u z := by
…

theorem OAI.Problem358.exists_uniform_finite_map_and_potential line 108

Source documentation

Presentation-free finite-source data for compactness/approximation arguments.

theorem exists_uniform_finite_map_and_potential
    (K : Set (E d)) (hK : IsCompact K) (hinterior : (interior K).Nonempty)
    (μ : Measure (E d)) [IsProbabilityMeasure μ]
    {F Y : Set (E d)} (hF : F.Finite) (hFY : F ⊆ Y) (hμ : IsSupported μ F)
    (L : NNReal) (hL : ∀ z ∈ Y, ‖z‖ ≤ L) (x₀ : E d) :
    ∃ (u : E d → ℝ) (T : E d → E d),
      IsUniqueQuadraticOptimalMap (uniformMeasure K) μ T ∧
      ConvexOn ℝ Set.univ u ∧ LipschitzWith L u ∧ u x₀ = 0 ∧
      (∀ x, T x ∈ Y) ∧ ∀ x z, u x + ⟪T x, z - x⟫ ≤ u z := by
…

theorem OAI.Problem358.exists_unique_optimal_map_of_approximating_potentials line 143

Source documentation

Passing normalized convex supporting potentials and their maps to the limit gives a unique optimal map with the prescribed target law. No stability estimate is required here.

theorem exists_unique_optimal_map_of_approximating_potentials
    {d : ℕ} {K Y : Set (E d)} {μ : Measure (E d)}
    [IsFiniteMeasure (uniformMeasure K)] [IsFiniteMeasure μ]
    (hK : IsCompact K) (hKconv : Convex ℝ K) (hY : IsCompact Y)
    (hμ : IsSupported μ Y) (x₀ : E d) (hx₀ : x₀ ∈ K)
    (uₙ : ℕ → E d → ℝ) (Tₙ Qₙ : ℕ → E d → E d) (L : ℝ≥0)
    (hLip : ∀ n, LipschitzOnWith L (uₙ n) K)
    (hconv : ∀ n, ConvexOn ℝ K (uₙ n))
    (hnormal : ∀ n, uₙ n x₀ = 0)
    (hTmeas : ∀ n, Measurable (Tₙ n)) (hQmeas : ∀ n, Measurable (Qₙ n))
    (hmem : ∀ n, ∀ᵐ x ∂uniformMeasure K, Tₙ n x ∈ Y)
    (hs : ∀ n, ∀ᵐ x ∂uniformMeasure K, ∀ z ∈ K,
…

theorem OAI.Problem358.exists_unique_optimal_map_of_simpleFunc_potentials line 176

Source documentation

Reduction of general optimal-map existence to a uniformly Lipschitz convex-potential construction for finite-range quantizations of the target.

theorem exists_unique_optimal_map_of_simpleFunc_potentials
    {d : ℕ} {K Y : Set (E d)} {μ : Measure (E d)}
    [IsFiniteMeasure (uniformMeasure K)] [IsFiniteMeasure μ]
    (hK : IsCompact K) (hKconv : Convex ℝ K) (hY : IsCompact Y) (hYne : Y.Nonempty)
    (hμ : IsSupported μ Y) (x₀ : E d) (hx₀ : x₀ ∈ K) (L : ℝ≥0)
    (hfinite : ∀ q : SimpleFunc (E d) (E d), (∀ x, q x ∈ Y) →
      ∃ (u : E d → ℝ) (T : E d → E d), LipschitzOnWith L u K ∧
        ConvexOn ℝ K u ∧ u x₀ = 0 ∧ Measurable T ∧
        (∀ᵐ x ∂uniformMeasure K, T x ∈ Y) ∧
        (∀ᵐ x ∂uniformMeasure K, ∀ z ∈ K, u x + inner ℝ (T x) (z - x) ≤ u z) ∧
        Measure.map T (uniformMeasure K) = Measure.map q μ) :
    ∃ T : E d → E d, IsUniqueQuadraticOptimalMap (uniformMeasure K) μ T := by
…

theorem OAI.Problem358.exists_unique_optimal_map_uniform_compact line 206

Source documentation

General Brenier existence and uniqueness among all quadratic transport plans for uniform compact convex sources and arbitrary compactly supported probability targets.

theorem exists_unique_optimal_map_uniform_compact
    {d : ℕ} {K Y : Set (E d)}
    (hK : IsCompact K) (hKconv : Convex ℝ K) (hInterior : (interior K).Nonempty)
    (hY : IsCompact Y) (hYne : Y.Nonempty)
    (μ : Measure (E d)) [IsProbabilityMeasure μ] (hμ : IsSupported μ Y) :
    ∃ T : E d → E d, IsUniqueQuadraticOptimalMap (uniformMeasure K) μ T := by
…