OAI/Geometry/RCD/Sobolev/IntervalEnergyWeightLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Changing spatial weights in an interval energy integral

  1. theorem OAI.RegularPointCoordinates.integral_intervalExtension_subinterval line 13
  2. theorem OAI.RegularPointCoordinates.weighted_energy_interval_weight_tendsto line 25