OAI/Analysis/CircleDomains/Sobolev/SmoothCollarLowerBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Choose the smoothing accuracy before the inward circuit. Uniform variation of the fixed smooth weight and the actual starting-point law give a strictly positive boundary integral on every sufficiently small inward circuit.

  1. theorem OAI.CircleDomainRigidity.OrderedCollarLift.exists_strict_mean_lower_bound line 18