OAI/Analysis/CircleDomains/Probability/AffinePhysicalOccupation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Weighted physical costs of restricted paths are the old costs on the retained interval, with full multiplicity and no endpoint atoms.

  1. theorem OAI.CircleDomainRigidity.physicalOccupation_affine line 19
  2. theorem OAI.CircleDomainRigidity.physicalCost_affine line 35