LocalSobolevPoincare.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Poincare for the precise continuous local W1,2 representative, with its actual distributional partials and no additional line assumptions.

lemma OAI.CircleDomainRigidity.locally_sobolev_rectangular_poincare line 13