OAI/NumberTheory/Ostmann/Construction/DiagonalRegularMultiplier.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.diagonalRegularMultiplier line 12

   Source documentation

   other i is the fixed denominator consisting of the outside and all small slots other than the regular prime i. The two giants are retained.

   noncomputable def diagonalRegularMultiplier {I : Type*} [Fintype I]
       (p : I → ℕ) [∀ i, Fact (p i).Prime] (active : I → Bool)
       (s : ℤ) (other : ∀ i, ZMod (p i)) (g : ∀ i, ZMod (p i) → ℂ)
       (z : ∀ i, ZMod (p i) × (ZMod (p i))ˣ) : ℝ :=
   …

2. def OAI.Ostmann.diagonalRegularCoefficient line 21
3. theorem OAI.Ostmann.diagonalRegularMultiplier_local line 26
4. theorem OAI.Ostmann.diagonalRegularMultiplier_crt line 53

   Source documentation

   The manuscript's regular multiplier is integrated before taking any absolute value of the signed remainder, which may include Page factors.

   theorem diagonalRegularMultiplier_crt {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, (diagonalRegularMultiplier p active s other g
           (crtExternalPairEquiv p hc (crtSplitExternalEquiv (∏ i, p i) r hcop z).1) : ℂ) *
   …

   Mentions: OAI.Ostmann.diagonalRegularMultiplier, OAI.Ostmann.crtExternalPairEquiv, OAI.Ostmann.crtSplitExternalEquiv