OAI/Analysis/CircleDomains/Modulus/UnitGraphCapacity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The unit Sobolev capacity estimate supplies a countable graph cover with a quantitative quadratic cost and uniformly bounded diameters.

  1. lemma OAI.CircleDomainRigidity.unit_graph_capacity_cover line 13