OAI/Analysis/RCDHeat/DimensionalH1.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: DimensionalH1, DimensionalHeatSecant, WeightedLogCosh, WeightedMidpointGrid.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.dimensional_H1_dual line 21
  2. theorem OAI.RegularPointCoordinates.heat_inner_secant line 134
  3. theorem OAI.RegularPointCoordinates.compactDual_integral_density line 168
  4. theorem OAI.RegularPointCoordinates.dimensional_heat_cutoff_dual_secant line 183
  5. lemma OAI.RegularPointCoordinates.log_cosh_sqrt_lower line 234
  6. lemma OAI.RegularPointCoordinates.weighted_log_cosh line 272
  7. lemma OAI.RegularPointCoordinates.weighted_dimensional_midpoint line 284
  8. lemma OAI.RegularPointCoordinates.sum_weighted_first_difference line 304
  9. lemma OAI.RegularPointCoordinates.sum_affine_square_trapezoid line 313
  10. lemma OAI.RegularPointCoordinates.weighted_dimensional_discrete line 323
  11. lemma OAI.RegularPointCoordinates.weighted_dimensional_midpoint_grid line 344