OAI/Analysis/Brenier/AffineOptimality.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem358.finiteAffine_map_ae_mem_range line 18

   Source documentation

   An active finite-affine selection takes values in the finite site set almost everywhere.

   theorem finiteAffine_map_ae_mem_range [Nonempty ι] (y : ι → E d) (c : ι → ℝ)
       (hT : Measurable T)
       (hactive : ∀ᵐ x ∂ρ, ∃ i, T x = y i ∧ FiniteAffine.Maximizes y c x i) :
       ∀ᵐ z ∂Measure.map T ρ, z ∈ Set.range y := by
   …

   Mentions: OAI.Problem358.FiniteAffine.Maximizes

2. theorem OAI.Problem358.finiteAffine_coupling_dual_bound line 30

   Source documentation

   The pointwise finite-affine dual estimate holds under every competing coupling.

   theorem finiteAffine_coupling_dual_bound (y : ι → E d) (c : ι → ℝ)
       (hy : Function.Injective y) (hT : Measurable T)
       (hactive : ∀ᵐ x ∂ρ, ∃ i, T x = y i ∧ FiniteAffine.Maximizes y c x i)
       {π : Measure (E d × E d)} (hπ : IsCoupling ρ (Measure.map T ρ) π) :
       ∀ᵐ p ∂π, FiniteAffine.sourceDual y c p.1 +
         FiniteAffine.targetDual y c p.2 ≤ ‖p.1 - p.2‖ ^ 2 := by
   …

   Mentions: OAI.Problem358.FiniteAffine.Maximizes, OAI.Problem358.FiniteAffine.sourceDual, OAI.Problem358.FiniteAffine.targetDual

3. theorem OAI.Problem358.isQuadraticOptimalMap_of_finite_affine line 43

   Source documentation

   A measurable active selection of distinct affine sites is quadratically optimal.

   theorem isQuadraticOptimalMap_of_finite_affine
       [IsProbabilityMeasure ρ] (y : ι → E d) (c : ι → ℝ)
       (hy : Function.Injective y) (hT : Measurable T)
       (hsource : Integrable (FiniteAffine.sourceDual y c) ρ)
       (hactive : ∀ᵐ x ∂ρ, ∃ i, T x = y i ∧ FiniteAffine.Maximizes y c x i) :
       IsQuadraticOptimalMap ρ (Measure.map T ρ) T := by
   …

   Mentions: OAI.Problem358.FiniteAffine.sourceDual, OAI.Problem358.FiniteAffine.Maximizes

