OAI/Analysis/CircleDomains/Modulus/PhysicalPieceLength.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local physical arclength of a glued path is charged to the original piece, without assuming in advance that the glued path is rectifiable.

  1. theorem OAI.CircleDomainRigidity.physicalSubpath_piece_length line 18