OAI/Geometry/RCD/Transport/UniformLengthPartition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite uniform bins for bounded nonnegative transport lengths

  1. def OAI.RegularPointCoordinates.lengthBin line 12
  2. theorem OAI.RegularPointCoordinates.lengthBin_measurable line 14
  3. theorem OAI.RegularPointCoordinates.lengthBin_pairwise line 17
  4. theorem OAI.RegularPointCoordinates.mem_lengthBin_floor line 29
  5. theorem OAI.RegularPointCoordinates.lengthBin_finite_cover line 36
  6. theorem OAI.RegularPointCoordinates.bounded_length_uniform_partition line 44