OAI/Analysis/CircleDomains/Modulus/CriticalFiberLength.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Critical points of a C1 scalar planar map contribute zero fiber length for almost every level. No assertion that C1 critical values have measure zero is used.

  1. lemma OAI.CircleDomainRigidity.critical_fiber_majorant line 15
  2. lemma OAI.CircleDomainRigidity.ae_zero_critical_fiber_length line 69