4. theorem OAI.Problem358.finiteAffine_dual_eq_implies_graph_ae line 61

   Source documentation

   Under an absolutely continuous source, saturation of the finite-affine certificate forces every competing plan onto the selected graph.

   theorem finiteAffine_dual_eq_implies_graph_ae
       (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
       (hρ : ρ ≪ (volume : Measure (E d))) (hT : Measurable T)
       (hactive : ∀ᵐ x ∂ρ, ∃ i, T x = y i ∧ FiniteAffine.Maximizes y c x i)
       {π : Measure (E d × E d)} (hπ : IsCoupling ρ (Measure.map T ρ) π) :
       ∀ᵐ p ∂π, FiniteAffine.sourceDual y c p.1 +
         FiniteAffine.targetDual y c p.2 = ‖p.1 - p.2‖ ^ 2 → p.2 = T p.1 := by
   …

   Mentions: OAI.Problem358.FiniteAffine.Maximizes, OAI.Problem358.FiniteAffine.sourceDual, OAI.Problem358.FiniteAffine.targetDual

5. theorem OAI.Problem358.integrable_finiteAffine_sourceDual_of_compact line 91

   Source documentation

   Compact support makes the continuous source potential integrable.

   theorem integrable_finiteAffine_sourceDual_of_compact
       [IsFiniteMeasure ρ] (y : ι → E d) (c : ι → ℝ)
       {K : Set (E d)} (hK : IsCompact K) (hρK : IsSupported ρ K) :
       Integrable (FiniteAffine.sourceDual y c) ρ := by
   …

   Mentions: OAI.Problem358.FiniteAffine.sourceDual

6. theorem OAI.Problem358.isUniqueQuadraticOptimalMap_of_finite_affine line 104

   Source documentation

   The finite-affine construction gives uniqueness among all transport plans, not merely among maps, whenever the source is absolutely continuous.

   theorem isUniqueQuadraticOptimalMap_of_finite_affine
       [IsProbabilityMeasure ρ] (y : ι → E d) (c : ι → ℝ)
       (hy : Function.Injective y) (hρ : ρ ≪ (volume : Measure (E d)))
       (hT : Measurable T) (hsource : Integrable (FiniteAffine.sourceDual y c) ρ)
       (hactive : ∀ᵐ x ∂ρ, ∃ i, T x = y i ∧ FiniteAffine.Maximizes y c x i) :
       IsUniqueQuadraticOptimalMap ρ (Measure.map T ρ) T := by
   …

   Mentions: OAI.Problem358.FiniteAffine.sourceDual, OAI.Problem358.FiniteAffine.Maximizes

7. theorem OAI.Problem358.isUniqueQuadraticOptimalMap_of_finite_affine_of_compact line 124

   Source documentation

   Compactly supported absolutely continuous probabilities admit the finite-affine optimality certificate without auxiliary integrability assumptions.

   theorem isUniqueQuadraticOptimalMap_of_finite_affine_of_compact
       [IsProbabilityMeasure ρ] (y : ι → E d) (c : ι → ℝ)
       (hy : Function.Injective y) (hρ : ρ ≪ (volume : Measure (E d)))
       {K : Set (E d)} (hK : IsCompact K) (hρK : IsSupported ρ K)
       (hT : Measurable T)
       (hactive : ∀ᵐ x ∂ρ, ∃ i, T x = y i ∧ FiniteAffine.Maximizes y c x i) :
       IsUniqueQuadraticOptimalMap ρ (Measure.map T ρ) T :=
   …

   Mentions: OAI.Problem358.FiniteAffine.Maximizes

8. theorem OAI.Problem358.isUniqueQuadraticOptimalMap_uniform_of_finite_affine line 135

   Source documentation

   Uniform compact-source specialization for the finite-affine maps used in sharpness.

   theorem isUniqueQuadraticOptimalMap_uniform_of_finite_affine
       (K : Set (E d)) [IsProbabilityMeasure (uniformMeasure K)]
       (hK : IsCompact K) (y : ι → E d) (c : ι → ℝ)
       (hy : Function.Injective y) (hT : Measurable T)
       (hactive : ∀ᵐ x ∂uniformMeasure K,
         ∃ i, T x = y i ∧ FiniteAffine.Maximizes y c x i) :
       IsUniqueQuadraticOptimalMap (uniformMeasure K)
         (Measure.map T (uniformMeasure K)) T := by
   …

   Mentions: OAI.Problem358.FiniteAffine.Maximizes

9. theorem OAI.Problem358.FiniteAffine.isQuadraticOptimalMap_of_maximizes line 156

   Source documentation

   A measurable active-site map solves the quadratic transport problem to its law.

   theorem isQuadraticOptimalMap_of_maximizes
       (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
       (ρ : Measure (E d)) [IsProbabilityMeasure ρ]
       {T : E d → E d} (hT : Measurable T)
       (hsource : Integrable (sourceDual y c) ρ)
       (hmax : ∀ᵐ x ∂ρ, ∃ i, T x = y i ∧ Maximizes y c x i) :
       IsQuadraticOptimalMap ρ (Measure.map T ρ) T := by
   …

   Mentions: OAI.Problem358.FiniteAffine.sourceDual, OAI.Problem358.FiniteAffine.Maximizes

10. theorem OAI.Problem358.FiniteAffine.isQuadraticOptimalMap_of_maximizes_of_compact line 181

    Source documentation

    Compact support supplies the dual-potential integrability automatically.

    theorem isQuadraticOptimalMap_of_maximizes_of_compact
        (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
        (ρ : Measure (E d)) [IsProbabilityMeasure ρ]
        {K : Set (E d)} (hK : IsCompact K) (hρ : IsSupported ρ K)
        {T : E d → E d} (hT : Measurable T)
        (hmax : ∀ᵐ x ∂ρ, ∃ i, T x = y i ∧ Maximizes y c x i) :
        IsQuadraticOptimalMap ρ (Measure.map T ρ) T :=
    …

    Mentions: OAI.Problem358.FiniteAffine.Maximizes

11. theorem OAI.Problem358.FiniteAffine.isUniqueQuadraticOptimalMap_of_maximizes line 192

    Source documentation

    No ties between distinct maximizing sites upgrades finite-affine optimality to plan uniqueness.

    theorem isUniqueQuadraticOptimalMap_of_maximizes
        (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
        (ρ : Measure (E d)) [IsProbabilityMeasure ρ]
        {T : E d → E d} (hT : Measurable T)
        (hsource : Integrable (sourceDual y c) ρ)
        (hmax : ∀ᵐ x ∂ρ, ∃ i, T x = y i ∧ Maximizes y c x i)
        (hunique : ∀ᵐ x ∂ρ, ∀ i j, Maximizes y c x i →
          Maximizes y c x j → y i = y j) :
        IsUniqueQuadraticOptimalMap ρ (Measure.map T ρ) T := by
    …

    Mentions: OAI.Problem358.FiniteAffine.sourceDual, OAI.Problem358.FiniteAffine.Maximizes

12. theorem OAI.Problem358.FiniteAffine.isUniqueQuadraticOptimalMap_of_maximizes_of_compact line 236

    Source documentation

    The compact-source form of the finite-affine unique-optimality criterion.

    theorem isUniqueQuadraticOptimalMap_of_maximizes_of_compact
        (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
        (ρ : Measure (E d)) [IsProbabilityMeasure ρ]
        {K : Set (E d)} (hK : IsCompact K) (hρ : IsSupported ρ K)
        {T : E d → E d} (hT : Measurable T)
        (hmax : ∀ᵐ x ∂ρ, ∃ i, T x = y i ∧ Maximizes y c x i)
        (hunique : ∀ᵐ x ∂ρ, ∀ i j, Maximizes y c x i →
          Maximizes y c x j → y i = y j) :
        IsUniqueQuadraticOptimalMap ρ (Measure.map T ρ) T :=
    …

    Mentions: OAI.Problem358.FiniteAffine.Maximizes

13. theorem OAI.Problem358.FiniteAffine.isUniqueQuadraticOptimalMap_of_maximizes_of_ac_volume line 249

    Source documentation

    For an absolutely continuous source, distinct slopes have no positive-mass ties.

    theorem isUniqueQuadraticOptimalMap_of_maximizes_of_ac_volume
        (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
        (ρ : Measure (E d)) [IsProbabilityMeasure ρ]
        {K : Set (E d)} (hK : IsCompact K) (hρ : IsSupported ρ K)
        (hac : ρ ≪ volume) {T : E d → E d} (hT : Measurable T)
        (hmax : ∀ᵐ x ∂ρ, ∃ i, T x = y i ∧ Maximizes y c x i) :
        IsUniqueQuadraticOptimalMap ρ (Measure.map T ρ) T := by
    …

    Mentions: OAI.Problem358.FiniteAffine.Maximizes

14. theorem OAI.Problem358.FiniteAffine.isUniqueQuadraticOptimalMap_uniform_of_maximizes line 262

    Source documentation

    Direct finite-affine uniqueness on a uniform compact source.

    theorem isUniqueQuadraticOptimalMap_uniform_of_maximizes
        (y : ι → E d) (c : ι → ℝ) (hy : Function.Injective y)
        {K : Set (E d)} (hK : IsCompact K)
        [IsProbabilityMeasure (uniformMeasure K)]
        {T : E d → E d} (hT : Measurable T)
        (hmax : ∀ᵐ x ∂uniformMeasure K, ∃ i, T x = y i ∧ Maximizes y c x i) :
        IsUniqueQuadraticOptimalMap (uniformMeasure K)
          (Measure.map T (uniformMeasure K)) T := by
    …

    Mentions: OAI.Problem358.FiniteAffine.Maximizes