OAI/Analysis/RCDHeat/DimensionalCompactWeightedGradient.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: DimensionalCompactWeightedGradient, DimensionalWeightedGradient, CoefficientLimit, HeatGeneratorComposition, DimensionalHeatBochner.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.dimensional_compact_weighted_gradient line 20
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.dimensional_weighted_gradient line 115
  3. theorem OAI.RegularPointCoordinates.heatDimensionCoefficient_div_tendsto line 165
  4. theorem OAI.RegularPointCoordinates.heatGeneratorAt_comp_heat line 200
  5. theorem OAI.RegularPointCoordinates.heatGeneratorAt_comp_heat_tendsto line 214
  6. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.dimensional_heat_weak_bochner line 235