OAI/NumberTheory/Ostmann/ZeroDensity/MovingZeroFrequency.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Zero frequencies vanish in the original sampled histories

  1. theorem OAI.Ostmann.recursiveTransferWeight_nonzero_frequencies line 11
  2. theorem OAI.Ostmann.movingSupportedSampledWeight_zero_frequency line 41
  3. theorem OAI.Ostmann.movingOriginalSampleAverage_zero_frequency line 65