OAI/Analysis/Brenier/MaxLimits.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.eventually_limiting_maximizer line 18

   Source documentation

   A maximizer among finitely many convergent scores is eventually a maximizer of the limiting scores. Only membership in the limiting maximizing set is asserted; ties among the limiting scores need not be resolved consistently.

   theorem eventually_limiting_maximizer
       {ι β : Type*} [Finite ι] {l : Filter β}
       {score : β → ι → ℝ} {limitScore : ι → ℝ} {pick : β → ι}
       (hscore : ∀ i, Tendsto (fun n => score n i) l (nhds (limitScore i)))
       (hpick : ∀ᶠ n in l, ∀ i, score n i ≤ score n (pick n)) :
       ∀ᶠ n in l, ∀ i, limitScore i ≤ limitScore (pick n) := by
   …

2. theorem OAI.Problem358.tendsto_value_of_finite_maximizer line 41

   Source documentation

   Finite active-value convergence, allowing different active indices at every parameter and repeated limiting slopes. This is the endpoint argument for finite maxima of moving affine functions.

   theorem tendsto_value_of_finite_maximizer
       {ι β X : Type*} [Finite ι] [TopologicalSpace X] {l : Filter β}
       {score : β → ι → ℝ} {limitScore : ι → ℝ} {pick : β → ι}
       {value : β → ι → X} {limitValue : ι → X} {x : X}
       (hscore : ∀ i, Tendsto (fun n => score n i) l (nhds (limitScore i)))
       (hpick : ∀ᶠ n in l, ∀ i, score n i ≤ score n (pick n))
       (hvalue : ∀ i, Tendsto (fun n => value n i) l (nhds (limitValue i)))
       (hactive : ∀ i, (∀ j, limitScore j ≤ limitScore i) → limitValue i = x) :
       Tendsto (fun n => value n (pick n)) l (nhds x) := by
   …

3. theorem OAI.Problem358.exists_tendsto_value_of_finite_maximizer line 69

   Source documentation

   If equal maximal scores force equal values, some limiting maximizing value is the limit, without requiring the maximizing index to be unique.

   theorem exists_tendsto_value_of_finite_maximizer
       {ι β X : Type*} [Finite ι] [Nonempty ι] [TopologicalSpace X]
       {l : Filter β} {score : β → ι → ℝ} {limitScore : ι → ℝ}
       {pick : β → ι} {value : β → ι → X} {limitValue : ι → X}
       (hscore : ∀ i, Tendsto (fun n => score n i) l (nhds (limitScore i)))
       (hpick : ∀ᶠ n in l, ∀ i, score n i ≤ score n (pick n))
       (hvalue : ∀ i, Tendsto (fun n => value n i) l (nhds (limitValue i)))
       (hties : ∀ i j, limitScore i = limitScore j → limitValue i = limitValue j) :
       ∃ i, (∀ j, limitScore j ≤ limitScore i) ∧
         Tendsto (fun n => value n (pick n)) l (nhds (limitValue i)) := by
   …

