OAI/Analysis/Brenier/AffineCertificate.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem358.FiniteAffine.potential line 16

   Source documentation

   The convex potential used by a finite-affine transport map.

   def potential (y : ι → F) (c : ι → ℝ) (x : F) : ℝ :=
   …

2. def OAI.Problem358.FiniteAffine.Maximizes line 20

   Source documentation

   An index is active when its affine form dominates every other form.

   def Maximizes (y : ι → F) (c : ι → ℝ) (x : F) (i : ι) : Prop :=
   …

3. lemma OAI.Problem358.FiniteAffine.affine_le_potential line 23
4. lemma OAI.Problem358.FiniteAffine.potential_eq_iff_maximizes line 28
5. lemma OAI.Problem358.FiniteAffine.exists_maximizer line 37
6. lemma OAI.Problem358.FiniteAffine.continuous_potential line 43
7. lemma OAI.Problem358.FiniteAffine.potential_le_of_affine_le line 49
8. lemma OAI.Problem358.FiniteAffine.convexOn_potential line 53
9. lemma OAI.Problem358.FiniteAffine.potential_sub_le line 65
10. lemma OAI.Problem358.FiniteAffine.abs_potential_sub_le line 77
11. lemma OAI.Problem358.FiniteAffine.lipschitzWith_potential line 85
12. lemma OAI.Problem358.FiniteAffine.potential_add_const line 91
13. lemma OAI.Problem358.FiniteAffine.supporting_inequality line 103
14. lemma OAI.Problem358.FiniteAffine.active_slopes_monotone line 111
15. lemma OAI.Problem358.FiniteAffine.intercept_le_potential_add line 119
16. def OAI.Problem358.FiniteAffine.sourceDual line 130

    Source documentation

    The source term of the quadratic Kantorovich certificate.

    def sourceDual (y : ι → F) (c : ι → ℝ) (x : F) : ℝ :=
    …

17. def OAI.Problem358.FiniteAffine.targetDualAt line 134

    Source documentation

    The target term at a specified site.

    def targetDualAt (y : ι → F) (c : ι → ℝ) (i : ι) : ℝ :=
    …

18. lemma OAI.Problem358.FiniteAffine.dual_gap line 137
19. lemma OAI.Problem358.FiniteAffine.dual_le_cost line 144
20. lemma OAI.Problem358.FiniteAffine.dual_eq_cost_iff line 150
21. lemma OAI.Problem358.FiniteAffine.dual_eq_cost_of_maximizes line 157
22. lemma OAI.Problem358.FiniteAffine.maximizing_site_unique_of_strict line 163
23. lemma OAI.Problem358.FiniteAffine.continuous_sourceDual line 170
24. def OAI.Problem358.FiniteAffine.targetDual line 175

    Source documentation

    A Borel extension of the target term from the finite set of sites.

    def targetDual (y : ι → F) (c : ι → ℝ) (z : F) : ℝ :=
    …

25. lemma OAI.Problem358.FiniteAffine.targetDual_site line 179
26. lemma OAI.Problem358.FiniteAffine.measurable_targetDual line 187
27. lemma OAI.Problem358.FiniteAffine.integrable_targetDual line 194
28. lemma OAI.Problem358.FiniteAffine.dual_le_cost_on_range line 201
29. lemma OAI.Problem358.FiniteAffine.dual_eq_cost_on_range_iff line 209
30. theorem OAI.Problem358.FiniteAffine.maximizes_midpoint_of_symmetric_intercepts line 229

    Source documentation

    Opposite intercept perturbations cancel at the midpoint of two active cells.

    theorem maximizes_midpoint_of_symmetric_intercepts
        (y : ι → V) (c q : ι → ℝ) (s : ℝ) {x z : V} {i : ι}
        (hx : Maximizes y (fun j => c j - s * q j) x i)
        (hz : Maximizes y (fun j => c j + s * q j) z i) :
        Maximizes y c ((1 / 2 : ℝ) • (x + z)) i := by
    …

    Mentions: OAI.Problem358.FiniteAffine.Maximizes

31. theorem OAI.Problem358.FiniteAffine.midpoint_mem_cell_of_symmetric_intercepts line 241

    Source documentation

    The same inclusion restricted to a convex source body.

    theorem midpoint_mem_cell_of_symmetric_intercepts
        (y : ι → V) (c q : ι → ℝ) (s : ℝ) {K : Set V}
        (hK : Convex ℝ K) {x z : V} {i : ι}
        (hxK : x ∈ K) (hzK : z ∈ K)
        (hx : Maximizes y (fun j => c j - s * q j) x i)
        (hz : Maximizes y (fun j => c j + s * q j) z i) :
        (1 / 2 : ℝ) • (x + z) ∈ K ∧
          Maximizes y c ((1 / 2 : ℝ) • (x + z)) i := by
    …

    Mentions: OAI.Problem358.FiniteAffine.Maximizes

32. theorem OAI.Problem358.FiniteAffine.isClosed_setOf_maximizes line 253
33. theorem OAI.Problem358.FiniteAffine.le_restrict_of_ae_mem line 262

    Source documentation

    Global domination restricts to the support of the dominated measure.

    theorem le_restrict_of_ae_mem {X : Type*} [MeasurableSpace X]
        {ρ ν : Measure X} {S : Set X} (hle : ρ ≤ ν) (hS : ∀ᵐ x ∂ρ, x ∈ S) :
        ρ ≤ ν.restrict S := by
    …

34. theorem OAI.Problem358.FiniteAffine.scaled_midpoint_law_le_restrict_cell line 270

    Source documentation

    A midpoint coupling of opposite cells is supported on the middle cell, so any ambient density domination automatically restricts to that middle cell.

    theorem scaled_midpoint_law_le_restrict_cell
        [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V]
        (y : ι → V) (c q : ι → ℝ) (s : ℝ) (i : ι)
        {K : Set V} (hK : Convex ℝ K) (hKm : MeasurableSet K)
        {π : Measure (V × V)} {ν : Measure V} {γ : ℝ≥0∞}
        (hminus : ∀ᵐ p ∂π, p.1 ∈ K ∧ Maximizes y (fun j => c j - s * q j) p.1 i)
        (hplus : ∀ᵐ p ∂π, p.2 ∈ K ∧ Maximizes y (fun j => c j + s * q j) p.2 i)
        (hdom : γ • Measure.map (fun p : V × V => (1 / 2 : ℝ) • (p.1 + p.2)) π ≤ ν) :
        γ • Measure.map (fun p : V × V => (1 / 2 : ℝ) • (p.1 + p.2)) π ≤
          ν.restrict {x | x ∈ K ∧ Maximizes y c x i} := by
    …

    Mentions: OAI.Problem358.FiniteAffine.Maximizes