OAI/NumberTheory/Ostmann/Arithmetic/MovingSeparatedCoefficient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingSeparatedSupport line 11
2. def OAI.Ostmann.movingSeparatedResidueCoefficient line 18
3. theorem OAI.Ostmann.movingSpectatorResidue_eq_modularProduct line 28
4. theorem OAI.Ostmann.movingReducedResidueCoefficient_eq_separated line 42

   Source documentation

   Exact identity for the literal original reduced residue coefficient. Its frequency factor has a frequency-only period; the other factors use only internal-prime squares and individual spectator primes.

   theorem movingReducedResidueCoefficient_eq_separated {σ I : Type*} (q : I → ℕ)
       [∀ i, Fact (q i).Prime] (tier : σ → ℕ) (value : σ → ℕ)
       (hprime : ∀ i, (value i).Prime)
       (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
       (outside : List ℕ)
       (childBound pivotBound : ℕ → ℕ)
       (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (E : {n : ℕ} → MovingSlotData σ n → ℤ → ℤ → ℤ → ℝ)
       (g : ∀ i, ZMod (q i) → ℂ) (D : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (hcover : ∀ p ∈ outside, ∃ i ∈ S, q i = p)
       (hg0 : ∀ i ∈ S, g i 0 = 0)
       {n : ℕ} (T : MovingSlotData σ n) (hlevels : T.Levels tier)
   …

   Mentions: OAI.Ostmann.MovingSlotData