OAI/Analysis/CircleDomains/Modulus/PathLengthKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The arclength measures form a Borel kernel on rectifiable paths.

  1. theorem OAI.CircleDomainRigidity.measurable_pathLengthMeasure line 18
  2. def OAI.CircleDomainRigidity.pathLengthKernel line 31
  3. theorem OAI.CircleDomainRigidity.pathLengthKernel_apply line 35
  4. instance OAI.CircleDomainRigidity.(instance at line 38) line 38