OAI/Analysis/CircleDomains/Modulus/PathHausdorffLength.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every continuous path has image Hausdorff length at most its metric variation. Small dyadic images supply the covers in the definition.

  1. theorem OAI.CircleDomainRigidity.exists_small_dyadic_images line 16
  2. theorem OAI.CircleDomainRigidity.path_hausdorff_length_le_variation line 33