OAI/Analysis/RCDHeat/BidirectionalPotential.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: BidirectionalPotential, CompactSobolevDual, DimensionalCoreDual, DimensionalDualLimit, DimensionalH1Square.

  1. theorem OAI.RegularPointCoordinates.IsOptimalCoupling.bidirectional_sobolev_potential line 23
  2. structure OAI.RegularPointCoordinates.CompactSobolevDual line 119
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.dimensional_core_dual line 150
  4. def OAI.RegularPointCoordinates.CompactSobolevDual.flip line 224
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.dimensional_dual_limit line 245
  6. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.dimensional_H1_square_dual line 335