OAI/Analysis/CircleDomains/Modulus/PerturbedBarrierData.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An admissible extended coding metric supplies the actual positive physical density, countable quotient tolls, and endpoint cost used by the barrier theorem. No restriction on values on area-null sets is imposed.

  1. theorem OAI.CircleDomainRigidity.exists_perturbed_barrier_data line 19