OAI/Analysis/CircleDomains/Modulus/WeightedHausdorffImage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Weighted Hausdorff-measure estimates for the finite sphere chart. The estimates are proved from the library's Lipschitz Hausdorff bound.

  1. theorem OAI.CircleDomainRigidity.lipschitzOn_hausdorff_restrict_le_map line 16
  2. theorem OAI.CircleDomainRigidity.lipschitzOn_lintegral_hausdorff_image_le line 38
  3. theorem OAI.CircleDomainRigidity.lintegral_hausdorff_image_le_of_partition line 50