OAI/MeasureTheory/Falconer/Angular/QuantitativeCaps.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative smooth cap partition on the sphere

This supplies the actual partition used in angular localization, with uniform derivatives, a polynomial global count, and bounded local overlap. It contains no Fourier or incidence estimate as an assumption.

  1. theorem OAI.Falconer.normalizedCap_complex_chart_derivatives line 17
  2. theorem OAI.Falconer.quantitative_smooth_cap_partition line 40