OAI/Analysis/CircleDomains/Modulus/CountableConcatenationLength.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact arclength addition over the decreasing collar intervals. This is an extended-real identity and therefore does not assume rectifiability.

  1. theorem OAI.CircleDomainRigidity.collar_variation_partial line 18
  2. theorem OAI.CircleDomainRigidity.collar_variation_sum line 30
  3. theorem OAI.CircleDomainRigidity.collarConcatenation_variation line 52
  4. theorem OAI.CircleDomainRigidity.collarConcatenation_rectifiable line 69