OAI/Analysis/CircleDomains/Probability/PointHitPairOccupation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A common interior visit forces a unit lower bound for every sufficiently small proximity integral. The bound concerns the original physical occupations.

  1. theorem OAI.CircleDomainRigidity.one_le_ball_pair_integral line 16
  2. theorem OAI.CircleDomainRigidity.code_hit_ball_occupation_ge line 50