OAI/Analysis/CircleDomains/Selection/SquareVisitTolls.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Square bounds on weights and mean visits give finite actual weighted tolls almost surely. This retains all visits, including both endpoints.

  1. theorem OAI.CircleDomainRigidity.tsum_mul_le_countingSquareNorm line 14
  2. theorem OAI.CircleDomainRigidity.lintegral_boundaryToll_le_square_norms line 27
  3. theorem OAI.CircleDomainRigidity.ae_boundaryToll_finite line 36