OAI/Analysis/CircleDomains/Modulus/RawBarrierCompatibility.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compatibility for the actual raw path-cost barrier. Finite level payments and square-summable point incidences give the null component traces; the only descriptive-set input is the cited finite-torus form of Kechris's analytic-measurability theorem.

  1. theorem OAI.CircleDomainRigidity.freeComponentFailure_empty_labels line 18
  2. theorem OAI.CircleDomainRigidity.raw_barrier_compatibility_of_finite_level_payments line 31