OAI/Analysis/RCDHeat/Noncrossing.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: Noncrossing, ConditionalPair, ConditionalSets, InteriorSingularity, EntropyEndpoint, EntropyEndpointFork.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_optimal_plan_no_interior_crossing line 24
  2. lemma OAI.RegularPointCoordinates.conditional_identity_fiber line 98
  3. def OAI.RegularPointCoordinates.conditionalPair line 108
  4. lemma OAI.RegularPointCoordinates.conditionalPair_probability line 113
  5. lemma OAI.RegularPointCoordinates.conditionalPair_fst line 121
  6. lemma OAI.RegularPointCoordinates.conditionalPair_snd line 128
  7. lemma OAI.RegularPointCoordinates.conditionalPair_fiber line 134
  8. lemma OAI.RegularPointCoordinates.conditionalPair_set_factor line 160
  9. lemma OAI.RegularPointCoordinates.map_mutuallySingular_of_conditionalPair_diagonal line 196
  10. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_subplans_singular_at line 225
  11. lemma OAI.RegularPointCoordinates.lowerSemicontinuous_entropy_compressed_plan line 264
  12. lemma OAI.RegularPointCoordinates.NoncollapsedRCD.entropy_compressed_plan_continuousAt_zero line 286
  13. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.no_entropy_endpoint_fork line 333