OAI/Analysis/CircleDomains/Selection/UncountableHitTail.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Shrinking hit estimates on the whole dust set. Square summability itself supplies the countable support; the dust is not assumed countable.

  1. theorem OAI.CircleDomainRigidity.tendsto_punctured_hit_energy_of_finite_tsum line 14
  2. theorem OAI.CircleDomainRigidity.tendsto_punctured_hit_norm_of_finite_tsum line 50