The coprimality partition of Fouvry

The binary separation argument underlying F84, Lemma 6 (pp. 226–227), and F87, Lemma 7 (p. 624). The exponent is the square of the bound on the number of distinct prime factors, as in F84's proof and F87's statement.

@[reducible, inline]

abbrev LiLiuPrereqFouvry.CoprimePartition.BitColor (T : ℕ) : Type

A separating bit and its value on the first coordinate.

Equations

• LiLiuPrereqFouvry.CoprimePartition.BitColor T = (Fin (T.log2 + 1) × Bool)

theorem LiLiuPrereqFouvry.CoprimePartition.exists_separating_bit {T a b : ℕ} (ha : a ≤ T) (hb : b ≤ T) (hab : a ≠ b) : ∃ (i : Fin (T.log2 + 1)), a.testBit ↑i ≠ b.testBit ↑i

noncomputable def LiLiuPrereqFouvry.CoprimePartition.bitColor (T a b : ℕ) : BitColor T

Choose a differing bit when there is one; the fallback is only used off domain.

Equations

• LiLiuPrereqFouvry.CoprimePartition.bitColor T a b = if h : ∃ (i : Fin (T.log2 + 1)), a.testBit ↑i ≠ b.testBit ↑i then (Classical.choose h, a.testBit ↑(Classical.choose h)) else (⟨0, ⋯⟩, false)

theorem LiLiuPrereqFouvry.CoprimePartition.bitColor_spec {T a b : ℕ} (ha : a ≤ T) (hb : b ≤ T) (hab : a ≠ b) : a.testBit ↑(bitColor T a b).1 = (bitColor T a b).2 ∧ b.testBit ↑(bitColor T a b).1 ≠ (bitColor T a b).2

theorem LiLiuPrereqFouvry.CoprimePartition.bitColor_cross_ne {T a b c d : ℕ} (ha : a ≤ T) (hb : b ≤ T) (hc : c ≤ T) (hd : d ≤ T) (hab : a ≠ b) (hcd : c ≠ d) (hcolor : bitColor T a b = bitColor T c d) : a ≠ d

Equal binary colors prohibit cross equality, not merely equality within a pair.

theorem LiLiuPrereqFouvry.CoprimePartition.card_bitColor (T : ℕ) : Fintype.card (BitColor T) = 2 * (T.log2 + 1)

noncomputable def LiLiuPrereqFouvry.CoprimePartition.paddedFactor (ω n pad : ℕ) (i : Fin ω) : ℕ

Enumerate the distinct prime factors increasingly and pad to the requested length.

Equations

• LiLiuPrereqFouvry.CoprimePartition.paddedFactor ω n pad i = if h : ↑i < n.primeFactors.card then (n.primeFactors.orderEmbOfFin ⋯) ⟨↑i, h⟩ else pad

theorem LiLiuPrereqFouvry.CoprimePartition.paddedFactor_mem_or_eq (ω n pad : ℕ) (i : Fin ω) : paddedFactor ω n pad i ∈ n.primeFactors ∨ paddedFactor ω n pad i = pad

theorem LiLiuPrereqFouvry.CoprimePartition.exists_paddedFactor {ω n p : ℕ} (hω : n.primeFactors.card ≤ ω) (hp : p ∈ n.primeFactors) (pad : ℕ) : ∃ (i : Fin ω), paddedFactor ω n pad i = p

theorem LiLiuPrereqFouvry.CoprimePartition.paddedFactor_le {T ω n pad : ℕ} (hn : n ≤ T) (hpad : pad ≤ T) (i : Fin ω) : paddedFactor ω n pad i ≤ T

theorem LiLiuPrereqFouvry.CoprimePartition.paddedFactor_ne {ω a b : ℕ} (hab : a.Coprime b) (i j : Fin ω) : paddedFactor ω a 0 i ≠ paddedFactor ω b 1 j

Asymmetric padding by 0 and 1 never creates a common prime factor.

@[reducible, inline]

abbrev LiLiuPrereqFouvry.CoprimePartition.MatrixColor (T ω : ℕ) : Type

One binary color for every pair of prime-factor slots.

Equations

• LiLiuPrereqFouvry.CoprimePartition.MatrixColor T ω = (Fin ω → Fin ω → LiLiuPrereqFouvry.CoprimePartition.BitColor T)

noncomputable def LiLiuPrereqFouvry.CoprimePartition.matrixColor (T ω : ℕ) (a : ℕ × ℕ) : MatrixColor T ω

Equations

• LiLiuPrereqFouvry.CoprimePartition.matrixColor T ω a i j = LiLiuPrereqFouvry.CoprimePartition.bitColor T (LiLiuPrereqFouvry.CoprimePartition.paddedFactor ω a.1 0 i) (LiLiuPrereqFouvry.CoprimePartition.paddedFactor ω a.2 1 j)

theorem LiLiuPrereqFouvry.CoprimePartition.card_matrixColor (T ω : ℕ) : Fintype.card (MatrixColor T ω) = (2 * (T.log2 + 1)) ^ ω ^ 2

