OAI/NumberTheory/Ostmann/Arithmetic/GuardedRegularCRT.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.regular_unit_tests_iff line 10
2. theorem OAI.Ostmann.guardedRegularMultiplier_eq_coprime line 17
3. theorem OAI.Ostmann.multiply_regular_after_support line 25
4. theorem OAI.Ostmann.guardedRegularMultiplier_crt line 45
5. theorem OAI.Ostmann.guardedRegularMultiplier_average line 72

   Source documentation

   This is the actual natural-coordinate multiplier, not an auxiliary copy of its transform. The remainder stays complex and may contain the Page factor.

   theorem guardedRegularMultiplier_average {I : Type*} [Fintype I] [DecidableEq I]
       (p : I → ℕ) [∀ i, Fact (p i).Prime] [∀ i, NeZero (p i)] [NeZero (∏ i, p i)]
       (hc : Pairwise (fun i j => (p i).Coprime (p j)))
       (r : ℕ) [NeZero r] [NeZero ((∏ i, p i) * r)] (hcop : (∏ i, p i).Coprime r)
       (active : I → Bool) (s : ℤ) (other : ∀ i, ZMod (p i))
       (hs : ∀ i, (s : ZMod (p i)) ≠ 0) (ho : ∀ i, other i ≠ 0)
       (g : ∀ i, ZMod (p i) → ℂ) (hg : ∀ i, g i 0 = 0)
       (henergy : ∀ i, (∑ x : ZMod (p i), ‖g i x‖ ^ 2) = p i)
       (F : ZMod r × (ZMod r)ˣ → ℂ) :
       (Fintype.card (ZMod ((∏ i, p i) * r) × (ZMod ((∏ i, p i) * r))ˣ) : ℂ)⁻¹ *
         (∑ z, (guardedRegularMultiplier p active s other g z.1.val
           (z.2 : ZMod ((∏ i, p i) * r)).val : ℂ) *
   …

   Mentions: OAI.Ostmann.guardedRegularMultiplier