DirichletSobolevInput.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The local Sobolev input used by the Poisson construction

Hajlasz--Koskela, Sobolev met Poincare, Mem. AMS 145 (2000), no.688, Theorem5.1 (22)--(23), printed pp.22--23, and Remark3 give local normalized Sobolev inequalities under local doubling and Poincare. The displayed specialization uses the RCD local constants at bounded rescaled curvature. Zero extension from B(r) and the positive annulus B(2r)\B(r) remove the mean. Only one exponent strictly above two is needed, including n=2.

Zero-boundary coercivity combines with the local Sobolev inequality.

def OAI.RegularPointCoordinates.LocalDirichletSobolevInput line 28
Source documentation
A fixed superquadratic exponent and normalized zero-boundary Sobolev constant for small balls with a definite exterior annulus.
```
def LocalDirichletSobolevInput {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD