OAI/Analysis/RCDHeat/MidpointEndpoint.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: MidpointEndpoint, PlanEntropyEndpoint, RawEntropyVariation, SqrtCorePlanVariation, DimensionalCore.

  1. theorem OAI.RegularPointCoordinates.dimensional_midpoint_endpoint line 19
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_plan_dimensional_endpoint line 107
  3. theorem OAI.RegularPointCoordinates.entropy_regularized_raw_plan_secant line 188
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.sqrt_core_raw_entropy_variation line 249
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compressed_plan_dimensional_core_energy line 322