OAI/Analysis/CircleDomains/Probability/PathLengthMeasure.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The arclength measure of an ordinary rectifiable continuous metric path. It is atomless and assigns each interval its actual metric variation.

  1. abbrev OAI.CircleDomainRigidity.RectifiablePath line 18
  2. def OAI.CircleDomainRigidity.pathLengthFunction line 21
  3. def OAI.CircleDomainRigidity.pathLengthMeasure line 28
  4. theorem OAI.CircleDomainRigidity.continuous_pathLengthFunction line 31
  5. instance OAI.CircleDomainRigidity.(instance at line 37) line 37
  6. instance OAI.CircleDomainRigidity.(instance at line 41) line 41
  7. theorem OAI.CircleDomainRigidity.pathLengthMeasure_Ioc line 49
  8. theorem OAI.CircleDomainRigidity.pathLengthMeasure_Icc line 59
  9. theorem OAI.CircleDomainRigidity.pathLengthMeasure_univ line 64