OAI/MeasureTheory/Falconer/Fourier/JetStateNearFar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The near/far decomposition for actual recursive angular states

All descriptor factors remain in the far integrals. The intermediate child model masses cancel exactly when these integrals are opened.

  1. theorem OAI.Falconer.jetState_energy_near_far line 19