OAI/Analysis/RCDHeat/CompactKantorovich.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: CompactKantorovich, CompactDualSlackness, CompactSquaredCost, KantorovichTestPlan, CompactOptimalPotentials.

  1. theorem OAI.RegularPointCoordinates.transportEnvelope_support line 23
  2. theorem OAI.RegularPointCoordinates.compact_transport_primal_dual line 45
  3. theorem OAI.RegularPointCoordinates.compact_coupling_separated_integral line 102
  4. theorem OAI.RegularPointCoordinates.compact_dual_slackness line 116
  5. theorem OAI.RegularPointCoordinates.compact_transport_primal_dual_attained line 137
  6. def OAI.RegularPointCoordinates.compactDistanceCost line 160
  7. def OAI.RegularPointCoordinates.compactSquaredCost line 163
  8. theorem OAI.RegularPointCoordinates.compactSquaredCost_lipschitz line 166
  9. theorem OAI.RegularPointCoordinates.compact_squared_cost_potentials line 204
  10. theorem OAI.RegularPointCoordinates.IsGeodesic.kantorovich_increment line 237
  11. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.kantorovich_action_le_pairing line 255
  12. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.kantorovich_action_le_gradient_square line 308
  13. theorem OAI.RegularPointCoordinates.compact_transportCost_integral line 340
  14. theorem OAI.RegularPointCoordinates.coupling_probability_of_fst line 349
  15. theorem OAI.RegularPointCoordinates.compact_contact_isOptimal line 355
  16. theorem OAI.RegularPointCoordinates.compact_optimal_cost_eq line 379
  17. theorem OAI.RegularPointCoordinates.IsOptimalCoupling.compact_potentials line 386