OAI/Analysis/Brenier/SharpMaps.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem358.Sharpness.centralCell line 17

   Source documentation

   The central cell of the three-plane example.

   def centralCell (i j : Fin d) (a b : ℝ) : Set (EuclideanSpace ℝ (Fin d)) :=
   …

2. def OAI.Problem358.Sharpness.outerSlope line 21

   Source documentation

   A fixed measurable choice of the outer slope.

   def outerSlope (i : Fin d) (x : EuclideanSpace ℝ (Fin d)) :
       EuclideanSpace ℝ (Fin d) :=
   …

3. def OAI.Problem358.Sharpness.slabMap line 26

   Source documentation

   A transport map selected from the maximum of -xᵢ, xᵢ and a+b*xⱼ.

   def slabMap (i j : Fin d) (a b : ℝ) (x : EuclideanSpace ℝ (Fin d)) :
       EuclideanSpace ℝ (Fin d) := by
   …

4. lemma OAI.Problem358.Sharpness.measurableSet_centralCell line 31
5. lemma OAI.Problem358.Sharpness.measurable_outerSlope line 36
6. lemma OAI.Problem358.Sharpness.measurable_slabMap line 42
7. lemma OAI.Problem358.Sharpness.norm_outerSlope line 46
8. lemma OAI.Problem358.Sharpness.norm_sq_single_sub_single line 51
9. lemma OAI.Problem358.Sharpness.norm_sq_outerSlope_sub_single line 56
10. lemma OAI.Problem358.Sharpness.single_zero line 62
11. lemma OAI.Problem358.Sharpness.slabMap_norm_sq_difference line 67

    Source documentation

    The exact pointwise cost identity for the sharpness construction.

    lemma slabMap_norm_sq_difference (i j : Fin d) (hij : i ≠ j)
        (a b : ℝ) (x : EuclideanSpace ℝ (Fin d)) :
        ‖slabMap i j a 0 x - slabMap i j a b x‖ ^ 2 =
          (centralCell i j a 0 ∆ centralCell i j a b).indicator (fun _ => (1 : ℝ)) x +
          (centralCell i j a b).indicator (fun _ => b ^ 2) x := by
    …

    Mentions: OAI.Problem358.Sharpness.slabMap, OAI.Problem358.Sharpness.centralCell

12. def OAI.Problem358.Sharpness.sites line 82

    Source documentation

    The three site vectors, ordered negative/positive/central.

    def sites (i j : Fin d) (b : ℝ) : Fin 3 → EuclideanSpace ℝ (Fin d) :=
    …

13. def OAI.Problem358.Sharpness.intercepts line 86

    Source documentation

    The corresponding affine intercepts.

    def intercepts (a : ℝ) : Fin 3 → ℝ := ![0, 0, a]

14. def OAI.Problem358.Sharpness.potential line 89

    Source documentation

    The maximum of the three affine branches.

    def potential (i j : Fin d) (a b : ℝ) (x : EuclideanSpace ℝ (Fin d)) : ℝ :=
    …

15. lemma OAI.Problem358.Sharpness.inner_outerSlope line 92
16. lemma OAI.Problem358.Sharpness.site_affine_le_potential line 99
17. lemma OAI.Problem358.Sharpness.exists_active_site line 110

    Source documentation

    Everywhere, the selected slope is one of the three active affine branches.

    lemma exists_active_site (i j : Fin d) (a b : ℝ)
        (x : EuclideanSpace ℝ (Fin d)) :
        ∃ k : Fin 3, slabMap i j a b x = sites i j b k ∧
          potential i j a b x = inner ℝ (sites i j b k) x + intercepts a k := by
    …

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

18. lemma OAI.Problem358.Sharpness.slabMap_supporting line 132
19. lemma OAI.Problem358.Sharpness.sites_injective line 142

    Source documentation

    The three sites are distinct whenever the coordinate directions are distinct.

    lemma sites_injective (i j : Fin d) (hij : i ≠ j) (b : ℝ) :
        Function.Injective (sites i j b) := by
    …

    Mentions: OAI.Problem358.Sharpness.sites

20. lemma OAI.Problem358.Sharpness.site_eq_slabMap_of_active line 152

    Source documentation

    Away from the two slanted boundary hyperplanes, the active slope is unique. The positive-threshold assumption excludes the tie between the two outer branches.

    lemma site_eq_slabMap_of_active (i j : Fin d) (a b : ℝ)
        (x : EuclideanSpace ℝ (Fin d)) (hq : 0 < a + b * x j)
        (htie : |x i| ≠ a + b * x j) (k : Fin 3)
        (hk : inner ℝ (sites i j b k) x + intercepts a k = potential i j a b x) :
        sites i j b k = slabMap i j a b x := by
    …

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

21. def OAI.Problem358.Sharpness.slabIndex line 194

    Source documentation

    A finite label for the cell partition and its pushforward law.

    def slabIndex (i j : Fin d) (a b : ℝ) (x : EuclideanSpace ℝ (Fin d)) : Fin 3 := by
    …

