MeanPoincareInput.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The local L2 Poincare input used by the Euler forcing

Rajala (2012), Calc. Var. PDE 44, 477--494, Theorem 1.2 supplies the weak local Poincare inequality. The local doubling bound and the Sobolev--Poincare consequence in Hajlasz--Koskela (2000), Theorem 5.1, give this L2 specialization on a smaller ball. Eightfold interior room is retained; only bounded rescaled curvature is used. The extension from Lipschitz functions to the canonical Sobolev space is by relaxation.

def OAI.RegularPointCoordinates.LocalMeanPoincareInput line 25
Source documentation
Only approximation by one constant on an interior ball is retained from the Sobolev--Poincare inequality. This applies to arbitrary Sobolev functions, with no harmonic or Euler equation assumed.
```
def LocalMeanPoincareInput {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD