OAI/Analysis/CircleDomains/Modulus/CompatibleLevelBarrier.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The real barrier in the endpoint problem, with its actual physical representative, countable enlarged flags, and finite-torus compatibility.

  1. structure OAI.CircleDomainRigidity.CompatibleLevelBarrier line 20
  2. def OAI.CircleDomainRigidity.CompatibleLevelBarrier.controlledSize line 53
  3. theorem OAI.CircleDomainRigidity.CompatibleLevelBarrier.finite_compatibility line 60
  4. theorem OAI.CircleDomainRigidity.CompatibleLevelBarrier.controlledSize_le_of_partial_bounds line 71