OAI/Analysis/RCDHeat/EndpointCut.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: EndpointCut, EndpointPair, ConditionalUnique, Uniqueness, DensitySlab.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.no_coupled_endpoint_cut line 22
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_optimal_plan_no_endpoint_fork line 139
  3. lemma OAI.RegularPointCoordinates.measure_eq_of_conditionalPair_diagonal line 202
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_optimal_plan_unique line 230
  5. theorem OAI.RegularPointCoordinates.exists_positive_density_slab line 290
  6. theorem OAI.RegularPointCoordinates.restricted_density_slab_bounds line 324