OAI/MeasureTheory/Falconer/Fourier/JetStateBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform graph budget for factorized angular symbols

The constants are fixed before the descriptor list and scale. Every symbol in the recursive class then has the same size-one graph control, provided its explicit mask derivative scale fits inside the displayed graph scale.

  1. theorem OAI.Falconer.exists_descriptorJetSymbol_admissible line 16