OAI/Analysis/CircleDomains/Selection/CountableHitTests.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The visit estimate from modulus extraction supplies the finite point-hit tests used by fusion, with the same numerical constant.

  1. theorem OAI.CircleDomainRigidity.finite_hit_square_sum_le_of_counting_norm line 20
  2. theorem OAI.CircleDomainRigidity.passesHitTests_of_counting_norm line 68