OAI/NumberTheory/Ostmann/Arithmetic/MovingArithmeticBlocks.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.MovingArithmeticBlocks line 11
2. def OAI.Ostmann.movingArithmeticModuli line 16

   Source documentation

   One frequency block, one square for each distinct internal prime, and one field for each spectator.

   def movingArithmeticModuli {I : Type*} (r : ℕ) (q : I → ℕ)
       (P : Finset ℕ) (S : Finset I) : MovingArithmeticBlocks P S → ℕ
     | .inl _ => r
     | .inr (.inl p) => p.val ^ 2
     | .inr (.inr i) => q i.val

   Mentions: OAI.Ostmann.MovingArithmeticBlocks

3. theorem OAI.Ostmann.movingArithmeticModuli_product line 22
4. theorem OAI.Ostmann.movingFrequencyPairFactor_modEq line 31
5. theorem OAI.Ostmann.crtExternalPairEquiv_casts line 51

   Source documentation

   CRT coordinates are the casts of the original two residue representatives.

   theorem crtExternalPairEquiv_casts {B : Type*} [Fintype B] (a : B → ℕ)
       [NeZero (∏ i, a i)] (hc : Pairwise (fun i j => (a i).Coprime (a j)))
       (z : ZMod (∏ i, a i) × (ZMod (∏ i, a i))ˣ) (i : B) :
       ((z.1.val : ZMod (a i)), ((z.2 : ZMod (∏ i, a i)).val : ZMod (a i))) =
         ((crtExternalPairEquiv a hc z i).1, ((crtExternalPairEquiv a hc z i).2 : ZMod (a i))) := by
   …

   Mentions: OAI.Ostmann.crtExternalPairEquiv

6. def OAI.Ostmann.movingArithmeticLocalFactor line 69
7. theorem OAI.Ostmann.movingArithmeticBlocks_average line 85

   Source documentation

   Complex-valued finite CRT factorization for the actual arithmetic blocks.

   theorem movingArithmeticBlocks_average {I : Type*} (r : ℕ) (q : I → ℕ)
       (P : Finset ℕ) (S : Finset I)
       [∀ b, NeZero (movingArithmeticModuli r q P S b)]
       [NeZero (∏ b, movingArithmeticModuli r q P S b)]
       (hc : Pairwise (fun b c => (movingArithmeticModuli r q P S b).Coprime
         (movingArithmeticModuli r q P S c)))
       (f : ∀ b, ZMod (movingArithmeticModuli r q P S b) ×
         (ZMod (movingArithmeticModuli r q P S b))ˣ → ℂ) :
       (Fintype.card (ZMod (∏ b, movingArithmeticModuli r q P S b) ×
         (ZMod (∏ b, movingArithmeticModuli r q P S b))ˣ) : ℂ)⁻¹ *
         (∑ z, ∏ b, f b (crtExternalPairEquiv (movingArithmeticModuli r q P S) hc z b)) =
       ∏ b, (Fintype.card (ZMod (movingArithmeticModuli r q P S b) ×
   …

   Mentions: OAI.Ostmann.movingArithmeticModuli, OAI.Ostmann.crtExternalPairEquiv