OAI/Analysis/RCDHeat/EnergyLp.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: EnergyLp, Markov, VariationalLaplacian.

  1. def OAI.RegularPointCoordinates.energyLp line 18
  2. theorem OAI.RegularPointCoordinates.energyLp_zero line 20
  3. theorem OAI.RegularPointCoordinates.energyLp_smul line 25
  4. theorem OAI.RegularPointCoordinates.energyLp_parallelogram line 31
  5. def OAI.RegularPointCoordinates.finiteEnergy line 40
  6. def OAI.RegularPointCoordinates.SobolevSpace line 57
  7. instance OAI.RegularPointCoordinates.(instance at line 59) line 59
  8. instance OAI.RegularPointCoordinates.(instance at line 61) line 61
  9. def OAI.RegularPointCoordinates.SobolevSpace.toLp line 67
  10. def OAI.RegularPointCoordinates.SobolevSpace.energy line 69
  11. theorem OAI.RegularPointCoordinates.SobolevSpace.energy_nonneg line 72
  12. theorem OAI.RegularPointCoordinates.SobolevSpace.energy_zero line 75
  13. theorem OAI.RegularPointCoordinates.SobolevSpace.energy_smul line 78
  14. theorem OAI.RegularPointCoordinates.SobolevSpace.energy_parallelogram line 83
  15. def OAI.RegularPointCoordinates.SobolevSpace.normSq line 97
  16. theorem OAI.RegularPointCoordinates.SobolevSpace.normSq_nonneg line 100
  17. theorem OAI.RegularPointCoordinates.SobolevSpace.normSq_zero line 104
  18. theorem OAI.RegularPointCoordinates.SobolevSpace.normSq_smul line 107
  19. theorem OAI.RegularPointCoordinates.SobolevSpace.normSq_parallelogram line 113
  20. theorem OAI.RegularPointCoordinates.SobolevSpace.normSq_eq_zero line 122
  21. def OAI.RegularPointCoordinates.SobolevSpace.innerCore line 132
  22. instance OAI.RegularPointCoordinates.(instance at line 142) line 142
  23. instance OAI.RegularPointCoordinates.(instance at line 145) line 145
  24. theorem OAI.RegularPointCoordinates.energyLp_le_liminf line 149
  25. theorem OAI.RegularPointCoordinates.SobolevSpace.norm_sq line 157
  26. theorem OAI.RegularPointCoordinates.SobolevSpace.norm_toLp_le line 163
  27. def OAI.RegularPointCoordinates.SobolevSpace.toLpCLM line 170
  28. theorem OAI.RegularPointCoordinates.SobolevSpace.two_energy_le_norm_sq line 175
  29. theorem OAI.RegularPointCoordinates.SobolevSpace.energyLp_le_of_norm_le line 180
  30. theorem OAI.RegularPointCoordinates.SobolevSpace.energyLp_le_of_tendsto_of_norm_bdd line 189
  31. instance OAI.RegularPointCoordinates.(instance at line 200) line 200
  32. theorem OAI.RegularPointCoordinates.localSlope_comp_le line 246
  33. theorem OAI.RegularPointCoordinates.slopeEnergy_comp_le line 258
  34. theorem OAI.RegularPointCoordinates.IsLipschitzApproximation.memLp line 263
  35. theorem OAI.RegularPointCoordinates.IsLipschitzApproximation.comp_contraction line 270
  36. theorem OAI.RegularPointCoordinates.cheegerEnergy_comp_contraction line 287
  37. def OAI.RegularPointCoordinates.energyForm line 303
  38. theorem OAI.RegularPointCoordinates.energyForm_self line 306
  39. theorem OAI.RegularPointCoordinates.energyForm_add_left line 312
  40. theorem OAI.RegularPointCoordinates.energyForm_smul_left line 317
  41. theorem OAI.RegularPointCoordinates.energyForm_comm line 322
  42. def OAI.RegularPointCoordinates.IsWeakLaplacian line 328
  43. def OAI.RegularPointCoordinates.SobolevSpace.resolvent line 333
  44. theorem OAI.RegularPointCoordinates.SobolevSpace.resolvent_inner line 336
  45. theorem OAI.RegularPointCoordinates.SobolevSpace.resolvent_weak_laplacian line 340
  46. theorem OAI.RegularPointCoordinates.SobolevSpace.resolvent_unique line 347
  47. theorem OAI.RegularPointCoordinates.SobolevSpace.resolvent_norm_le line 357
  48. theorem OAI.RegularPointCoordinates.SobolevSpace.resolvent_variational_identity line 372
  49. theorem OAI.RegularPointCoordinates.SobolevSpace.resolvent_minimizes line 389