Choosing coprime moduli at the desired scale

As in Lecomte and Ramakrishnan, Section 4, use the smallest power of each of the first r primes that exceeds the integer scale k. These powers lie between k and a constant (depending only on r) times k.

Main results

• Cslib.Circuits.Boolean.ShallowSymmetric.exists_moduli: r pairwise coprime moduli between k and C k.

References

• V. Lecomte, P. Ramakrishnan, Optimal Shallow Circuits for Majority

theorem Cslib.Circuits.Boolean.ShallowSymmetric.exists_moduli (r : ℕ) : ∃ (C : ℕ), 1 ≤ C ∧ ∀ (k : ℕ), 1 ≤ k → ∃ (m : Fin r → ℕ), (Pairwise fun (i j : Fin r) => (m i).Coprime (m j)) ∧ (∀ (i : Fin r), k < m i) ∧ ∀ (i : Fin r), m i ≤ C * k

Any fixed number of pairwise coprime moduli can be chosen at a common scale, with constants independent of that scale.

theorem Cslib.Circuits.Boolean.ShallowSymmetric.pow_lt_prod_moduli {r k : ℕ} (hr : 0 < r) (m : Fin r → ℕ) (hm : ∀ (i : Fin r), k < m i) : k ^ r < ∏ i : Fin r, m i

The product of r moduli exceeding k exceeds k^r.