OAI/Analysis/RCDHeat/VariableHeatQuadratic.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: VariableHeatQuadratic, GeometricAELimit, HeatTwoSidedRemainder, HeatGeometricTime, HeatTimeCurve, VariableGeometricIncrement.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.variable_heat_slope_quadratic_bound line 19
  2. theorem OAI.RegularPointCoordinates.ae_tendsto_of_summable_L2_norm line 93
  3. theorem OAI.RegularPointCoordinates.ae_tendsto_of_geometric_L2_norm line 102
  4. theorem OAI.RegularPointCoordinates.ae_tendsto_of_eventually_geometric_L2_norm line 110
  5. theorem OAI.RegularPointCoordinates.heatAt_twoSided_remainder line 131
  6. theorem OAI.RegularPointCoordinates.heatAt_time_norm_sub_le line 163
  7. theorem OAI.RegularPointCoordinates.heatAt_geometric_time_tendsto_ae line 176
  8. theorem OAI.RegularPointCoordinates.heatAt_geometric_secant_tendsto_ae line 198
  9. def OAI.RegularPointCoordinates.heatKernelIntegral line 248
  10. theorem OAI.RegularPointCoordinates.heatKernelIntegral_continuous line 251
  11. theorem OAI.RegularPointCoordinates.heatKernelIntegral_one line 256
  12. theorem OAI.RegularPointCoordinates.geometric_square_time_limits line 261
  13. theorem OAI.RegularPointCoordinates.geometric_square_time_bound line 275
  14. theorem OAI.RegularPointCoordinates.geometric_heat_factors_tendsto line 287
  15. theorem OAI.RegularPointCoordinates.geometric_increment_algebra line 319
  16. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.variable_geometric_increment line 325