OAI/Analysis/Brenier/SharpSlices.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem358.SharpSlice.centralInterval line 12
  2. lemma OAI.Problem358.SharpSlice.centralInterval_eq_Ioo line 14
  3. lemma OAI.Problem358.SharpSlice.centralInterval_mono line 20
  4. lemma OAI.Problem358.SharpSlice.measurableSet_centralInterval line 25
  5. lemma OAI.Problem358.SharpSlice.volume_centralInterval line 29
  6. lemma OAI.Problem358.SharpSlice.volume_centralInterval_symmDiff line 35
  7. def OAI.Problem358.SharpSlice.centralSlice line 59

    Source documentation

    A central interval clipped to the source coordinate range.

    def centralSlice (r : ℝ) : Set ℝ := Icc (-1) 1 ∩ centralInterval r

    Mentions: OAI.Problem358.SharpSlice.centralInterval

  8. lemma OAI.Problem358.SharpSlice.centralSlice_eq line 61
  9. lemma OAI.Problem358.SharpSlice.volume_centralSlice line 69
  10. lemma OAI.Problem358.SharpSlice.tiltedRadius_bounds line 73
  11. lemma OAI.Problem358.SharpSlice.volume_tilted_centralSlice line 81
  12. lemma OAI.Problem358.SharpSlice.volume_centralSlice_symmDiff line 86
  13. def OAI.Problem358.SharpSlice.leftOuterSlice line 99

    Source documentation

    The negative outer cell of the sharpness map, with all ties assigned centrally.

    def leftOuterSlice (r : ℝ) : Set ℝ := Icc (-1) 1 ∩ Iio (-r)
  14. def OAI.Problem358.SharpSlice.rightOuterSlice line 102

    Source documentation

    The positive outer cell of the sharpness map, with all ties assigned centrally.

    def rightOuterSlice (r : ℝ) : Set ℝ := Icc (-1) 1 ∩ Ioi r
  15. lemma OAI.Problem358.SharpSlice.leftOuterSlice_eq_Ico line 104
  16. lemma OAI.Problem358.SharpSlice.rightOuterSlice_eq_Ioc line 113
  17. lemma OAI.Problem358.SharpSlice.volume_leftOuterSlice line 122
  18. lemma OAI.Problem358.SharpSlice.volume_rightOuterSlice line 128
  19. lemma OAI.Problem358.SharpSlice.leftOuterSlice_eq_mapRegion line 132
  20. lemma OAI.Problem358.SharpSlice.rightOuterSlice_eq_mapRegion line 148
  21. lemma OAI.Problem358.SharpSlice.volume_tilted_leftOuterSlice line 164
  22. lemma OAI.Problem358.SharpSlice.volume_tilted_rightOuterSlice line 171
  23. def OAI.Problem358.centralInterval line 190

    Source documentation

    The one-dimensional central cell in the sharpness construction.

    def centralInterval (r : ℝ) : Set ℝ := {s | |s| < r}
  24. lemma OAI.Problem358.centralInterval_eq_Ioo line 192
  25. lemma OAI.Problem358.measurableSet_centralInterval line 197
  26. lemma OAI.Problem358.centralInterval_mono line 201
  27. lemma OAI.Problem358.volume_centralInterval line 206
  28. lemma OAI.Problem358.centralInterval_subset_unit line 212
  29. lemma OAI.Problem358.restricted_volume_centralInterval line 218
  30. lemma OAI.Problem358.volume_centralInterval_symmDiff line 224
  31. lemma OAI.Problem358.restricted_volume_centralInterval_symmDiff line 245
  32. def OAI.Problem358.sharpSliceLaw line 257

    Source documentation

    The uniform probability law on the interval [-1,1].

    def sharpSliceLaw : Measure ℝ :=
…
  33. instance OAI.Problem358.sharpSliceLaw_isProbabilityMeasure line 260
  34. lemma OAI.Problem358.sharpSliceLaw_centralInterval line 268
  35. lemma OAI.Problem358.sharpSliceLaw_centralInterval_symmDiff line 275
  36. lemma OAI.Problem358.sharp_tilted_radius_bounds line 285
  37. lemma OAI.Problem358.sharpSliceLaw_tiltedCentral line 290
  38. lemma OAI.Problem358.sharpSliceLaw_tiltedSymmDiff line 296
  39. lemma OAI.Problem358.integral_sharpSliceLaw line 305
  40. lemma OAI.Problem358.integral_id_sharpSliceLaw line 311
  41. lemma OAI.Problem358.integral_affine_sharpSliceLaw line 315
  42. lemma OAI.Problem358.intervalIntegral_abs_unitInterval line 326
  43. lemma OAI.Problem358.integral_abs_sharpSliceLaw line 342
  44. lemma OAI.Problem358.integral_mul_abs_sharpSliceLaw line 346
  45. def OAI.Problem358.closedCentralInterval line 352

    Source documentation

    Closed central cells have the same slice law as open central cells.

    def closedCentralInterval (r : ℝ) : Set ℝ := {s | |s| ≤ r}
  46. lemma OAI.Problem358.closedCentralInterval_eq_Icc line 354
  47. lemma OAI.Problem358.centralInterval_ae_eq_closed line 359
  48. lemma OAI.Problem358.sharpSliceLaw_closedCentralInterval line 364
  49. lemma OAI.Problem358.sharpSliceLaw_closedCentralInterval_symmDiff line 369
  50. lemma OAI.Problem358.ae_mem_sharpSliceLaw line 377
  51. lemma OAI.Problem358.integrable_sharpSliceLaw_of_continuous line 380
  52. lemma OAI.Problem358.lintegral_tiltedRadius_sharpSliceLaw line 384
  53. lemma OAI.Problem358.lintegral_mul_abs_sharpSliceLaw line 395
  54. lemma OAI.Problem358.lintegral_affine_sharpSliceLaw line 403
  55. lemma OAI.Problem358.lintegral_centralSlices line 418
  56. lemma OAI.Problem358.lintegral_symmDiffSlices line 428
  57. lemma OAI.Problem358.lintegral_closedCentralSlices line 440
  58. lemma OAI.Problem358.lintegral_closedSymmDiffSlices line 448