OAI/Analysis/RCDHeat/CouplingRepair.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: CouplingRepair, RetainedCoupling, RetainedConvergence, CouplingCost, DensityCouplingRecovery, CompactSobolevDescent.

  1. theorem OAI.RegularPointCoordinates.coupling_repair line 18
  2. theorem OAI.RegularPointCoordinates.map_withDensity_pullback line 61
  3. def OAI.RegularPointCoordinates.retainedFraction line 70
  4. theorem OAI.RegularPointCoordinates.retainedFraction_le line 71
  5. theorem OAI.RegularPointCoordinates.retainedFraction_mul line 72
  6. theorem OAI.RegularPointCoordinates.retainedFraction_measurable line 77
  7. theorem OAI.RegularPointCoordinates.retainedCoupling_le line 79
  8. theorem OAI.RegularPointCoordinates.retainedCoupling_fst line 84
  9. theorem OAI.RegularPointCoordinates.retainedFraction_tendsto line 102
  10. theorem OAI.RegularPointCoordinates.retainedCoupling_fraction_tendsto line 109
  11. theorem OAI.RegularPointCoordinates.withDensity_complement_add line 121
  12. theorem OAI.RegularPointCoordinates.complement_lintegral_tendsto_zero line 130
  13. theorem OAI.RegularPointCoordinates.transportCost_le_marginal_moments line 157
  14. theorem OAI.RegularPointCoordinates.equalMass_product_marginals line 178
  15. theorem OAI.RegularPointCoordinates.equalMass_product_cost_le line 191
  16. theorem OAI.RegularPointCoordinates.density_coupling_recovery line 208
  17. theorem OAI.RegularPointCoordinates.FullCD.compact_sobolev_HWI line 333