OAI/Analysis/CircleDomains/Selection/FiniteSupBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A simultaneous finite weighted bound survives taking the independent supremum in each coordinate. This will bound every tail of the fusion tree.

  1. theorem OAI.CircleDomainRigidity.finite_weighted_sup_le line 16