OAI/MeasureTheory/Falconer/Angular/CapEnergyExpansion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Inserting the actual cap partition before localization

The complex cross terms remain inside the angular and radial integrals. The cap insertion is an exact identity; no positivity or pointwise truncation is used to discard an oscillatory term.

  1. theorem OAI.Falconer.cap_pair_partition line 16
  2. theorem OAI.Falconer.cap_partition_cross_sum line 23
  3. theorem OAI.Falconer.integrated_cap_cross_expansion line 32