OAI/Analysis/RCDHeat/SobolevTestPlan.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: SobolevTestPlan, TestPlanStrongContinuity, TestPlanFlux, TestPlanInitialSlope.

  1. theorem OAI.RegularPointCoordinates.ae_deriv_le_of_integral_domination line 17
  2. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_ae_weakDerivative line 43
  3. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_testPlan line 75
  4. theorem OAI.RegularPointCoordinates.compressionPullback_norm_le line 102
  5. def OAI.RegularPointCoordinates.testPlanPullback line 114
  6. theorem OAI.RegularPointCoordinates.testPlanPullback_toLp_ae line 120
  7. theorem OAI.RegularPointCoordinates.testPlanPullback_lipschitz line 129
  8. theorem OAI.RegularPointCoordinates.lp_lipschitz_dense line 165
  9. theorem OAI.RegularPointCoordinates.testPlanPullback_jointly_continuous line 185
  10. theorem OAI.RegularPointCoordinates.testPlanPullback_continuous line 205
  11. theorem OAI.RegularPointCoordinates.testPlan_flux_continuous line 219
  12. theorem OAI.RegularPointCoordinates.testPlan_flux_fubini line 249
  13. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_integrated_subinterval line 286
  14. theorem OAI.RegularPointCoordinates.IsRelaxedSlope.testPlan_initial_bound line 305