OAI/Analysis/Brenier/SharpOptimality.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem358.Sharpness.slabMap_exists_maximizing_site line 14

   Source documentation

   The concrete map selects a maximizing site in the generic finite-affine interface.

   lemma slabMap_exists_maximizing_site {d : ℕ} (i j : Fin d) (a b : ℝ)
       (x : E d) :
       ∃ k : Fin 3, slabMap i j a b x = sites i j b k ∧
         FiniteAffine.Maximizes (sites i j b) (intercepts a) x k := by
   …

   Mentions: OAI.Problem358.Sharpness.slabMap, OAI.Problem358.Sharpness.sites, OAI.Problem358.FiniteAffine.Maximizes, OAI.Problem358.Sharpness.intercepts

2. lemma OAI.Problem358.Sharpness.finiteAffine_potential_eq line 26

   Source documentation

   The explicit maximum agrees with the generic finite-affine potential.

   lemma finiteAffine_potential_eq {d : ℕ} (i j : Fin d) (a b : ℝ) :
       FiniteAffine.potential (sites i j b) (intercepts a) = potential i j a b := by
   …

   Mentions: OAI.Problem358.FiniteAffine.potential, OAI.Problem358.Sharpness.sites, OAI.Problem358.Sharpness.intercepts, OAI.Problem358.Sharpness.potential

3. lemma OAI.Problem358.Sharpness.sites_eq_sharpAtoms line 38
4. lemma OAI.Problem358.Sharpness.uniformCube_isProbabilityMeasure line 41
5. lemma OAI.Problem358.Sharpness.uniformCube_isSupported line 48
6. lemma OAI.Problem358.Sharpness.uniformCube_absolutelyContinuous line 54
7. lemma OAI.Problem358.Sharpness.slabMap_compact_range line 59
8. lemma OAI.Problem358.Sharpness.slabMap_map_supported_sites line 65
9. theorem OAI.Problem358.Sharpness.slabMap_isUniqueQuadraticOptimalMap_uniform line 77

   Source documentation

   Every map in the explicit three-plane family is the unique quadratic optimal map for its law under a compact uniform probability source.

   theorem slabMap_isUniqueQuadraticOptimalMap_uniform {d : ℕ}
       (K : Set (E d)) [IsProbabilityMeasure (uniformMeasure K)] (hK : IsCompact K)
       (i j : Fin d) (hij : i ≠ j) (a b : ℝ) :
       IsUniqueQuadraticOptimalMap (uniformMeasure K)
         (Measure.map (slabMap i j a b) (uniformMeasure K)) (slabMap i j a b) := by
   …

   Mentions: OAI.Problem358.Sharpness.slabMap

10. theorem OAI.Problem358.Sharpness.slabMap_isUniqueQuadraticOptimalMap_uniformCube line 88

    Source documentation

    The unique-optimality field of the fixed-cube sharpness construction.

    theorem slabMap_isUniqueQuadraticOptimalMap_uniformCube {d : ℕ}
        (i j : Fin d) (hij : i ≠ j) (a b : ℝ) :
        IsUniqueQuadraticOptimalMap (uniformMeasure (cube d))
          (Measure.map (slabMap i j a b) (uniformMeasure (cube d))) (slabMap i j a b) := by
    …

    Mentions: OAI.Problem358.Sharpness.slabMap

11. theorem OAI.Problem358.Sharpness.slabMap_isUniqueQuadraticOptimalMap_sharpTarget line 96

    Source documentation

    An identified law immediately gives unique optimality to the named three-atom target.

    theorem slabMap_isUniqueQuadraticOptimalMap_sharpTarget (d : ℕ) (hd : 2 ≤ d)
        (a b : ℝ)
        (hpush : Measure.map (slabMap (sharpAxis0 d hd) (sharpAxis1 d hd) a b)
          (uniformMeasure (cube d)) = sharpTarget d hd a b) :
        IsUniqueQuadraticOptimalMap (uniformMeasure (cube d)) (sharpTarget d hd a b)
          (slabMap (sharpAxis0 d hd) (sharpAxis1 d hd) a b) := by
    …

    Mentions: OAI.Problem358.Sharpness.slabMap, OAI.Problem358.sharpAxis0, OAI.Problem358.sharpAxis1, OAI.Problem358.sharpTarget

12. lemma OAI.Problem358.sharpSource_ae_mem_cube line 116
13. lemma OAI.Problem358.sharpThreshold_nonneg line 121
14. lemma OAI.Problem358.uniformMeasure_cube_slab_negative line 128

    Source documentation

    The selected negative outer branch has the required probability.

    lemma uniformMeasure_cube_slab_negative {d : ℕ} (i j : Fin d) (hij : i ≠ j)
        (a b : ℝ) (hb : 0 ≤ b) (hba : b ≤ a) (hab : a + b ≤ 1) :
        uniformMeasure (cube d) {x | x ∉ Sharpness.centralCell i j a b ∧ x i < 0} =
          ENNReal.ofReal ((1-a)/2) := by
    …

    Mentions: OAI.Problem358.Sharpness.centralCell

15. lemma OAI.Problem358.uniformMeasure_cube_slab_positive line 147

    Source documentation

    The selected positive outer branch has the required probability.

    lemma uniformMeasure_cube_slab_positive {d : ℕ} (i j : Fin d) (hij : i ≠ j)
        (a b : ℝ) (hb : 0 ≤ b) (hba : b ≤ a) (hab : a + b ≤ 1) :
        uniformMeasure (cube d) {x | x ∉ Sharpness.centralCell i j a b ∧ 0 ≤ x i} =
          ENNReal.ofReal ((1-a)/2) := by
    …

    Mentions: OAI.Problem358.Sharpness.centralCell

16. lemma OAI.Problem358.map_slabMap_uniform_cube line 166

    Source documentation

    The concrete closed slab map has the explicit weighted three-site target law.

    lemma map_slabMap_uniform_cube {d : ℕ} (i j : Fin d) (hij : i ≠ j)
        (a b : ℝ) (hb : 0 ≤ b) (hba : b ≤ a) (hab : a + b ≤ 1) :
        Measure.map (Sharpness.slabMap i j a b) (uniformMeasure (cube d)) =
          ∑ k, sharpWeights a k • Measure.dirac (Sharpness.sites i j b k) := by
    …

    Mentions: OAI.Problem358.Sharpness.slabMap, OAI.Problem358.sharpWeights, OAI.Problem358.Sharpness.sites

17. lemma OAI.Problem358.map_sharpSlab_uniform_cube line 176

    Source documentation

    Target-family form used in the final sharpness example.

    lemma map_sharpSlab_uniform_cube (d : ℕ) (hd : 2 ≤ d)
        (a b : ℝ) (hb : 0 ≤ b) (hba : b ≤ a) (hab : a + b ≤ 1) :
        Measure.map (Sharpness.slabMap (sharpAxis0 d hd) (sharpAxis1 d hd) a b)
          (uniformMeasure (cube d)) = sharpTarget d hd a b := by
    …

    Mentions: OAI.Problem358.Sharpness.slabMap, OAI.Problem358.sharpAxis0, OAI.Problem358.sharpAxis1, OAI.Problem358.sharpTarget