OAI/Analysis/RCDHeat/CDSubplan.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: CDSubplan, TransportExcess, TransportExcessVariational, GeodesicPlanCompact, TransportExcessLocalization.

  1. theorem OAI.RegularPointCoordinates.FiniteSecondMoment.of_le line 17
  2. theorem OAI.RegularPointCoordinates.FiniteSecondMoment.smul line 22
  3. theorem OAI.RegularPointCoordinates.FullCD.replace_subplan line 34
  4. def OAI.RegularPointCoordinates.transportExcessMass line 99
  5. theorem OAI.RegularPointCoordinates.transportExcessMass_zero_iff line 102
  6. theorem OAI.RegularPointCoordinates.transportExcessMass_le line 115
  7. theorem OAI.RegularPointCoordinates.transportExcessMass_eq_density line 120
  8. theorem OAI.RegularPointCoordinates.transportExcessMass_mixture line 136
  9. theorem OAI.RegularPointCoordinates.transportExcessMass_set_le line 160
  10. theorem OAI.RegularPointCoordinates.transportExcessMass_attained line 173
  11. theorem OAI.RegularPointCoordinates.transportExcessMass_le_iff_open line 199
  12. theorem OAI.RegularPointCoordinates.transportExcessMass_le_of_tendsto line 218
  13. theorem OAI.RegularPointCoordinates.lowerSemicontinuous_transportExcessMass line 232
  14. theorem OAI.RegularPointCoordinates.compact_family_minimizes_excess line 247
  15. theorem OAI.RegularPointCoordinates.isCompact_bounded_geodesics line 263
  16. theorem OAI.RegularPointCoordinates.isCompact_bounded_geodesic_plans line 313
  17. theorem OAI.RegularPointCoordinates.compression_iff_localized line 334
  18. theorem OAI.RegularPointCoordinates.localized_excess_zero_iff line 352