OAI/Analysis/CircleDomains/Modulus/PartialSimpleArcLength.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite physical length of a simple quotient arc follows from the Hausdorff length of its physical part. No boundary extension of its physical lift is required.

  1. theorem OAI.CircleDomainRigidity.partial_simple_arc_dyadic_sum_le line 16
  2. theorem OAI.CircleDomainRigidity.physicalValue_path_continuousOn line 48
  3. theorem OAI.CircleDomainRigidity.physicalValue_path_injOn line 61
  4. theorem OAI.CircleDomainRigidity.physicalSubpath_variation_eq_value line 73
  5. theorem OAI.CircleDomainRigidity.simple_quotient_arc_physical_length_le line 90
  6. theorem OAI.CircleDomainRigidity.simple_quotient_arc_physical_length_le_preimage line 115