OAI/MeasureTheory/Falconer/Estimates/EligibilityExcision.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Removing all ineligible cell terms from the exact expansion

The exceptional angular sets are chosen before the radial frequency. Consequently the finite whole-cell decision is valid in the full product integral and never truncates an angular support by a nonsmooth test.

  1. theorem OAI.Falconer.capIncidence_nonneg line 18
  2. theorem OAI.Falconer.DyadicCube.cap_sum_eq_eligible line 23
  3. theorem OAI.Falconer.pair_transform_sum line 57
  4. theorem OAI.Falconer.weighted_dyadic_expansion_excision line 66