OAI/Geometry/RCD/Sobolev/RadialLocalSobolevLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local Lipschitz limits in the original Sobolev space

The radial realizations converge strongly in L2 and weakly in H1. Positive bounded weights therefore give the expected energy lower bound.

  1. theorem OAI.RegularPointCoordinates.radialLocalSobolev_L2_limit line 21
  2. theorem OAI.RegularPointCoordinates.radialLocalSobolev_weak_limit line 47