OAI/Analysis/CircleDomains/Selection/GatedMeanCoordinateExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The law alternative produces one actual coordinate with both a small source budget and an open exclusion of the prescribed map--disk pair. The gate and the smoothing tolerance refer to the same compact arc law.

  1. theorem OAI.CircleDomainRigidity.exists_gated_small_mean_exclusion line 20