OAI/MeasureTheory/Falconer/Fourier/AmbientSymbols.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Ambient smooth symbols in the adapted spherical chart

The smooth cap partition is constructed in Euclidean space. Its restriction to every rotated one-coordinate spherical chart is smooth, including at points where the amplitude vanishes.

  1. theorem OAI.Falconer.normalizedLine_contDiff line 20
  2. theorem OAI.Falconer.ambient_symbol_chart_smooth line 26
  3. theorem OAI.Falconer.finite_smooth_chart_cap_partition line 41