OAI/Analysis/CircleDomains/Selection/FiniteFlagIntersections.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The countable flags contribute finitely many distinct intersections for almost every independently chosen level. Repeated visits are paid only through the actual path law's square bound.

  1. theorem OAI.CircleDomainRigidity.measurable_flag_intersection_count line 20
  2. theorem OAI.CircleDomainRigidity.ae_flag_intersection_count_finite_of_sum line 33
  3. theorem OAI.CircleDomainRigidity.ae_flag_intersection_count_finite line 56
  4. theorem OAI.CircleDomainRigidity.tsum_flag_weight_hit_finite line 69
  5. theorem OAI.CircleDomainRigidity.ae_flag_intersection_count_finite_of_support line 97
  6. theorem OAI.CircleDomainRigidity.mean_flag_intersection_count_finite_of_support line 110