OAI/MeasureTheory/Falconer/Fourier/DescriptorJetMeasurable.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Measurability of the actual anchored mask jets

The spatial variable only selects one of finitely many Borel anchor cells. Within such a cell all angular jets are derivatives of its fixed smooth mask.

  1. theorem OAI.Falconer.normalizedDescriptorJet_anchor_sum line 17
  2. theorem OAI.Falconer.normalizedDescriptorJet_measurable line 51
  3. theorem OAI.Falconer.descriptorJetProduct_measurable line 74