4. theorem OAI.Problem358.tendsto_affine_active_slope line 86

   Source documentation

   Endpoint convergence of the active slopes of affine maxima. The source point is fixed; a.e. applications remove the finite union of limiting tie hyperplanes.

   theorem tendsto_affine_active_slope
       {ι β V : Type*} [Finite ι] [NormedAddCommGroup V] [InnerProductSpace ℝ V]
       {l : Filter β} {site : β → ι → V} {limitSite : ι → V}
       {offset : β → ι → ℝ} {limitOffset : ι → ℝ} {pick : β → ι}
       {point target : V}
       (hsite : ∀ i, Tendsto (fun n => site n i) l (nhds (limitSite i)))
       (hoffset : ∀ i, Tendsto (fun n => offset n i) l (nhds (limitOffset i)))
       (hpick : ∀ᶠ n in l, ∀ i,
         inner ℝ point (site n i) + offset n i ≤
           inner ℝ point (site n (pick n)) + offset n (pick n))
       (hactive : ∀ i, (∀ j,
         inner ℝ point (limitSite j) + limitOffset j ≤
   …

5. theorem OAI.Problem358.ae_tendsto_selected_affine_slopes line 122

   Source documentation

   Almost-everywhere active-slope convergence, without distinctness of the limiting sites. The finite union of limiting affine tie hyperplanes is removed here.

   theorem ae_tendsto_selected_affine_slopes
       {d : ℕ} {ι β : Type*} [Fintype ι] {l : Filter β}
       {ρ : Measure (E d)} (hρ : ρ ≪ volume)
       {y : β → ι → E d} {y₀ : ι → E d}
       {c : β → ι → ℝ} {c₀ : ι → ℝ}
       {pick : β → E d → ι} {pick₀ : E d → ι}
       (hy : ∀ i, Tendsto (fun n => y n i) l (𝓝 (y₀ i)))
       (hc : ∀ i, Tendsto (fun n => c n i) l (𝓝 (c₀ i)))
       (hpick : ∀ᵐ x ∂ρ, ∀ᶠ n in l, ∀ i,
         inner ℝ x (y n i) + c n i ≤ inner ℝ x (y n (pick n x)) + c n (pick n x))
       (hpick₀ : ∀ᵐ x ∂ρ, ∀ i,
         inner ℝ x (y₀ i) + c₀ i ≤ inner ℝ x (y₀ (pick₀ x)) + c₀ (pick₀ x)) :
   …

6. theorem OAI.Problem358.ae_tendsto_affine_maximizer_maps line 143

   Source documentation

   The same endpoint statement for maps specified by active-slope certificates. No convergence of active indices, and no injectivity of limiting sites, is required.

   theorem ae_tendsto_affine_maximizer_maps
       {d : ℕ} {ι : Type*} [Fintype ι]
       {ρ : Measure (E d)} (hρ : ρ ≪ volume)
       {y : ℕ → ι → E d} {y₀ : ι → E d}
       {c : ℕ → ι → ℝ} {c₀ : ι → ℝ}
       {T : ℕ → E d → E d} {T₀ : E d → E d}
       (hy : ∀ i, Tendsto (fun n => y n i) atTop (𝓝 (y₀ i)))
       (hc : ∀ i, Tendsto (fun n => c n i) atTop (𝓝 (c₀ i)))
       (hT : ∀ n, ∀ᵐ x ∂ρ, ∃ i, T n x = y n i ∧
         ∀ j, inner ℝ x (y n j) + c n j ≤ inner ℝ x (y n i) + c n i)
       (hT₀ : ∀ᵐ x ∂ρ, ∃ i, T₀ x = y₀ i ∧
         ∀ j, inner ℝ x (y₀ j) + c₀ j ≤ inner ℝ x (y₀ i) + c₀ i) :
   …

7. theorem OAI.Problem358.tendsto_mapL2Dist_affine_maximizer_maps line 172

   Source documentation

   Coefficient convergence also gives L² convergence for any finite absolutely continuous source. A common compact slope range follows from convergence of the finite family; boundedness of the source itself is not needed.

   theorem tendsto_mapL2Dist_affine_maximizer_maps
       {d : ℕ} {ι : Type*} [Fintype ι]
       {ρ : Measure (E d)} [IsFiniteMeasure ρ] (hρ : ρ ≪ volume)
       {y : ℕ → ι → E d} {y₀ : ι → E d}
       {c : ℕ → ι → ℝ} {c₀ : ι → ℝ}
       {T : ℕ → E d → E d} {T₀ : E d → E d}
       (hy : ∀ i, Tendsto (fun n => y n i) atTop (𝓝 (y₀ i)))
       (hc : ∀ i, Tendsto (fun n => c n i) atTop (𝓝 (c₀ i)))
       (hTm : ∀ n, Measurable (T n)) (hT₀m : Measurable T₀)
       (hT : ∀ n, ∀ᵐ x ∂ρ, ∃ i, T n x = y n i ∧
         ∀ j, inner ℝ x (y n j) + c n j ≤ inner ℝ x (y n i) + c n i)
       (hT₀ : ∀ᵐ x ∂ρ, ∃ i, T₀ x = y₀ i ∧
   …

8. theorem OAI.Problem358.map_eq_of_finite_site_law_limit line 200

   Source documentation

   Identification of an endpoint law carried by a fixed finite index measure. Different limiting indices may have the same site; their masses are automatically merged by the pushforward, so no endpoint injectivity is needed.

   theorem map_eq_of_finite_site_law_limit
       {d : ℕ} {ι : Type*} [Fintype ι] [MeasurableSpace ι]
       [MeasurableSingletonClass ι]
       {ρ : Measure (E d)} [IsFiniteMeasure ρ]
       {η : Measure ι} [IsFiniteMeasure η]
       {y : ℕ → ι → E d} {y₀ : ι → E d}
       {T : ℕ → E d → E d} {T₀ : E d → E d}
       (hy : ∀ i, Tendsto (fun n => y n i) atTop (𝓝 (y₀ i)))
       (hTm : ∀ n, Measurable (T n)) (hT₀m : Measurable T₀)
       (hlim : ∀ᵐ x ∂ρ, Tendsto (fun n => T n x) atTop (𝓝 (T₀ x)))
       (hpush : ∀ n, Measure.map (T n) ρ = Measure.map (y n) η) :
       Measure.map T₀ ρ = Measure.map y₀ η := by
   …

9. theorem OAI.Problem358.map_eq_atomic_of_finite_site_limit line 227

   Source documentation

   Explicit atomic form of endpoint-law identification. Repeated endpoint sites are allowed, so this applies at both ends of an optimal finite atomic motion.

   theorem map_eq_atomic_of_finite_site_limit
       {d : ℕ} {ι : Type*} [Fintype ι]
       {ρ : Measure (E d)} [IsFiniteMeasure ρ]
       {y : ℕ → ι → E d} {y₀ : ι → E d}
       {T : ℕ → E d → E d} {T₀ : E d → E d}
       (w : ι → ℝ≥0∞) (hw : ∑ i, w i = 1)
       (hy : ∀ i, Tendsto (fun n => y n i) atTop (𝓝 (y₀ i)))
       (hTm : ∀ n, Measurable (T n)) (hT₀m : Measurable T₀)
       (hlim : ∀ᵐ x ∂ρ, Tendsto (fun n => T n x) atTop (𝓝 (T₀ x)))
       (hpush : ∀ n, Measure.map (T n) ρ = ∑ i, w i • Measure.dirac (y n i)) :
       Measure.map T₀ ρ = ∑ i, w i • Measure.dirac (y₀ i) := by
   …

10. theorem OAI.Problem358.isUniqueQuadraticOptimalMap_uniform_of_finite_affine_repeated line 268

    Source documentation

    A finite-affine selected map is plan-uniquely optimal on a uniform convex source even when the slopes are repeated. The supporting-potential certificate avoids any choice of a merged presentation.

    theorem isUniqueQuadraticOptimalMap_uniform_of_finite_affine_repeated
        {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
        {K : Set (E d)} [IsFiniteMeasure (uniformMeasure K)]
        (hK : IsCompact K) (hne : K.Nonempty) (hconv : Convex ℝ K)
        (y : ι → E d) (c : ι → ℝ) {T : E d → E d} (hT : Measurable T)
        (hactive : ∀ᵐ x ∂uniformMeasure K, ∃ i, T x = y i ∧
          ∀ j, inner ℝ x (y j) + c j ≤ inner ℝ x (y i) + c i) :
        IsUniqueQuadraticOptimalMap (uniformMeasure K)
          (Measure.map T (uniformMeasure K)) T := by
    …

11. theorem OAI.Problem358.exists_unique_optimal_finite_affine_endpoint line 300

    Source documentation

    Coefficient limits at an endpoint of a fixed-mass finite affine motion produce an actual measurable endpoint map, its exact atomic law, plan-unique optimality, and both almost-everywhere and L² convergence. Endpoint slopes may coincide.

    theorem exists_unique_optimal_finite_affine_endpoint
        {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
        {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
        (hinterior : (interior K).Nonempty)
        {y : ℕ → ι → E d} {y₀ : ι → E d}
        {c : ℕ → ι → ℝ} {c₀ : ι → ℝ} {T : ℕ → E d → E d}
        (w : ι → ℝ≥0∞) (hw : ∑ i, w i = 1)
        (hy : ∀ i, Tendsto (fun n => y n i) atTop (𝓝 (y₀ i)))
        (hc : ∀ i, Tendsto (fun n => c n i) atTop (𝓝 (c₀ i)))
        (hTm : ∀ n, Measurable (T n))
        (hT : ∀ n, ∀ᵐ x ∂uniformMeasure K, ∃ i, T n x = y n i ∧
          ∀ j, inner ℝ x (y n j) + c n j ≤ inner ℝ x (y n i) + c n i)
    …

12. theorem OAI.Problem358.exists_unique_optimal_finite_affine_boundary line 351

    Source documentation

    A boundary value of a continuous finite-affine family has the prescribed atomic law and a plan-uniquely optimal selected map. Only the coefficient limits within the parameter set are needed, and limiting sites may coincide.

    theorem exists_unique_optimal_finite_affine_boundary
        {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
        {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
        (hinterior : (interior K).Nonempty)
        {S : Set ℝ} {t₀ : ℝ} (ht₀ : t₀ ∈ closure S)
        {y : ℝ → ι → E d} {c : ℝ → ι → ℝ}
        {T : ℝ → E d → E d}
        (w : ι → ℝ≥0∞) (hw : ∑ i, w i = 1)
        (hy : ∀ i, ContinuousWithinAt (fun t => y t i) S t₀)
        (hc : ∀ i, ContinuousWithinAt (fun t => c t i) S t₀)
        (hTm : ∀ t ∈ S, Measurable (T t))
        (hT : ∀ t ∈ S, ∀ᵐ x ∂uniformMeasure K, ∃ i, T t x = y t i ∧
    …

13. theorem OAI.Problem358.exists_unique_optimal_finite_affine_path_endpoints line 386

    Source documentation

    Continuous coefficients on a closed time interval and the fixed-mass law on its interior produce both exact endpoint maps. No injectivity or cell-mass condition is required at either endpoint.

    theorem exists_unique_optimal_finite_affine_path_endpoints
        {d : ℕ} {ι : Type*} [Fintype ι] [Nonempty ι]
        {K : Set (E d)} (hK : IsCompact K) (hconv : Convex ℝ K)
        (hinterior : (interior K).Nonempty)
        {a b : ℝ} (hab : a < b)
        {y : ℝ → ι → E d} {c : ℝ → ι → ℝ}
        {T : ℝ → E d → E d}
        (w : ι → ℝ≥0∞) (hw : ∑ i, w i = 1)
        (hy : ∀ i, ContinuousOn (fun t => y t i) (Set.Icc a b))
        (hc : ∀ i, ContinuousOn (fun t => c t i) (Set.Icc a b))
        (hTm : ∀ t ∈ Set.Ioo a b, Measurable (T t))
        (hT : ∀ t ∈ Set.Ioo a b, ∀ᵐ x ∂uniformMeasure K, ∃ i,
    …