OAI/Analysis/CircleDomains/Topology/CompactHeightPullback.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The flattened height, cut off beyond the actual omitted set, is a compact continuous Sobolev test on the source. The constancy on holes is proved from the constructed height.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.height_cutoff_constant_on_components line 17
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.compact_flattened_height_pullback line 43