OAI/Analysis/CircleDomains/Sobolev/LipschitzPieceGradient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A Lipschitz extension agreeing on a measurable piece has the original Sobolev weak gradient there, almost everywhere.

  1. lemma OAI.CircleDomainRigidity.lipschitz_piece_partial_eq line 16
  2. lemma OAI.CircleDomainRigidity.lipschitz_piece_gradient_eq line 50