OAI/Analysis/RCDHeat/UniformBoundedApply.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: UniformBoundedApply, HeatDifferentiable, HeatEVI, LipschitzCalculus, SobolevAlgebra.

  1. theorem OAI.RegularPointCoordinates.tendstoUniformlyOn_bounded_apply line 20
  2. def OAI.RegularPointCoordinates.heatGeneratorAt line 43
  3. theorem OAI.RegularPointCoordinates.heatGeneratorAt_of_pos line 46
  4. theorem OAI.RegularPointCoordinates.heatGeneratorAt_norm_le_of_ge line 49
  5. theorem OAI.RegularPointCoordinates.heatAt_hasDerivAt line 56
  6. theorem OAI.RegularPointCoordinates.heatGenerator_add line 76
  7. theorem OAI.RegularPointCoordinates.energyForm_sub_right line 95
  8. theorem OAI.RegularPointCoordinates.SobolevSpace.energy_sub_eq line 100
  9. theorem OAI.RegularPointCoordinates.heatAt_dist_sq_hasDerivAt line 109
  10. theorem OAI.RegularPointCoordinates.heatAt_evi line 125
  11. def OAI.RegularPointCoordinates.heatTail line 132
  12. theorem OAI.RegularPointCoordinates.heatTail_toLp line 135
  13. theorem OAI.RegularPointCoordinates.heatTail_eq line 142
  14. theorem OAI.RegularPointCoordinates.heatTail_hasDerivAt line 147
  15. theorem OAI.RegularPointCoordinates.heatTail_deriv_toLp line 154
  16. theorem OAI.RegularPointCoordinates.heatAt_energy_hasDerivAt line 164
  17. theorem OAI.RegularPointCoordinates.localSlope_comp_lipschitz line 186
  18. theorem OAI.RegularPointCoordinates.slopeEnergy_comp_lipschitz line 213
  19. theorem OAI.RegularPointCoordinates.IsLipschitzApproximation.comp_lipschitz line 225
  20. theorem OAI.RegularPointCoordinates.cheegerEnergy_comp_lipschitz line 246
  21. theorem OAI.RegularPointCoordinates.cheegerEnergy_comp_lipschitz_ne_top line 272
  22. def OAI.RegularPointCoordinates.clipReal line 281
  23. theorem OAI.RegularPointCoordinates.clipReal_lipschitz line 283
  24. theorem OAI.RegularPointCoordinates.clipReal_eq_self line 286
  25. theorem OAI.RegularPointCoordinates.clipReal_abs_le line 289
  26. theorem OAI.RegularPointCoordinates.clipReal_zero line 293
  27. theorem OAI.RegularPointCoordinates.clipReal_sq_lipschitz line 296
  28. def OAI.RegularPointCoordinates.SobolevSpace.comp line 312
  29. theorem OAI.RegularPointCoordinates.SobolevSpace.comp_coe line 319
  30. theorem OAI.RegularPointCoordinates.SobolevSpace.comp_energy_le line 324
  31. def OAI.RegularPointCoordinates.SobolevSpace.square line 338
  32. theorem OAI.RegularPointCoordinates.SobolevSpace.square_coe line 341
  33. theorem OAI.RegularPointCoordinates.SobolevSpace.square_energy_le line 349
  34. def OAI.RegularPointCoordinates.SobolevSpace.product line 360
  35. theorem OAI.RegularPointCoordinates.SobolevSpace.product_coe line 364