OAI/Analysis/RCDHeat/HopfTransport.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: HopfTransport, HopfPath, L2Dominated, L2LipschitzPath, HopfL2.

  1. theorem OAI.RegularPointCoordinates.coupling_of_compact_hopf_bound line 19
  2. theorem OAI.RegularPointCoordinates.hopfLax_zero_outside line 87
  3. def OAI.RegularPointCoordinates.hopfPath line 100
  4. theorem OAI.RegularPointCoordinates.hopfPath_time_lipschitz line 102
  5. theorem OAI.RegularPointCoordinates.hopfPath_space_lipschitz line 113
  6. theorem OAI.RegularPointCoordinates.hopfPath_joint_lipschitz line 117
  7. theorem OAI.RegularPointCoordinates.hopfPath_zero_outside line 134
  8. theorem OAI.RegularPointCoordinates.hopfPath_hasCompactSupport line 142
  9. theorem OAI.RegularPointCoordinates.hopfPath_eq line 151
  10. theorem OAI.RegularPointCoordinates.hopfPath_eventuallyEq line 157
  11. theorem OAI.RegularPointCoordinates.L2Differentiation.integral_sq line 171
  12. theorem OAI.RegularPointCoordinates.L2Differentiation.toLp_tendsto_of_dominated line 176
  13. theorem OAI.RegularPointCoordinates.L2Differentiation.toLp_hasDerivAt line 203
  14. theorem OAI.RegularPointCoordinates.L2Differentiation.ae_fiber_differentiable line 236
  15. theorem OAI.RegularPointCoordinates.L2Differentiation.deriv_memLp line 244
  16. theorem OAI.RegularPointCoordinates.L2Differentiation.toLp_lipschitz line 261
  17. theorem OAI.RegularPointCoordinates.L2Differentiation.ae_toLp_hasDerivAt line 287
  18. theorem OAI.RegularPointCoordinates.SobolevSpace.ofLipschitzCompact_minimalSlope_le_slope line 330
  19. theorem OAI.RegularPointCoordinates.SobolevSpace.ofLipschitzCompact_minimalSlope_le_lip line 342
  20. def OAI.RegularPointCoordinates.hopfPathSobolev line 355
  21. theorem OAI.RegularPointCoordinates.hopfPathSobolev_coe line 358
  22. theorem OAI.RegularPointCoordinates.hopfPathSobolev_lipschitz line 361
  23. theorem OAI.RegularPointCoordinates.hopfPathSobolev_ae_hasDerivAt_hj line 374