OAI/Analysis/CircleDomains/Selection/SmallMeanCoordinateConstruction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Arbitrarily small compact-law norms produce the actual masked coordinate with a strictly small full Stokes budget.

  1. theorem OAI.CircleDomainRigidity.exists_smooth_mean_coordinate_with_small_budget line 19