OAI/MeasureTheory/Falconer/Fourier/JetStateSpatialShell.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Spatial Fourier terms controlled by the exact recursive state

Spatial phases and conjugation preserve the actual descriptor symbol class. Consequently each separated inverse factor is controlled by its own next-state supremum, without enlarging the class of angular symbols.

  1. def OAI.Falconer.DescriptorJetSymbol.spatialFourier line 23
  2. theorem OAI.Falconer.DescriptorJetSymbol.spatialFourier_value line 28
  3. theorem OAI.Falconer.spatial_endpoint_energy_le_jetStateEnvelope line 39
  4. theorem OAI.Falconer.jet_state_spatial_shell_le line 67