Logarithmic cardinality bound for the Fouvry partition

The explicit absolute constant 4 / log 2 converts the exact binary count to the bound in F87, Lemma 7. Real cutoffs are handled by the natural floor, with the original integer-pair domain proved exactly.

noncomputable def LiLiuPrereqFouvry.CoprimePartition.partitionConstant : ℝ

Equations

• LiLiuPrereqFouvry.CoprimePartition.partitionConstant = 4 / Real.log 2

theorem LiLiuPrereqFouvry.CoprimePartition.partitionConstant_pos : 0 < partitionConstant

theorem LiLiuPrereqFouvry.CoprimePartition.bitColor_card_le_log {T : ℕ} (hT : 2 ≤ T) : ↑(2 * (T.log2 + 1)) ≤ partitionConstant * Real.log ↑T

theorem LiLiuPrereqFouvry.CoprimePartition.card_partition_le_log {T : ℕ} (hT : 2 ≤ T) (ω : ℕ) : ↑(partition T ω).card ≤ (partitionConstant * Real.log ↑T) ^ ω ^ 2

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

The integer pairs with real upper cutoff T.

Equations

• LiLiuPrereqFouvry.CoprimePartition.realAdmissiblePairs T ω = LiLiuPrereqFouvry.CoprimePartition.admissiblePairs ⌊T⌋₊ ω

theorem LiLiuPrereqFouvry.CoprimePartition.mem_realAdmissiblePairs {T : ℝ} (hT : 0 ≤ T) {ω : ℕ} {a : ℕ × ℕ} : a ∈ realAdmissiblePairs 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.realPartition (T : ℝ) (ω : ℕ) : Finset (Finset (ℕ × ℕ))

Equations

• LiLiuPrereqFouvry.CoprimePartition.realPartition T ω = LiLiuPrereqFouvry.CoprimePartition.partition ⌊T⌋₊ ω

theorem LiLiuPrereqFouvry.CoprimePartition.realPartition_nonempty {T : ℝ} {ω : ℕ} {s : Finset (ℕ × ℕ)} (hs : s ∈ realPartition T ω) : s.Nonempty

theorem LiLiuPrereqFouvry.CoprimePartition.realPartition_pairwise_disjoint (T : ℝ) (ω : ℕ) : (↑(realPartition T ω)).PairwiseDisjoint id

theorem LiLiuPrereqFouvry.CoprimePartition.realPartition_cover (T : ℝ) (ω : ℕ) : (realPartition T ω).biUnion id = realAdmissiblePairs T ω

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

theorem LiLiuPrereqFouvry.CoprimePartition.card_realPartition_le_log {T : ℝ} (hT : 2 ≤ T) (ω : ℕ) : ↑(realPartition T ω).card ≤ (partitionConstant * Real.log T) ^ ω ^ 2

theorem LiLiuPrereqFouvry.CoprimePartition.sum_realPartition {M : Type u_1} [AddCommMonoid M] (T : ℝ) (ω : ℕ) (f : ℕ × ℕ → M) : ∑ s ∈ realPartition T ω, ∑ a ∈ s, f a = ∑ a ∈ realAdmissiblePairs T ω, f a

theorem LiLiuPrereqFouvry.CoprimePartition.fouvry_coprime_partition : ∃ (C : ℝ), 0 < C ∧ ∀ (T : ℝ), 2 ≤ T → ∀ (ω : ℕ), ∃ (P : Finset (Finset (ℕ × ℕ))), (∀ s ∈ P, s.Nonempty) ∧ (↑P).PairwiseDisjoint id ∧ P.biUnion id = realAdmissiblePairs T ω ∧ (∀ s ∈ P, ∀ a ∈ s, ∀ b ∈ s, a.1.Coprime b.2) ∧ ↑P.card ≤ (C * Real.log T) ^ ω ^ 2

F87, Lemma 7, with a constructed finite partition and an explicit absolute constant. The statement also allows ω = 0; the printed lemma only requires ω ≥ 1.