OAI/Analysis/RCDHeat/HeatEntropyPath.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: HeatEntropyPath, SqrtShift, FisherSqrt, SquareClip, FisherSqrtExact.

  1. theorem OAI.RegularPointCoordinates.fisherInformation_aemeasurable line 19
  2. theorem OAI.RegularPointCoordinates.heatAt_fisher_intervalIntegrable line 25
  3. theorem OAI.RegularPointCoordinates.heatAt_fisher_integral_entropy line 34
  4. theorem OAI.RegularPointCoordinates.heatAt_entropy_ae_hasDerivAt line 54
  5. theorem OAI.RegularPointCoordinates.absolutelyContinuousOnInterval_congr line 73
  6. theorem OAI.RegularPointCoordinates.heatAt_entropy_absolutelyContinuous line 85
  7. def OAI.RegularPointCoordinates.sqrtShiftDeriv line 109
  8. def OAI.RegularPointCoordinates.sqrtShift line 110
  9. theorem OAI.RegularPointCoordinates.sqrtShiftDeriv_continuous line 111
  10. theorem OAI.RegularPointCoordinates.sqrtShiftDeriv_nonneg line 118
  11. theorem OAI.RegularPointCoordinates.sqrtShiftDeriv_le line 121
  12. theorem OAI.RegularPointCoordinates.sqrtShift_hasDerivAt line 127
  13. theorem OAI.RegularPointCoordinates.sqrtShift_lipschitz line 133
  14. theorem OAI.RegularPointCoordinates.sqrtShift_zero line 139
  15. theorem OAI.RegularPointCoordinates.sqrtShift_of_nonneg line 140
  16. theorem OAI.RegularPointCoordinates.sqrtShift_nonneg_le line 151
  17. theorem OAI.RegularPointCoordinates.integrable_sqrt_memLp line 173
  18. theorem OAI.RegularPointCoordinates.SobolevSpace.energyLp_eq_half_slope line 182
  19. theorem OAI.RegularPointCoordinates.sqrtShift_gradient_energy_le line 198
  20. theorem OAI.RegularPointCoordinates.SobolevSpace.sqrt_energy_le line 248
  21. def OAI.RegularPointCoordinates.squareClipDeriv line 294
  22. def OAI.RegularPointCoordinates.squareClip line 295
  23. theorem OAI.RegularPointCoordinates.squareClipDeriv_continuous line 296
  24. theorem OAI.RegularPointCoordinates.squareClipDeriv_bound line 299
  25. theorem OAI.RegularPointCoordinates.squareClip_hasDerivAt line 304
  26. theorem OAI.RegularPointCoordinates.squareClip_lipschitz line 309
  27. theorem OAI.RegularPointCoordinates.squareClip_zero line 315
  28. theorem OAI.RegularPointCoordinates.squareClipDeriv_eq line 316
  29. theorem OAI.RegularPointCoordinates.squareClip_eq line 319
  30. theorem OAI.RegularPointCoordinates.SobolevSpace.fisher_eq_of_sqrt line 338
  31. theorem OAI.RegularPointCoordinates.SobolevSpace.fisher_eq_eight_sqrt_energy line 395