OAI/NumberTheory/Ostmann/Arithmetic/MovingOriginalBulkAction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The original coefficient and common transform under bulk reassignment

  1. theorem OAI.Ostmann.MovingSlotReversal.naturalProduct_selected_bulk line 12
  2. theorem OAI.Ostmann.movingExternalDiagonalWeight_selectedBulkSample line 32
  3. theorem OAI.Ostmann.movingExternalDiagonalWeight_positive line 46
  4. theorem OAI.Ostmann.movingFrequencyCoefficient_bulk_action line 72
  5. theorem OAI.Ostmann.movingOriginalMatchedCorrelation_bulk_action line 88