OAI/Analysis/RCDHeat/EVIConvexity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: EVIConvexity, StrongEntropySegment, DensityEntropyBounds, StrongEntropyPlan.

  1. theorem OAI.RegularPointCoordinates.nonneg_of_boundary_min_integrated_bound line 19
  2. theorem OAI.RegularPointCoordinates.weighted_dist_sq_lower line 58
  3. theorem OAI.RegularPointCoordinates.metric_segment_convexity_of_integrated_evi line 70
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.entropy_convexity_bounded_segment line 137
  5. theorem OAI.RegularPointCoordinates.entropy_le_log_density_bound line 238
  6. theorem OAI.RegularPointCoordinates.log_density_floor_lt_entropy line 258
  7. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.entropy_convexity_bounded_plan_marginal line 288
  8. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.entropy_plan_marginal_le_log_capacity line 331