OAI/Analysis/RCDHeat/HeatH1.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: HeatH1, HeatFormDerivative, HeatJensen, CarrePositive, StrongEnergyDensity.

  1. theorem OAI.RegularPointCoordinates.heatAt_of_nonpos line 20
  2. def OAI.RegularPointCoordinates.heatH1 line 24
  3. theorem OAI.RegularPointCoordinates.heatH1_toLp line 27
  4. theorem OAI.RegularPointCoordinates.heatH1_energy_le line 33
  5. theorem OAI.RegularPointCoordinates.heatH1_norm_le line 40
  6. def OAI.RegularPointCoordinates.heatH1Map line 51
  7. theorem OAI.RegularPointCoordinates.heatH1Map_norm_le line 68
  8. theorem OAI.RegularPointCoordinates.heatH1_core line 73
  9. theorem OAI.RegularPointCoordinates.heatH1_continuous line 80
  10. theorem OAI.RegularPointCoordinates.heatH1_zero line 95
  11. theorem OAI.RegularPointCoordinates.heatH1_add line 98
  12. theorem OAI.RegularPointCoordinates.energyForm_continuous line 110
  13. theorem OAI.RegularPointCoordinates.heatAt_inner_hasDerivAt line 119
  14. theorem OAI.RegularPointCoordinates.heatAt_inner_hasDerivWithinAt_zero line 128
  15. theorem OAI.RegularPointCoordinates.heatAt_form_limit line 148
  16. theorem OAI.RegularPointCoordinates.heatAt_nonneg line 163
  17. theorem OAI.RegularPointCoordinates.heatAt_le_const line 166
  18. theorem OAI.RegularPointCoordinates.heatAt_abs_le_const line 170
  19. theorem OAI.RegularPointCoordinates.heatAt_jensen_square line 185
  20. theorem OAI.RegularPointCoordinates.heatAt_square_increment_nonneg line 214
  21. theorem OAI.RegularPointCoordinates.lp_inner_nonneg line 229
  22. theorem OAI.RegularPointCoordinates.SobolevSpace.inner_product_swap line 237
  23. theorem OAI.RegularPointCoordinates.SobolevSpace.inner_square_product line 251
  24. def OAI.RegularPointCoordinates.carrePair line 266
  25. theorem OAI.RegularPointCoordinates.heatH1_abs_le_const line 272
  26. theorem OAI.RegularPointCoordinates.heatAt_carre_increment_nonneg line 278
  27. theorem OAI.RegularPointCoordinates.carrePair_nonneg line 315
  28. theorem OAI.RegularPointCoordinates.SobolevSpace.eventually_energy_gt line 342
  29. theorem OAI.RegularPointCoordinates.SobolevSpace.tendsto_of_toLp_tendsto_energy_le line 360
  30. theorem OAI.RegularPointCoordinates.SobolevSpace.exists_strong_lipschitz_recovery line 396