OAI/Analysis/CircleDomains/Selection/VisitCardinality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The measurable finite-witness count agrees with the actual extended sum of unit tolls over all visit times.

  1. theorem OAI.CircleDomainRigidity.visitCount_eq_tsum line 17