theorem LiLiuPrereqFouvry.CoprimePartition.matrixColor_cross_coprime {T ω a b c d : ℕ} (hT : 1 ≤ T) (ha₀ : a ≠ 0) (hd₀ : d ≠ 0) (ha : a ≤ T) (hb : b ≤ T) (hc : c ≤ T) (hd : d ≤ T) (haω : a.primeFactors.card ≤ ω) (hdω : d.primeFactors.card ≤ ω) (hab : a.Coprime b) (hcd : c.Coprime d) (hcolor : matrixColor T ω (a, b) = matrixColor T ω (c, d)) : a.Coprime d

Equality of the full matrix forces coprimality across two different pairs.

def LiLiuPrereqFouvry.CoprimePartition.admissiblePairs (T ω : ℕ) : Finset (ℕ × ℕ)

The finite set in F87, Lemma 7; the prime factors are counted without multiplicity.

Equations

• LiLiuPrereqFouvry.CoprimePartition.admissiblePairs T ω = {a ∈ Finset.Icc 1 T ×ˢ Finset.Icc 1 T | a.1.Coprime a.2 ∧ a.1.primeFactors.card ≤ ω ∧ a.2.primeFactors.card ≤ ω}

theorem LiLiuPrereqFouvry.CoprimePartition.mem_admissiblePairs {T ω : ℕ} {a : ℕ × ℕ} : a ∈ admissiblePairs T ω ↔ (1 ≤ a.1 ∧ a.1 ≤ T) ∧ (1 ≤ a.2 ∧ a.2 ≤ T) ∧ a.1.Coprime a.2 ∧ a.1.primeFactors.card ≤ ω ∧ a.2.primeFactors.card ≤ ω

noncomputable def LiLiuPrereqFouvry.CoprimePartition.cell (T ω : ℕ) (κ : MatrixColor T ω) : Finset (ℕ × ℕ)

The fiber of a prime-pair color matrix.

Equations

• LiLiuPrereqFouvry.CoprimePartition.cell T ω κ = {a ∈ LiLiuPrereqFouvry.CoprimePartition.admissiblePairs T ω | LiLiuPrereqFouvry.CoprimePartition.matrixColor T ω a = κ}

theorem LiLiuPrereqFouvry.CoprimePartition.mem_cell {T ω : ℕ} {κ : MatrixColor T ω} {a : ℕ × ℕ} : a ∈ cell T ω κ ↔ a ∈ admissiblePairs T ω ∧ matrixColor T ω a = κ

theorem LiLiuPrereqFouvry.CoprimePartition.cell_cross_coprime {T ω : ℕ} {κ : MatrixColor T ω} {a b : ℕ × ℕ} (ha : a ∈ cell T ω κ) (hb : b ∈ cell T ω κ) : a.1.Coprime b.2

theorem LiLiuPrereqFouvry.CoprimePartition.disjoint_cells {T ω : ℕ} {κ η : MatrixColor T ω} (h : κ ≠ η) : Disjoint (cell T ω κ) (cell T ω η)

noncomputable def LiLiuPrereqFouvry.CoprimePartition.partition (T ω : ℕ) : Finset (Finset (ℕ × ℕ))

Only nonempty fibers are retained, so this is a genuine partition into finite sets.

Equations

• LiLiuPrereqFouvry.CoprimePartition.partition T ω = Finset.image (LiLiuPrereqFouvry.CoprimePartition.cell T ω) (Finset.image (LiLiuPrereqFouvry.CoprimePartition.matrixColor T ω) (LiLiuPrereqFouvry.CoprimePartition.admissiblePairs T ω))

theorem LiLiuPrereqFouvry.CoprimePartition.mem_partition {T ω : ℕ} {s : Finset (ℕ × ℕ)} : s ∈ partition T ω ↔ ∃ a ∈ admissiblePairs T ω, cell T ω (matrixColor T ω a) = s

theorem LiLiuPrereqFouvry.CoprimePartition.partition_nonempty {T ω : ℕ} {s : Finset (ℕ × ℕ)} (hs : s ∈ partition T ω) : s.Nonempty

theorem LiLiuPrereqFouvry.CoprimePartition.partition_pairwise_disjoint (T ω : ℕ) : (↑(partition T ω)).PairwiseDisjoint id

theorem LiLiuPrereqFouvry.CoprimePartition.partition_cover (T ω : ℕ) : (partition T ω).biUnion id = admissiblePairs T ω

theorem LiLiuPrereqFouvry.CoprimePartition.partition_cross_coprime {T ω : ℕ} {s : Finset (ℕ × ℕ)} (hs : s ∈ partition T ω) {a b : ℕ × ℕ} (ha : a ∈ s) (hb : b ∈ s) : a.1.Coprime b.2

theorem LiLiuPrereqFouvry.CoprimePartition.card_partition_le (T ω : ℕ) : (partition T ω).card ≤ (2 * (T.log2 + 1)) ^ ω ^ 2

The exact finite bound, including ω = 0 and T = 0,1.

theorem LiLiuPrereqFouvry.CoprimePartition.sum_partition {M : Type u_1} [AddCommMonoid M] (T ω : ℕ) (f : ℕ × ℕ → M) : ∑ s ∈ partition T ω, ∑ a ∈ s, f a = ∑ a ∈ admissiblePairs T ω, f a

Arbitrary signed or complex weights decompose without a triangle inequality.