OAI/Analysis/RCDHeat/WeightedDimensionalH1Square.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Cheeger energy, curvature-dimension transport and heat-flow estimates: WeightedDimensionalH1Square, WeightedDimensionalH1, VariableHeatSecant, DimensionalDualNorm.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.weighted_dimensional_H1_square_dual line 21
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.weighted_dimensional_H1_dual line 111
  3. theorem OAI.RegularPointCoordinates.heat_inner_scaled_secant line 224
  4. theorem OAI.RegularPointCoordinates.variable_heat_cutoff_dual_secant line 237
  5. theorem OAI.RegularPointCoordinates.SobolevSpace.dimensionalDual_norm_le line 291