OAI/Analysis/CircleDomains/Modulus/PathVariation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Borel length data for ordinary continuous metric paths. These are applied to physical-domain subarcs when forming the path occupation kernel.

  1. theorem OAI.CircleDomainRigidity.pathVariation_lowerSemicontinuous line 18
  2. theorem OAI.CircleDomainRigidity.measurable_pathVariation line 30
  3. theorem OAI.CircleDomainRigidity.measurableSet_rectifiablePaths line 34
  4. theorem OAI.CircleDomainRigidity.measurable_pathVariationFromTo line 39