OAI/Analysis/CircleDomains/Probability/PhysicalOccupationAdd.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Physical arclength occupation is independent of the chosen compact restriction and adds across a subdivision of the same physical path.

  1. theorem OAI.CircleDomainRigidity.physicalSubpath_occupation_portion line 21
  2. theorem OAI.CircleDomainRigidity.physicalSubpath_occupation_add line 31