OAI/Analysis/RCDHeat/Density.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: Density, EnergyDensity, DenseDomain, ResolventMarkov, ParameterizedResolvent.

  1. theorem OAI.RegularPointCoordinates.exists_lipschitz_eLpNorm_sub_indicator_le line 21
  2. theorem OAI.RegularPointCoordinates.MemLp.exists_lipschitz_hasCompactSupport_eLpNorm_sub_le line 84
  3. theorem OAI.RegularPointCoordinates.localSlope_eq_zero_of_notMem_tsupport line 111
  4. theorem OAI.RegularPointCoordinates.cheegerEnergy_le_slopeEnergy line 125
  5. theorem OAI.RegularPointCoordinates.slopeEnergy_lt_top_of_lipschitz_hasCompactSupport line 134
  6. theorem OAI.RegularPointCoordinates.cheegerEnergy_lt_top_of_lipschitz_hasCompactSupport line 150
  7. theorem OAI.RegularPointCoordinates.SobolevSpace.toLp_denseRange line 163
  8. theorem OAI.RegularPointCoordinates.IsWeakLaplacian.unique line 189
  9. theorem OAI.RegularPointCoordinates.energyLp_comp_contraction_le line 208
  10. def OAI.RegularPointCoordinates.SobolevSpace.compContraction line 216
  11. theorem OAI.RegularPointCoordinates.SobolevSpace.compContraction_toLp line 221
  12. theorem OAI.RegularPointCoordinates.SobolevSpace.energy_compContraction_le line 226
  13. theorem OAI.RegularPointCoordinates.SobolevSpace.resolvent_contraction_fixed line 234
  14. theorem OAI.RegularPointCoordinates.SobolevSpace.resolvent_nonneg line 259
  15. theorem OAI.RegularPointCoordinates.SobolevSpace.resolvent_le_const line 273
  16. def OAI.RegularPointCoordinates.SobolevSpace.resolventForm line 293
  17. theorem OAI.RegularPointCoordinates.SobolevSpace.resolventForm_apply line 298
  18. theorem OAI.RegularPointCoordinates.SobolevSpace.resolventForm_self line 309
  19. theorem OAI.RegularPointCoordinates.SobolevSpace.resolventForm_coercive line 315
  20. def OAI.RegularPointCoordinates.SobolevSpace.resolventAt line 335
  21. theorem OAI.RegularPointCoordinates.SobolevSpace.resolventAt_equation line 340
  22. theorem OAI.RegularPointCoordinates.SobolevSpace.resolventAt_unique line 353
  23. theorem OAI.RegularPointCoordinates.SobolevSpace.resolventAt_weak_laplacian line 366
  24. theorem OAI.RegularPointCoordinates.SobolevSpace.resolventAt_variational_identity line 376
  25. theorem OAI.RegularPointCoordinates.SobolevSpace.resolventAt_minimizes line 407
  26. theorem OAI.RegularPointCoordinates.SobolevSpace.resolventAt_norm_le line 418