OAI/Analysis/CircleDomains/Modulus/FiniteWeightedCutoffs.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Smooth compact cutoffs have finite differential energy, so weighted coarea and Sard choose finite-cost regular contours without an added energy hypothesis on the cutoff.

  1. theorem OAI.CircleDomainRigidity.smooth_compact_differential_energy line 17
  2. theorem OAI.CircleDomainRigidity.exists_finite_weighted_regular_superlevel line 37