OAI/Analysis/CircleDomains/Probability/RectifiableOccupationCode.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A Borel occupation code on the Borel subset of rectifiable paths. The total extension is zero off that subset; length finiteness is always checked separately before it is used as physical occupation.

  1. def OAI.CircleDomainRigidity.rectifiableOccupationCode line 20
  2. theorem OAI.CircleDomainRigidity.rectifiableOccupationCode_eq line 24
  3. theorem OAI.CircleDomainRigidity.measurable_rectifiableOccupationCode line 29
  4. theorem OAI.CircleDomainRigidity.rectifiableOccupationCode_univ line 34
  5. instance OAI.CircleDomainRigidity.(instance at line 39) line 39
  6. instance OAI.CircleDomainRigidity.(instance at line 46) line 46