OAI/Analysis/RCDHeat/EnergyChain.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: EnergyChain, IntegralPotential, HeatPotential, HeatDissipation, RegularizedLog.

  1. def OAI.RegularPointCoordinates.SobolevSpace.chainGradient line 20
  2. theorem OAI.RegularPointCoordinates.SobolevSpace.chainGradient_coe line 26
  3. theorem OAI.RegularPointCoordinates.SobolevSpace.comp_add line 37
  4. theorem OAI.RegularPointCoordinates.SobolevSpace.comp_id line 56
  5. theorem OAI.RegularPointCoordinates.SobolevSpace.chainGradient_const_add line 61
  6. theorem OAI.RegularPointCoordinates.SobolevSpace.minimalSlope_comp_C1_eq_abs line 76
  7. theorem OAI.RegularPointCoordinates.SobolevSpace.chainGradient_norm_sq line 91
  8. theorem OAI.RegularPointCoordinates.energyForm_comp_C1 line 102
  9. theorem OAI.RegularPointCoordinates.energyForm_comp_C1_integral line 130
  10. theorem OAI.RegularPointCoordinates.scalar_potential_remainder line 147
  11. def OAI.RegularPointCoordinates.integralPotential line 166
  12. theorem OAI.RegularPointCoordinates.integral_sq_Lp line 168
  13. theorem OAI.RegularPointCoordinates.integralPotential_integrable line 174
  14. theorem OAI.RegularPointCoordinates.integralPotential_remainder line 185
  15. theorem OAI.RegularPointCoordinates.integralPotential_hasFDerivAt line 215
  16. theorem OAI.RegularPointCoordinates.heatAt_integralPotential_hasDerivAt line 241
  17. theorem OAI.RegularPointCoordinates.heatGeneratorAt_continuousAt line 271
  18. theorem OAI.RegularPointCoordinates.integralPotential_continuous line 283
  19. def OAI.RegularPointCoordinates.heatDissipation line 289
  20. theorem OAI.RegularPointCoordinates.heatDissipation_continuousOn line 293
  21. theorem OAI.RegularPointCoordinates.heatAt_integralPotential_deriv_form line 300
  22. theorem OAI.RegularPointCoordinates.heatDissipation_eq_integral line 311
  23. theorem OAI.RegularPointCoordinates.heatAt_integralPotential_dissipation line 325
  24. theorem OAI.RegularPointCoordinates.heatAt_integralPotential_antitoneOn line 340
  25. def OAI.RegularPointCoordinates.regularizedLog line 358
  26. def OAI.RegularPointCoordinates.regularizedReciprocal line 359
  27. def OAI.RegularPointCoordinates.regularizedEntropy line 360
  28. theorem OAI.RegularPointCoordinates.regularizedLog_zero line 362
  29. theorem OAI.RegularPointCoordinates.regularizedLog_continuous line 365
  30. theorem OAI.RegularPointCoordinates.regularizedLog_hasDerivAt line 368
  31. theorem OAI.RegularPointCoordinates.regularizedReciprocal_continuous line 374
  32. theorem OAI.RegularPointCoordinates.regularizedReciprocal_nonneg line 379
  33. theorem OAI.RegularPointCoordinates.regularizedReciprocal_bound line 382
  34. theorem OAI.RegularPointCoordinates.regularizedLog_lipschitz line 390
  35. theorem OAI.RegularPointCoordinates.regularizedEntropy_zero line 397
  36. theorem OAI.RegularPointCoordinates.regularizedEntropy_hasDerivAt line 400
  37. theorem OAI.RegularPointCoordinates.regularizedEntropy_nonneg line 407