OAI/Analysis/CircleDomains/Selection/PriorRawCompatibility.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Raw barrier compatibility for smooth finite-energy representatives of the earlier coordinates. The tagged-path inequality and band budget give compatibility using planar coarea, analytic measurability on finite tori, and arcs in connected open subsets.

  1. theorem OAI.CircleDomainRigidity.raw_barrier_compatibility_with_prior_levels line 22