OAI/Analysis/CircleDomains/Modulus/PathLengthLocality.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Time arclength is local on closed intervals and adds at shared endpoints.

  1. def OAI.CircleDomainRigidity.rectifiableLengthCode line 17
  2. theorem OAI.CircleDomainRigidity.rectifiableLengthCode_eq line 20
  3. theorem OAI.CircleDomainRigidity.rectifiableLengthCode_univ line 24
  4. instance OAI.CircleDomainRigidity.(instance at line 28) line 28
  5. instance OAI.CircleDomainRigidity.(instance at line 33) line 33
  6. theorem OAI.CircleDomainRigidity.rectifiableLengthCode_const line 39
  7. theorem OAI.CircleDomainRigidity.pathLengthMeasure_restrict_congr line 52
  8. theorem OAI.CircleDomainRigidity.pathLengthMeasure_restrict_add line 68
  9. theorem OAI.CircleDomainRigidity.measurable_rectifiableLengthCode line 90