OAI/Analysis/RCDHeat/ForkPlans.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: ForkPlans, EntropyCoupledFork, UniformCut.

  1. lemma OAI.RegularPointCoordinates.map_le_add_of_ae_or line 22
  2. lemma OAI.RegularPointCoordinates.optimalPlan_normalize_endpoint_dom line 38
  3. lemma OAI.RegularPointCoordinates.coupled_fork_unscaled line 66
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.entropy_coupled_fork_gap line 143
  5. def OAI.RegularPointCoordinates.fairBool line 277
  6. instance OAI.RegularPointCoordinates.fairBool_probability line 279
  7. lemma OAI.RegularPointCoordinates.fairBool_singleton line 283
  8. lemma OAI.RegularPointCoordinates.fair_colors_pair line 286
  9. lemma OAI.RegularPointCoordinates.exists_finite_label_cut line 303
  10. lemma OAI.RegularPointCoordinates.exists_measurable_directed_cut line 364