OAI/Analysis/CircleDomains/Selection/IndexAvoidance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An avoiding test path has constant sample index. Thus the mean index also has equal endpoint values if almost every sample misses the test path.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.diskArcIndex_eq_along_avoiding_path line 14
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.meanDiskArcIndex_eq_along_ae_avoiding_path line 28