OAI/MeasureTheory/Falconer/Fourier/JetStateEnvelope.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Supremum of the factorized recursive angular states

The supremum varies the actual finite jets and the bounded smooth/spatial multipliers. The displayed descriptor lists and all normalization data stay fixed. Reached deletion maps each such symbol into the exact shorter list.

  1. def OAI.Falconer.jetStateEnergy line 16
  2. def OAI.Falconer.jetStateValues line 26
  3. def OAI.Falconer.jetStateEnvelope line 33
  4. def OAI.Falconer.jetStateBound line 39
  5. theorem OAI.Falconer.jetStateBound_nonneg line 47
  6. theorem OAI.Falconer.jetStateEnergy_bound line 53
  7. theorem OAI.Falconer.jetStateValues_bddAbove line 75
  8. theorem OAI.Falconer.jetStateEnergy_le_envelope line 90
  9. theorem OAI.Falconer.jetStateEnvelope_remove_reached line 104