OAI/Analysis/CircleDomains/Probability/PhysicalOccupationCode.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Borel physical occupation on ordinary path space, with zero extension off the finite-length paths. This lets measurable arc selection act directly on path laws without introducing a new code law.

  1. def OAI.CircleDomainRigidity.physicalOccupationCode line 20
  2. lemma OAI.CircleDomainRigidity.physicalOccupationCode_eq line 23
  3. lemma OAI.CircleDomainRigidity.measurable_physicalOccupationCode line 30
  4. def OAI.CircleDomainRigidity.meanPhysicalOccupation line 44
  5. lemma OAI.CircleDomainRigidity.meanPhysicalOccupation_apply line 48
  6. lemma OAI.CircleDomainRigidity.physicalOccupationCode_simple_subarc_le line 56
  7. lemma OAI.CircleDomainRigidity.meanPhysicalOccupation_map_le line 65
  8. lemma OAI.CircleDomainRigidity.meanPhysicalOccupation_mono line 82