OAI/MeasureTheory/Falconer/Estimates/LocalizationSum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Summing integrated nonstationary errors

An edge is removed only after its whole oscillatory integral has been estimated. The cardinality loss is explicit and can be absorbed by the arbitrary power gain. No pointwise angular truncation is introduced.

  1. theorem OAI.Falconer.integrated_discarded_sum_bound line 17