OAI/Analysis/CircleDomains/Topology/PriorityCutoffSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous source selection: shrinking supports have small total weighted mass, while their smooth cutoff gradients have a prescribed summable budget. Overlap of the supports is allowed.

  1. theorem OAI.CircleDomainRigidity.exists_priority_cutoffs line 14