PrimeProductTranslations.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

CRT translation tables indexed by the prime product alone

theorem OAI.Ostmann.exists_primeSet_translation line 11

theorem OAI.Ostmann.exists_primeProduct_translations line 40

Source documentation

The chosen translation depends on the squarefree product, so all permutations of a tuple use the same Fourier phase and coefficient array.

theorem exists_primeProduct_translations (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (k L : ℕ) [NeZero L] (t : ℕ → ℤ)
    (hcop : ∀ M ∈ primeSubsetProducts P k, L.Coprime M) :
    ∃ τ h₀ : ℕ → ℕ, ∀ M ∈ primeSubsetProducts P k,
      τ M < M ∧ h₀ M < L ∧ (L : ℤ) ∣ (τ M : ℤ) + (M : ℤ) * h₀ M ∧
      ∀ p ∈ M.primeFactors, (τ M : ZMod p) = (t p : ZMod p) := by
…

Mentions: OAI.Ostmann.primeSubsetProducts

theorem OAI.Ostmann.primeTupleProduct_mem line 65
theorem OAI.Ostmann.primeTuple_member_primeFactors line 76