OAI/MeasureTheory/Falconer/Estimates/RotatedMaskedRemainder.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The stationary remainder for the actual masked distance Fourier transform

This is the original masked law, with its original model mass and its cell-scale distance weight. The integrability premise is supplied by the finite separated inverse integration theorem.

  1. theorem OAI.Falconer.exists_rotated_masked_fourier_inverse_order line 17