Large prime support produces a large square divisor

For the d₁ exclusion in Fouvry (1984), (8.3), a large prime factor is unnecessary: a positive integer supported on the primes of d produces a square divisor of d * s at least as large as s.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.squarefree_dvd_of_prime_support {a d : ℕ} (ha : Squarefree a) (hd : 0 < d) (hs : ∀ (p : ℕ), Nat.Prime p → p ∣ a → p ∣ d) : a ∣ d

A squarefree integer supported on the primes of a positive integer divides it.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.exists_square_dvd_of_prime_support {s d : ℕ} (hs : 0 < s) (hd : 0 < d) (hsd : ∀ (p : ℕ), Nat.Prime p → p ∣ s → p ∣ d) : ∃ (b : ℕ), 0 < b ∧ s ≤ b ^ 2 ∧ b ^ 2 ∣ d * s

The square witness uses the squarefree part of s, so it need not contain any individually large prime.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.exists_square_dvd_of_supported_mul_dvd {s d n : ℕ} (hs : 0 < s) (hd : 0 < d) (hsd : ∀ (p : ℕ), Nat.Prime p → p ∣ s → p ∣ d) (hn : d * s ∣ n) : ∃ (b : ℕ), 0 < b ∧ s ≤ b ^ 2 ∧ b ^ 2 ∣ n

The extraction transfers to any multiple of d * s.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.WGCDData.Valid.exists_square_dvd_N₁ {v : WGCDData} {q r N₁ N₂ : ℕ} (hv : v.Valid q r N₁ N₂) : ∃ (b : ℕ), 0 < b ∧ v.d₁ ≤ b ^ 2 ∧ b ^ 2 ∣ N₁

In the five-gcd coordinates, a large d₁ forces a square divisor of N₁.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDData_exists_square_dvd_N₁ (q r N₂ : ℕ) {N₁ : ℕ} (hN₁ : 0 < N₁) : ∃ (b : ℕ), 0 < b ∧ (wGCDData q r N₁ N₂).d₁ ≤ b ^ 2 ∧ b ^ 2 ∣ N₁

The canonical supported quotient has the square witness without any hypothesis on the other modulus or the auxiliary indices.