OAI/Analysis/RCDHeat/CompactTransportVariation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: CompactTransportVariation, WeightedPairLinear, EntropyKantorovich, OptimalSubcoupling, OptimalSubplan.

  1. theorem OAI.RegularPointCoordinates.compact_optimal_plan_signed_variation line 21
  2. theorem OAI.RegularPointCoordinates.convex_directional_derivative_add line 59
  3. theorem OAI.RegularPointCoordinates.weightedGradientPair_add_right line 90
  4. theorem OAI.RegularPointCoordinates.weightedGradientPair_smul_right line 100
  5. theorem OAI.RegularPointCoordinates.weightedGradientPair_reference line 117
  6. theorem OAI.RegularPointCoordinates.planInitialSecant_congr_ae line 147
  7. theorem OAI.RegularPointCoordinates.entropy_plan_signed_derivative_le line 161
  8. theorem OAI.RegularPointCoordinates.compact_entropy_plan_kantorovich_bound line 204
  9. theorem OAI.RegularPointCoordinates.transportCost_add line 265
  10. theorem OAI.RegularPointCoordinates.IsOptimalCoupling.subcoupling line 271
  11. theorem OAI.RegularPointCoordinates.IsOptimalCoupling.replace_subcoupling line 292
  12. theorem OAI.RegularPointCoordinates.transportCost_smul line 309
  13. theorem OAI.RegularPointCoordinates.IsOptimalCoupling.smul line 313
  14. theorem OAI.RegularPointCoordinates.optimalPlan_replace_subplan line 338