OAI/Analysis/CircleDomains/Sobolev/FiniteHitSquareEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite dust hit tests imply the full square sum needed for shrinking collars, with no enlargement of the constant.

  1. theorem OAI.CircleDomainRigidity.pathHit_square_tsum_le line 19
  2. theorem OAI.CircleDomainRigidity.codeHit_square_tsum_le line 35
  3. theorem OAI.CircleDomainRigidity.codeHit_square_tsum_restrict line 43