OAI/Analysis/RCDHeat/CompactCostTransform.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: CompactCostTransform, CompactTransportEnvelope, CompactLipschitzDual, CompactDualImprovement, CompactDualAttainment.

  1. def OAI.RegularPointCoordinates.compactCostTransform line 18
  2. theorem OAI.RegularPointCoordinates.compactCostTransform_bdd line 21
  3. theorem OAI.RegularPointCoordinates.le_compactCostTransform line 29
  4. theorem OAI.RegularPointCoordinates.compactCostTransform_le line 34
  5. theorem OAI.RegularPointCoordinates.compactCostTransform_difference line 40
  6. theorem OAI.RegularPointCoordinates.compactCostTransform_lipschitz line 49
  7. theorem OAI.RegularPointCoordinates.compactCostTransform_oscillation line 67
  8. theorem OAI.RegularPointCoordinates.compactCostTransform_bounded line 80
  9. def OAI.RegularPointCoordinates.separatedSum line 110
  10. theorem OAI.RegularPointCoordinates.compact_continuous_integrable line 113
  11. theorem OAI.RegularPointCoordinates.separatedSum_integral_mono line 116
  12. def OAI.RegularPointCoordinates.transportEnvelopeValues line 131
  13. def OAI.RegularPointCoordinates.transportEnvelope line 134
  14. theorem OAI.RegularPointCoordinates.transportEnvelopeValues_nonempty line 137
  15. theorem OAI.RegularPointCoordinates.transportEnvelopeValues_bddBelow line 146
  16. theorem OAI.RegularPointCoordinates.transportEnvelope_le line 159
  17. theorem OAI.RegularPointCoordinates.transportEnvelope_separatedSum line 163
  18. theorem OAI.RegularPointCoordinates.transportEnvelope_zero line 170
  19. theorem OAI.RegularPointCoordinates.transportEnvelope_add line 175
  20. theorem OAI.RegularPointCoordinates.transportEnvelope_smul_le line 195
  21. theorem OAI.RegularPointCoordinates.transportEnvelope_smul line 210
  22. theorem OAI.RegularPointCoordinates.compact_lipschitz_bounded_cmaps line 226
  23. theorem OAI.RegularPointCoordinates.compact_dual_pair_improvement line 262
  24. theorem OAI.RegularPointCoordinates.compact_integral_lipschitz line 324
  25. theorem OAI.RegularPointCoordinates.compact_transport_dual_attainment line 342