OAI/Analysis/RCDHeat/HeatTest.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: HeatTest, RadialEnergy, MassError, MassConservation, MassExtension.

  1. theorem OAI.RegularPointCoordinates.abs_sub_le_potential_drop line 17
  2. theorem OAI.RegularPointCoordinates.weightedSlope_le_mass line 50
  3. theorem OAI.RegularPointCoordinates.heatAt_inner_lp_hasDerivAt line 73
  4. theorem OAI.RegularPointCoordinates.heatAt_inner_abs_sub_le line 82
  5. theorem OAI.RegularPointCoordinates.radialCutoff_eventually_one line 133
  6. theorem OAI.RegularPointCoordinates.integral_radialCutoff_tendsto line 140
  7. theorem OAI.RegularPointCoordinates.radialSobolevCutoff_slope_bound line 153
  8. theorem OAI.RegularPointCoordinates.radialSobolevCutoff_energy_le line 158
  9. theorem OAI.RegularPointCoordinates.lp_inner_radialCutoff line 187
  10. theorem OAI.RegularPointCoordinates.regularized_cutoff_error_le line 197
  11. theorem OAI.RegularPointCoordinates.heatAt_cutoff_mass_bound line 227
  12. theorem OAI.RegularPointCoordinates.heatAt_integral_eq_of_exponential_volume_bounded line 266
  13. theorem OAI.RegularPointCoordinates.heatAt_integral_eq_of_exponential_volume line 296
  14. theorem OAI.RegularPointCoordinates.locallyFinite_of_finiteOnBounded line 355
  15. def OAI.RegularPointCoordinates.uniformOn line 365
  16. theorem OAI.RegularPointCoordinates.uniformOn_probability line 368
  17. theorem OAI.RegularPointCoordinates.uniformOn_absolutelyContinuous line 375
  18. theorem OAI.RegularPointCoordinates.uniformOn_ae_mem line 379
  19. theorem OAI.RegularPointCoordinates.uniformOn_finiteSecondMoment line 385
  20. theorem OAI.RegularPointCoordinates.renyiIntegral_le_support_volume line 399
  21. theorem OAI.RegularPointCoordinates.uniformOn_rnDeriv line 447
  22. theorem OAI.RegularPointCoordinates.uniformOn_rnDeriv_ae line 455
  23. theorem OAI.RegularPointCoordinates.uniformOn_rnDeriv_neg_power line 464