OAI/MeasureTheory/Falconer/Fourier/NormalizedJetDerivatives.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Scale-normalized ambient derivatives of a single mask

  1. def OAI.Falconer.normalizedAmbientDescriptorJet line 11
  2. theorem OAI.Falconer.normalizedAmbientDescriptorJet_sphere line 18
  3. theorem OAI.Falconer.normalizedAmbientDescriptorJet_contDiff line 25
  4. theorem OAI.Falconer.normalizedAmbientDescriptorJet_derivatives line 34