OAI/Analysis/CircleDomains/Modulus/BandBudgetNorm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Real square norms of band widths are bounded by their ENNReal budgets, including when the marked set is only a subset of the full budget support.

  1. theorem OAI.CircleDomainRigidity.real_square_norm_le_counting line 15