OAI/NumberTheory/Ostmann/Construction/DiagonalRegularLift.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.diagonalRegularMultiplier_full_modulus line 13

   Source documentation

   Extra powers introduced when clearing the moving denominators have no cost when the signed integrand factors through the displayed CRT coordinates.

   theorem diagonalRegularMultiplier_full_modulus {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)
       (M : ℕ) [NeZero M] (hd : (∏ i, p i) * r ∣ M)
       (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 M × (ZMod M)ˣ) : ℂ)⁻¹ *
         (∑ z, (diagonalRegularMultiplier p active s other g
   …

   Mentions: OAI.Ostmann.diagonalRegularMultiplier