Canonical prime-support splitting

Separate the full prime powers in n according to whether their primes divide d. These are the d-infinity factors used in Fouvry (1984), pp. 235–236. The definitions are total; reconstruction requires only 0 < n.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.supportedPart (n d : ℕ) : ℕ

The factor of n containing the full powers of primes dividing d.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.supportedPart n d = ∏ p ∈ n.primeFactors with p ∣ d, p ^ n.factorization p

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePart (n d : ℕ) : ℕ

The complementary factor of n, containing primes not dividing d.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePart n d = ∏ p ∈ n.primeFactors with ¬p ∣ d, p ^ n.factorization p

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.supportedPart_pos (n d : ℕ) : 0 < supportedPart n d

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePart_pos (n d : ℕ) : 0 < coprimePart n d

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.supportedPart_mul_coprimePart {n : ℕ} (hn : 0 < n) (d : ℕ) : supportedPart n d * coprimePart n d = n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.supportedPart_dvd {n : ℕ} (hn : 0 < n) (d : ℕ) : supportedPart n d ∣ n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePart_dvd {n : ℕ} (hn : 0 < n) (d : ℕ) : coprimePart n d ∣ n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.prime_dvd_supportedPart {n d p : ℕ} (hp : Nat.Prime p) (hps : p ∣ supportedPart n d) : p ∣ d

Every prime divisor of the supported part divides the reference integer.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.prime_dvd_coprimePart_not_dvd {n d p : ℕ} (hp : Nat.Prime p) (hpt : p ∣ coprimePart n d) : ¬p ∣ d

Every prime divisor of the complementary part avoids the reference integer.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePart_coprime (n d : ℕ) : (coprimePart n d).Coprime d

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprime_of_prime_support {u d s : ℕ} (hu : u.Coprime d) (hs : ∀ (p : ℕ), Nat.Prime p → p ∣ s → p ∣ d) : u.Coprime s

Coprimality transfers from d to every integer supported on primes dividing d.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePart_coprime_supportedPart (n d : ℕ) : (coprimePart n d).Coprime (supportedPart n d)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dvd_supportedPart_of_prime_support {n d s : ℕ} (hn : 0 < n) (hsn : s ∣ n) (hs : ∀ (p : ℕ), Nat.Prime p → p ∣ s → p ∣ d) : s ∣ supportedPart n d

Every supported divisor of n divides its canonical supported part.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.dvd_coprimePart_of_coprime {n d t : ℕ} (hn : 0 < n) (htn : t ∣ n) (htd : t.Coprime d) : t ∣ coprimePart n d

Every divisor of n coprime to d divides the complementary part.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.prime_support_split_unique {n d s t : ℕ} (hn : 0 < n) (hst : s * t = n) (hs : ∀ (p : ℕ), Nat.Prime p → p ∣ s → p ∣ d) (ht : t.Coprime d) : s = supportedPart n d ∧ t = coprimePart n d

The prime-support conditions determine both factors, including unit factors.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.prime_support_split_iff {n d s t : ℕ} (hn : 0 < n) : s * t = n ∧ (∀ (p : ℕ), Nat.Prime p → p ∣ s → p ∣ d) ∧ t.Coprime d ↔ s = supportedPart n d ∧ t = coprimePart n d

An exact characterization suitable for reindexing by the two factors.

@[simp]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.supportedPart_one_left (d : ℕ) : supportedPart 1 d = 1

@[simp]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePart_one_left (d : ℕ) : coprimePart 1 d = 1

@[simp]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.supportedPart_one_right (n : ℕ) : supportedPart n 1 = 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePart_one_right {n : ℕ} (hn : 0 < n) : coprimePart n 1 = n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.supportedPart_eq_one_of_coprime {n d : ℕ} (hn : 0 < n) (hnd : n.Coprime d) : supportedPart n d = 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePart_eq_self_of_coprime {n d : ℕ} (hn : 0 < n) (hnd : n.Coprime d) : coprimePart n d = n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.supportedPart_eq_self_of_prime_support {n d : ℕ} (hn : 0 < n) (hs : ∀ (p : ℕ), Nat.Prime p → p ∣ n → p ∣ d) : supportedPart n d = n

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.coprimePart_eq_one_of_prime_support {n d : ℕ} (hn : 0 < n) (hs : ∀ (p : ℕ), Nat.Prime p → p ∣ n → p ∣ d) : coprimePart n d = 1