OAI/MeasureTheory/Falconer/Fourier/OriginalStationaryReplacement.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Radial replacement of the original two-sphere kernel

Both endpoint amplitudes are the original recursive symbols. The estimate is pointwise in all four endpoints, so its norm can subsequently be integrated without any spatial measurability assertion for stationary jets.

  1. theorem OAI.Falconer.state_pair_sphere_measurable line 18
  2. theorem OAI.Falconer.state_pair_sphere_bound line 31
  3. theorem OAI.Falconer.exists_jetState_original_stationary_replacement line 48