OAI/Analysis/RCDHeat/HeatFisherSqrt.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: HeatFisherSqrt, RCDHeatConvexity, HeatHWI, WassersteinCost, HeatDissipationZero, HeatEntropyZeroPath.

  1. theorem OAI.RegularPointCoordinates.heat_fisher_eq_eight_sqrt_energy line 20
  2. theorem OAI.RegularPointCoordinates.heatMeasure_dist_sq_integrable line 53
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_entropy_convex_plan line 68
  4. theorem OAI.RegularPointCoordinates.FullCD.heat_HWI line 121
  5. def OAI.RegularPointCoordinates.wassersteinSq line 203
  6. theorem OAI.RegularPointCoordinates.wassersteinSq_le_cost line 206
  7. theorem OAI.RegularPointCoordinates.wassersteinSq_eq_cost line 210
  8. theorem OAI.RegularPointCoordinates.wassersteinSq_ne_top line 216
  9. theorem OAI.RegularPointCoordinates.regularizedFisher_aemeasurable_Ioc line 229
  10. theorem OAI.RegularPointCoordinates.heatAt_regularizedFisher_lintegral_zero line 239
  11. theorem OAI.RegularPointCoordinates.heatAt_entropy_dissipation_zero_of_finite line 293
  12. theorem OAI.RegularPointCoordinates.heatAt_entropy_dissipation_nonneg_of_finite line 320
  13. theorem OAI.RegularPointCoordinates.heatAt_entropy_dissipation_nonneg line 334
  14. theorem OAI.RegularPointCoordinates.fisherInformation_aemeasurable_nonneg line 356
  15. theorem OAI.RegularPointCoordinates.heatAt_fisher_time_finite_nonneg line 360
  16. theorem OAI.RegularPointCoordinates.heatAt_fisher_intervalIntegrable_nonneg line 368
  17. theorem OAI.RegularPointCoordinates.heatAt_fisher_integral_entropy_nonneg line 377
  18. theorem OAI.RegularPointCoordinates.heatAt_entropy_ae_hasDerivAt_nonneg line 397
  19. theorem OAI.RegularPointCoordinates.heatAt_entropy_absolutelyContinuous_nonneg line 415