OAI/Geometry/RCD/Transport/TestPlanIntervalFlux.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Flux and initial slope at every interior time of a geodesic plan

  1. theorem OAI.RegularPointCoordinates.testPlan_flux_fubini_interval line 14
  2. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_integrated_interval line 43
  3. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_right_slope_bound line 60