OAI/Analysis/RCDHeat/PoissonExp.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: PoissonExp, HeatMarkov, UniformContractions, HeatUniform, BoundedGeneratorRight, HeatGenerator.

  1. theorem OAI.RegularPointCoordinates.exp_smul_identity line 19
  2. theorem OAI.RegularPointCoordinates.exp_operator_poisson line 24
  3. theorem OAI.RegularPointCoordinates.poisson_weights_hasSum line 32
  4. theorem OAI.RegularPointCoordinates.poisson_operator_hasSum line 37
  5. theorem OAI.RegularPointCoordinates.exp_operator_mem_of_invariant line 46
  6. theorem OAI.RegularPointCoordinates.heatApprox_poisson line 69
  7. theorem OAI.RegularPointCoordinates.lp_upper_convex line 77
  8. theorem OAI.RegularPointCoordinates.lp_upper_closed line 89
  9. theorem OAI.RegularPointCoordinates.lp_nonneg_convex line 109
  10. theorem OAI.RegularPointCoordinates.heatApprox_nonneg line 119
  11. theorem OAI.RegularPointCoordinates.heatApprox_le_const line 127
  12. theorem OAI.RegularPointCoordinates.heatFlow_nonneg line 138
  13. theorem OAI.RegularPointCoordinates.heatFlow_le_const line 143
  14. theorem OAI.RegularPointCoordinates.heatFlow_mono line 148
  15. theorem OAI.RegularPointCoordinates.tendstoUniformlyOn_contractions_of_denseRange line 159
  16. theorem OAI.RegularPointCoordinates.tendstoUniformlyOn_contraction_apply line 188
  17. theorem OAI.RegularPointCoordinates.heatStep_tendsto line 213
  18. theorem OAI.RegularPointCoordinates.resolventLp_one_error line 216
  19. theorem OAI.RegularPointCoordinates.resolvent_heatStep_tendsto line 231
  20. theorem OAI.RegularPointCoordinates.yosida_heatStep_core_tendsto line 242
  21. def OAI.RegularPointCoordinates.heatAt line 253
  22. theorem OAI.RegularPointCoordinates.heatAt_of_nonneg line 256
  23. theorem OAI.RegularPointCoordinates.heatAt_zero line 259
  24. theorem OAI.RegularPointCoordinates.heatAt_continuous line 261
  25. theorem OAI.RegularPointCoordinates.heatAt_norm_le line 268
  26. theorem OAI.RegularPointCoordinates.heatApprox_core_error line 270
  27. theorem OAI.RegularPointCoordinates.heatApprox_uniform line 291
  28. theorem OAI.RegularPointCoordinates.expNeg_apply_hasDerivAt_right line 319
  29. theorem OAI.RegularPointCoordinates.yosida_resolvent_commute line 331
  30. theorem OAI.RegularPointCoordinates.heatApprox_resolvent_commute line 339
  31. theorem OAI.RegularPointCoordinates.heatApprox_core_hasDerivAt line 347
  32. theorem OAI.RegularPointCoordinates.heatAt_resolvent_commute line 355
  33. theorem OAI.RegularPointCoordinates.heatAt_core_hasDerivAt line 368
  34. def OAI.RegularPointCoordinates.heatCore line 382
  35. theorem OAI.RegularPointCoordinates.heatCore_toLp line 385
  36. theorem OAI.RegularPointCoordinates.heatCore_laplacian line 392
  37. theorem OAI.RegularPointCoordinates.heatCore_hasDerivAt line 400