OAI/Analysis/CircleDomains/Probability/PointHitOccupation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A visit to a fixed interior point forces physical occupation of each surrounding region before the path can end outside it.

  1. theorem OAI.CircleDomainRigidity.point_hit_occupation_lower_bound line 20
  2. theorem OAI.CircleDomainRigidity.mean_occupation_ge_point_hit line 67