OAI/Analysis/CircleDomains/Modulus/CompatibleRealBarrier.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.CompatibleRealBarrier line 20
  2. def OAI.CircleDomainRigidity.CompatibleRealBarrier.controlledSize line 53
  3. theorem OAI.CircleDomainRigidity.CompatibleRealBarrier.finite_compatibility line 60
  4. theorem OAI.CircleDomainRigidity.CompatibleRealBarrier.controlledSize_le_of_partial_bounds line 71