OAI/Analysis/RCDHeat/EntropySubsegment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: EntropySubsegment, EntropySlopeBound, EntropyPlanLipschitz, EntropyDisjointMixture, EntropyFork.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.entropy_plan_subsegment_bound line 21
  2. lemma OAI.RegularPointCoordinates.bounded_convex_four_values line 99
  3. lemma OAI.RegularPointCoordinates.bounded_semiconvex_four_values line 139
  4. theorem OAI.RegularPointCoordinates.entropy_ge_neg_twice_support_volume line 186
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.entropy_compressed_plan_lipschitz line 214
  6. theorem OAI.RegularPointCoordinates.entropy_disjoint_probability_midpoint line 272
  7. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.entropy_compressed_plan_lipschitz_uniform line 332
  8. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.entropy_fork_gap line 367