OAI/Geometry/RCD/Transport/ShortPlanFlux.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform flux bounds for short compressed transport plans

  1. theorem OAI.RegularPointCoordinates.testPlan_flux_eq_inner line 17
  2. theorem OAI.RegularPointCoordinates.short_plan_flux_le line 33
  3. theorem OAI.RegularPointCoordinates.short_plan_absolute_increment_le line 57