OAI/NumberTheory/Ostmann/Arithmetic/MovingRegularLiveOffDiagonal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingGiantOffDiagonal_regular_on_live line 17

   Source documentation

   The original coefficient and all its prior factors remain in W. Only the local Fourier arguments are rewritten; no absolute values are taken and no integer-pivot transform is introduced.

   theorem movingGiantOffDiagonal_regular_on_live {A H : Type*} [Fintype A] [Fintype H]
       (L : A → H → ℕ) [∀ a i, Fact (L a i).Prime]
       (g : ∀ a i, ZMod (L a i) → ℂ)
       (hg : ∀ a i x, g a i (-x) = conj (g a i x))
       (I : Finset ℕ) (V U D : ℕ) (v : A → ℤ) (w : ℕ → ℝ) (W : ℕ → A → ℂ)
       (hsupport : ∀ p ∈ I, ∀ a, W p a ≠ 0 →
         Pairwise (fun i j => (L a i).Coprime (L a j)) ∧
         (∏ i, L a i).Coprime (p * U) ∧ ∀ i, D.Coprime (L a i))
       (hlarge : ∀ p ∈ I, ∀ a, W p a ≠ 0 →
         ∀ q, q.Prime → q ∣ ∏ i, L a i → V < q) :
       movingGiantOffDiagonal I V U (fun a => ∏ i, L a i) v w
         (movingRegularCoefficient L g D U v W) =
   …

   Mentions: OAI.Ostmann.movingGiantOffDiagonal, OAI.Ostmann.movingRegularCoefficient