22. lemma OAI.Problem358.Sharpness.slabMap_eq_sites_slabIndex line 198
23. lemma OAI.Problem358.Sharpness.slabMap_eq_site_iff line 205
24. lemma OAI.Problem358.Sharpness.slabMap_mem_range_sites line 211
25. lemma OAI.Problem358.Sharpness.slabIndex_eq_two_iff line 216
26. lemma OAI.Problem358.Sharpness.slabIndex_eq_zero_iff line 224
27. lemma OAI.Problem358.Sharpness.slabIndex_eq_one_iff line 245
28. lemma OAI.Problem358.Sharpness.threshold_bounds line 265
29. lemma OAI.Problem358.Sharpness.norm_sites_le_one line 270
30. lemma OAI.Problem358.Sharpness.abs_sites_coordinate_le_one line 277
31. lemma OAI.Problem358.Sharpness.continuous_potential line 282
32. lemma OAI.Problem358.Sharpness.integral_slabMap_norm_sq_difference line 289

    Source documentation

    Integration reduces the map-distance computation to the masses of two cells.

    lemma integral_slabMap_norm_sq_difference (i j : Fin d) (hij : i ≠ j) (a b : ℝ)
        (ρ : Measure (EuclideanSpace ℝ (Fin d))) [IsFiniteMeasure ρ] :
        (∫ x, ‖slabMap i j a 0 x - slabMap i j a b x‖ ^ 2 ∂ρ) =
          (ρ (centralCell i j a 0 ∆ centralCell i j a b)).toReal +
            b ^ 2 * (ρ (centralCell i j a b)).toReal := by
    …

    Mentions: OAI.Problem358.Sharpness.slabMap, OAI.Problem358.Sharpness.centralCell

33. lemma OAI.Problem358.Sharpness.potential_eq_finiteAffine line 310
34. lemma OAI.Problem358.Sharpness.exists_maximizes_site line 322
35. lemma OAI.Problem358.Sharpness.slabIndex_maximizes line 331
36. lemma OAI.Problem358.Sharpness.eq_slabMap_of_maximizes line 339
37. def OAI.Problem358.Sharpness.slabSelector line 360

    Source documentation

    The selected branch, with central branches taking precedence on ties.

    def slabSelector (i j : Fin d) (a b : ℝ) (x : E d) : Fin 3 := by
    …

38. lemma OAI.Problem358.Sharpness.measurable_slabSelector line 364
39. lemma OAI.Problem358.Sharpness.slabMap_eq_sites_selector line 371
40. lemma OAI.Problem358.Sharpness.slabSelector_preimage_zero line 378
41. lemma OAI.Problem358.Sharpness.slabSelector_preimage_one line 385
42. lemma OAI.Problem358.Sharpness.slabSelector_preimage_two line 392
43. lemma OAI.Problem358.Sharpness.map_slabMap_of_cell_masses line 400

    Source documentation

    Exact cell masses immediately determine the pushforward law of the slab map.

    lemma map_slabMap_of_cell_masses (ρ : Measure (E d)) (i j : Fin d) (a b : ℝ)
        (hneg : ρ {x | x ∉ centralCell i j a b ∧ x i < 0} = ENNReal.ofReal ((1-a)/2))
        (hpos : ρ {x | x ∉ centralCell i j a b ∧ 0 ≤ x i} = ENNReal.ofReal ((1-a)/2))
        (hcent : ρ (centralCell i j a b) = ENNReal.ofReal a) :
        Measure.map (slabMap i j a b) ρ =
          ∑ k, sharpWeights a k • Measure.dirac (sites i j b k) := by
    …

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

44. lemma OAI.Problem358.sharpAtoms_eq_sites line 429
45. lemma OAI.Problem358.sharpAxis_ne line 432
46. lemma OAI.Problem358.map_slabMap_eq_sharpTarget_of_cell_masses line 436

    Source documentation

    The branch law in the target-family notation used by the sharpness theorem.

    lemma map_slabMap_eq_sharpTarget_of_cell_masses (d : ℕ) (hd : 2 ≤ d)
        (ρ : Measure (E d)) (a b : ℝ)
        (hneg : ρ {x | x ∉ Sharpness.centralCell (sharpAxis0 d hd) (sharpAxis1 d hd) a b ∧
          x (sharpAxis0 d hd) < 0} = ENNReal.ofReal ((1-a)/2))
        (hpos : ρ {x | x ∉ Sharpness.centralCell (sharpAxis0 d hd) (sharpAxis1 d hd) a b ∧
          0 ≤ x (sharpAxis0 d hd)} = ENNReal.ofReal ((1-a)/2))
        (hcent : ρ (Sharpness.centralCell (sharpAxis0 d hd) (sharpAxis1 d hd) a b) =
          ENNReal.ofReal a) :
        Measure.map (Sharpness.slabMap (sharpAxis0 d hd) (sharpAxis1 d hd) a b) ρ =
          sharpTarget d hd a b := by
    …

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