OAI/MeasureTheory/Falconer/Fourier/JetStateFarExpansion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Full-sphere expansion for the actual far-state amplitudes

All angular factors are the original normalized descriptor jets. The constants precede the scale and list, while each pair keeps both endpoints.

  1. theorem OAI.Falconer.exists_descriptorJetSymbol_pair_budget line 16
  2. theorem OAI.Falconer.exists_jetState_far_sphere_expansion line 51