OAI/Analysis/RCDHeat/WeightedHilbert.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: WeightedHilbert, DaviesLower, ScalarGronwall, DaviesHeat, RadialWeight, WeightedIntegral, HeatExponential, VolumeExponential.

  1. theorem OAI.RegularPointCoordinates.lpMultiplier_inner_symm line 23
  2. theorem OAI.RegularPointCoordinates.lpMultiplier_inner_nonneg line 31
  3. theorem OAI.RegularPointCoordinates.lpMultiplier_abs_inner line 42
  4. theorem OAI.RegularPointCoordinates.weighted_square_lower line 54
  5. theorem OAI.RegularPointCoordinates.energyForm_weight_lower line 74
  6. theorem OAI.RegularPointCoordinates.growth_le_exp line 90
  7. theorem OAI.RegularPointCoordinates.heatAt_weighted_hasDerivAt line 121
  8. theorem OAI.RegularPointCoordinates.heatAt_weighted_bound line 138
  9. def OAI.RegularPointCoordinates.radialWeight line 169
  10. theorem OAI.RegularPointCoordinates.radialWeight_nonneg line 172
  11. theorem OAI.RegularPointCoordinates.radialWeight_bound line 175
  12. theorem OAI.RegularPointCoordinates.radialWeight_lipschitz line 180
  13. theorem OAI.RegularPointCoordinates.radialWeight_slope line 199
  14. theorem OAI.RegularPointCoordinates.radialWeight_constant_outside line 222
  15. theorem OAI.RegularPointCoordinates.lpMultiplier_integral_sq line 233
  16. theorem OAI.RegularPointCoordinates.heatAt_radialWeight_integral line 250
  17. theorem OAI.RegularPointCoordinates.heatAt_radialWeight_integral_le line 269
  18. theorem OAI.RegularPointCoordinates.heatAt_exponential_square_lintegral_le line 298
  19. theorem OAI.RegularPointCoordinates.integrable_exp_neg_dist_of_volume line 335
  20. theorem OAI.RegularPointCoordinates.integrable_dist_pow_mul_exp line 384