OAI/MeasureTheory/Falconer/Fourier/RotatedMaskedJetShell.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual masked distance shell in the recursive jet class

The inverse family is constructed from the zero-jet root, with constants chosen before the masks, scale, and endpoint measures. The only analytic inputs are the published gnomonic formula and quadratic stationary phase.

  1. theorem OAI.Falconer.exists_rotated_masked_jet_shell_order line 19