OAI/Analysis/CircleDomains/Selection/PrincipalScalarZeroSet.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The zero gradient on a compact source set is preserved by the actual principal-map limit. This follows from compact containment and localized smooth energy bounds, without invoking a quasiconformal chain rule.

  1. lemma OAI.CircleDomainRigidity.PrincipalMapLimit.inverse_mapsTo_neighborhood line 17
  2. lemma OAI.CircleDomainRigidity.PrincipalMapLimit.scalar_energy_zero_set line 34
  3. lemma OAI.CircleDomainRigidity.PrincipalMapLimit.scalar_transport_zero_set line 81