OAI/NumberTheory/Ostmann/Arithmetic/MovingCompactLeaf.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Compact leaf multipliers preserve the scheduled statistic

  1. def OAI.Ostmann.movingCompactLeaf line 12

    Source documentation

    The zero frequency is removed and all live bottom frequencies are retained.

    noncomputable def movingCompactLeaf (V : ℕ) (s : ℤ) : ℂ :=
…
  2. theorem OAI.Ostmann.movingCompactLeaf_zero line 15
  3. theorem OAI.Ostmann.movingCompactLeaf_norm line 18
  4. theorem OAI.Ostmann.movingOriginalLeaf_congr line 23
  5. theorem OAI.Ostmann.movingFrequencyCoefficient_original_leaf_congr line 32
  6. theorem OAI.Ostmann.movingWeightedMatchedCorrelation_leaf_congr line 49
  7. theorem OAI.Ostmann.movingTemplateCoefficient_original_leaf_congr line 70
  8. theorem OAI.Ostmann.movingWeightedMatchedCorrelation_compact line 85