OAI/Analysis/CircleDomains/Rigidity/ENNRealBoundaryTrace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Pointwise trace convergence and the countable exceptional set for the ENNReal dust budgets used by the constructed chain potential.

  1. theorem OAI.CircleDomainRigidity.countable_square_toll_support line 14
  2. theorem OAI.CircleDomainRigidity.boundaryTrace_of_ennreal_budget line 19