OAI/Analysis/RCDHeat/StrongLimit.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: StrongLimit, StrongApply, HeatFlow, BoundedTime, DenseTendsto, HeatContinuity, ParameterizedMarkov, ConvexSum.

  1. theorem OAI.RegularPointCoordinates.bounded_cauchy_of_denseRange line 18
  2. def OAI.RegularPointCoordinates.contractionStrongLimit line 47
  3. theorem OAI.RegularPointCoordinates.contractionStrongLimit_tendsto line 54
  4. theorem OAI.RegularPointCoordinates.contractionStrongLimit_norm_le line 59
  5. theorem OAI.RegularPointCoordinates.tendsto_contraction_apply line 73
  6. def OAI.RegularPointCoordinates.heatStep line 95
  7. theorem OAI.RegularPointCoordinates.heatStep_pos line 97
  8. def OAI.RegularPointCoordinates.heatApprox line 101
  9. theorem OAI.RegularPointCoordinates.heatApprox_norm_le line 104
  10. theorem OAI.RegularPointCoordinates.heatApprox_core_cauchy line 108
  11. theorem OAI.RegularPointCoordinates.heatApprox_cauchy line 135
  12. def OAI.RegularPointCoordinates.heatFlow line 142
  13. theorem OAI.RegularPointCoordinates.heatApprox_tendsto line 146
  14. theorem OAI.RegularPointCoordinates.heatFlow_norm_le line 150
  15. theorem OAI.RegularPointCoordinates.heatFlow_zero line 153
  16. theorem OAI.RegularPointCoordinates.heatFlow_add line 160
  17. theorem OAI.RegularPointCoordinates.heatFlow_commute line 169
  18. theorem OAI.RegularPointCoordinates.expNeg_time_difference_bound line 181
  19. theorem OAI.RegularPointCoordinates.tendsto_contraction_of_denseRange line 201
  20. theorem OAI.RegularPointCoordinates.yosida_resolvent_one_norm_le line 232
  21. theorem OAI.RegularPointCoordinates.heatFlow_core_time_bound line 247
  22. theorem OAI.RegularPointCoordinates.heatFlow_core_lipschitz line 257
  23. theorem OAI.RegularPointCoordinates.heatFlow_continuous line 266
  24. theorem OAI.RegularPointCoordinates.heatFlow_tendsto_zero line 276
  25. theorem OAI.RegularPointCoordinates.SobolevSpace.resolventAt_contraction_fixed line 287
  26. theorem OAI.RegularPointCoordinates.resolventLp_nonneg line 314
  27. theorem OAI.RegularPointCoordinates.resolventLp_le_const line 329
  28. theorem OAI.RegularPointCoordinates.yosida_selfAdjoint line 343
  29. theorem OAI.RegularPointCoordinates.heatApprox_selfAdjoint line 350
  30. theorem OAI.RegularPointCoordinates.heatFlow_inner line 355
  31. theorem OAI.RegularPointCoordinates.heatFlow_selfAdjoint line 362
  32. theorem OAI.RegularPointCoordinates.convex_sum_mem_of_le_one line 370