OAI/Geometry/RCD/Sobolev/WeightedEnergyWeightLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Stability of weighted Sobolev energy under bounded weight convergence

First use domination by the fixed gradient pairing in space, then the uniform Sobolev norm bound in time. No joint pointwise gradient field is assumed.

  1. theorem OAI.RegularPointCoordinates.weightedGamma_weight_tendsto line 19
  2. theorem OAI.RegularPointCoordinates.weighted_energy_time_weight_tendsto line 36