OAI/NumberTheory/Ostmann/Arithmetic/MovingSlotRelabel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Relabelling repeated sampled slots by their equality-pattern classes

  1. def OAI.Ostmann.MovingSlotReversal.map line 11
  2. def OAI.Ostmann.MovingSlotData.map line 21
  3. theorem OAI.Ostmann.MovingSlotData.frequency_map line 27
  4. theorem OAI.Ostmann.MovingSlotData.frequencies_map line 31
  5. theorem OAI.Ostmann.MovingSlotData.size_map line 39
  6. theorem OAI.Ostmann.MovingSlotData.levels_map line 46
  7. theorem OAI.Ostmann.MovingSlotReversal.naturalProduct_map line 54
  8. theorem OAI.Ostmann.MovingSlotReversal.modularPivot_map line 59
  9. theorem OAI.Ostmann.MovingSlotData.step_map line 64
  10. theorem OAI.Ostmann.movingModularSpectator_map line 72

    Source documentation

    Evaluation after identifying two labels is precisely evaluation at the corresponding repeated prime value; no independence is asserted here.

    theorem movingModularSpectator_map {σ τ : Type*} (f : σ → τ)
    (value : τ → ℕ) (q : ℕ) [Fact q.Prime] (g : ZMod q → ℂ) (D : (ZMod q)ˣ)
    {n : ℕ} (T : MovingSlotData σ n) (x y : ZMod q) :
    movingModularSpectator value q g D (T.map f) x y =
      movingModularSpectator (value ∘ f) q g D T x y := by
…

    Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingModularSpectator