OAI/Analysis/CircleDomains/Sobolev/DifferentiableCriticalPieces.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

At critical differentiability points the linear-approximation partition has arbitrarily small Lipschitz constant on each measurable piece.

  1. lemma OAI.CircleDomainRigidity.differentiable_critical_pieces line 12