OAI/Analysis/CircleDomains/Probability/CodeLawPhysicalOccupation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Forgetting tags preserves the actual mean physical occupation.

  1. theorem OAI.CircleDomainRigidity.meanPhysicalOccupation_codePathLaw line 20
  2. theorem OAI.CircleDomainRigidity.codePathLaw_collar_endpoints line 35