OAI/NumberTheory/Ostmann/Arithmetic/MovingOriginalWeightRelabel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The original giant weight commutes with evaluating pattern labels

  1. theorem OAI.Ostmann.movingSlotModulus_map line 12
  2. theorem OAI.Ostmann.movingSlotCutoff_map line 19
  3. theorem OAI.Ostmann.movingPhiExtra_map line 28
  4. theorem OAI.Ostmann.movingOriginalGiantWeight_map line 38
  5. theorem OAI.Ostmann.MovingSlotData.regularSlots_map line 66
  6. theorem OAI.Ostmann.MovingSlotData.frequencyProduct_map line 70
  7. theorem OAI.Ostmann.MovingSlotData.currentSlots_map line 77
  8. theorem OAI.Ostmann.movingLocalGiantUnits_map line 82
  9. theorem OAI.Ostmann.MovingSlotReversal.naturalPivot_map line 89
  10. theorem OAI.Ostmann.movingLocalSupport_map line 95
  11. theorem OAI.Ostmann.movingFullSupport_map line 104
  12. theorem OAI.Ostmann.movingSupportedWeight_map line 121