OAI/Analysis/CircleDomains/Sobolev/DifferentiableCriticalFibers.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Critical differentiability points contribute zero length on almost every scalar fiber. No continuity of the differential is used.

  1. lemma OAI.CircleDomainRigidity.differentiable_critical_fiber_majorant line 14
  2. lemma OAI.CircleDomainRigidity.ae_zero_differentiable_critical_fiber_length line 52