OAI/Analysis/CircleDomains/Uniformization/UniformGraphHausdorff.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform small graph covers give an actual Hausdorff-measure bound. Only a fixed interior margin of the chosen energy neighborhood is used.

  1. lemma OAI.CircleDomainRigidity.uniform_graph_hausdorff_le line 12