OAI/Analysis/RCDHeat/Foundations.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates.

  1. abbrev OAI.RegularPointCoordinates.Euclidean line 27
  2. abbrev OAI.RegularPointCoordinates.Time line 28
  3. def OAI.RegularPointCoordinates.IsGeodesic line 31
  4. def OAI.RegularPointCoordinates.IsGeodesicSpace line 35
  5. def OAI.RegularPointCoordinates.hausdorff line 39
  6. def OAI.RegularPointCoordinates.localSlope line 45
  7. def OAI.RegularPointCoordinates.IsLipschitzApproximation line 51
  8. def OAI.RegularPointCoordinates.cheegerEnergy line 58
  9. def OAI.RegularPointCoordinates.QuadraticCheegerEnergy line 64
  10. def OAI.RegularPointCoordinates.FiniteSecondMoment line 71
  11. def OAI.RegularPointCoordinates.transportCost line 76
  12. def OAI.RegularPointCoordinates.IsOptimalCoupling line 81
  13. def OAI.RegularPointCoordinates.sigma line 90
  14. def OAI.RegularPointCoordinates.tau line 101
  15. def OAI.RegularPointCoordinates.renyiIntegral line 107
  16. def OAI.RegularPointCoordinates.FullCD line 113
  17. structure OAI.RegularPointCoordinates.NoncollapsedRCD line 132
  18. def OAI.RegularPointCoordinates.IsPointedApproximation line 144
  19. def OAI.RegularPointCoordinates.RescalingsConverge line 154
  20. def OAI.RegularPointCoordinates.IsTangent line 160
  21. def OAI.RegularPointCoordinates.IsRegular line 167
  22. def OAI.RegularPointCoordinates.HasOpenBilipschitzChart line 174
  23. theorem OAI.RegularPointCoordinates.localSlope_const line 186
  24. theorem OAI.RegularPointCoordinates.localSlope_const_mul line 193
  25. theorem OAI.RegularPointCoordinates.localSlope_le_of_lipschitz line 204
  26. theorem OAI.RegularPointCoordinates.cheegerEnergy_zero line 216
  27. theorem OAI.RegularPointCoordinates.IsLipschitzApproximation.const_mul line 228
  28. def OAI.RegularPointCoordinates.slopeEnergy line 252
  29. theorem OAI.RegularPointCoordinates.slopeEnergy_const_mul line 255
  30. theorem OAI.RegularPointCoordinates.cheegerEnergy_le_liminf line 261
  31. theorem OAI.RegularPointCoordinates.cheegerEnergy_const_mul_le line 266
  32. theorem OAI.RegularPointCoordinates.cheegerEnergy_const_mul line 289
  33. theorem OAI.RegularPointCoordinates.IsLipschitzApproximation.congr_ae line 309
  34. theorem OAI.RegularPointCoordinates.cheegerEnergy_congr_ae line 322
  35. theorem OAI.RegularPointCoordinates.QuadraticCheegerEnergy.finite_add line 332
  36. theorem OAI.RegularPointCoordinates.QuadraticCheegerEnergy.finite_sub line 342
  37. theorem OAI.RegularPointCoordinates.exists_lipschitzApproximation_of_energy_lt line 354
  38. theorem OAI.RegularPointCoordinates.cheegerEnergy_le_of_lipschitz_approximants line 367
  39. theorem OAI.RegularPointCoordinates.cheegerEnergy_le_liminf_of_L2 line 383
  40. def OAI.RegularPointCoordinates.EnergyPolarization.bracket line 421
  41. theorem OAI.RegularPointCoordinates.EnergyPolarization.neg line 424
  42. theorem OAI.RegularPointCoordinates.EnergyPolarization.bracket_self line 429
  43. theorem OAI.RegularPointCoordinates.EnergyPolarization.bracket_symm line 437
  44. theorem OAI.RegularPointCoordinates.EnergyPolarization.bracket_add_left line 444
  45. theorem OAI.RegularPointCoordinates.EnergyPolarization.bracket_abs_le line 456
  46. theorem OAI.RegularPointCoordinates.EnergyPolarization.bracket_smul_left line 465
  47. def OAI.RegularPointCoordinates.EnergyPolarization.preInner line 484