OAI/Analysis/CircleDomains/Modulus/AffinePhysicalArclength.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact arclength of a physical compact subpath after affine restriction. Constant extension outside the subpath adds no endpoint mass.

  1. theorem OAI.CircleDomainRigidity.physicalSubpath_affine_lengthCode line 18