OAI/Analysis/CircleDomains/Selection/FlagIntersectionCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Flagged intersections count each image point once. Tonelli bounds these actual counts by the level-band width times its hit probability, so repeated visits introduce no extra factor in the final bound.

  1. theorem OAI.CircleDomainRigidity.pathImageCount_inter_eq_tsum line 19
  2. theorem OAI.CircleDomainRigidity.mean_flag_intersection_count_le line 34