Finite density of large square divisors

The union over square divisors has an exact finite range and a floor-sum majorant. The elementary inverse-square tail gives the uniform constant 2, including cutoffs below one and empty intervals.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.largeSquareDivisorSet (T : ℕ) (Z : ℝ) : Finset ℕ

Positive integers at most T with a square divisor whose root exceeds Z.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.largeSquareDivisorSet T Z = {n ∈ Finset.Ioc 0 T | ∃ (b : ℕ), Z < ↑b ∧ b ^ 2 ∣ n}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.largeSquareDivisorSet_eq_biUnion (T : ℕ) {Z : ℝ} (hZ : 0 ≤ Z) : largeSquareDivisorSet T Z = (Finset.Ioc ⌊Z⌋₊ T.sqrt).biUnion fun (b : ℕ) => {n ∈ Finset.Ioc 0 T | b ^ 2 ∣ n}

The square-root upper endpoint and the floor lower endpoint are exact.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.card_largeSquareDivisorSet_le_floor_sum (T : ℕ) {Z : ℝ} (hZ : 0 ≤ Z) : (largeSquareDivisorSet T Z).card ≤ ∑ b ∈ Finset.Ioc ⌊Z⌋₊ T.sqrt, T / b ^ 2

An exact integer floor-sum majorant, with no asymptotic endpoint convention.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.card_largeSquareDivisorSet_le_floor (T : ℕ) {Z : ℝ} (hZ : 0 ≤ Z) : ↑(largeSquareDivisorSet T Z).card ≤ 2 * ↑T / (↑⌊Z⌋₊ + 1)

A uniform reciprocal-square estimate retains the natural floor at the cutoff.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.card_largeSquareDivisorSet_le (T : ℕ) {Z : ℝ} (hZ : 0 < Z) : ↑(largeSquareDivisorSet T Z).card ≤ 2 * ↑T / Z

Large square divisors have density at most 2 / Z for every positive cutoff.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.card_largeSquareDivisorSet_le_real {T Z : ℝ} (hT : 0 ≤ T) (hZ : 0 < Z) : ↑(largeSquareDivisorSet ⌊T⌋₊ Z).card ≤ 2 * T / Z

Real upper endpoints are truncated exactly before the density estimate.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mem_largeSquareDivisorSet_of_large_support {n s d T : ℕ} {Y : ℝ} (hn : n ∈ Finset.Ioc 0 T) (hs : 0 < s) (hd : 0 < d) (hY : 0 ≤ Y) (hlarge : Y < ↑s) (hsd : ∀ (p : ℕ), Nat.Prime p → p ∣ s → p ∣ d) (hdsn : d * s ∣ n) : n ∈ largeSquareDivisorSet T √Y

Any supported factor above Y forces membership in the sparse square-divisor set.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.card_largeSupport_le {T Y : ℝ} (hT : 0 ≤ T) (hY : 0 < Y) (S : Finset ℕ) (hS : S ⊆ Finset.Ioc 0 ⌊T⌋₊) (hs : ∀ n ∈ S, ∃ (s : ℕ) (d : ℕ), 0 < s ∧ 0 < d ∧ Y < ↑s ∧ (∀ (p : ℕ), Nat.Prime p → p ∣ s → p ∣ d) ∧ d * s ∣ n) : ↑S.card ≤ 2 * T / √Y

A uniform sparse envelope, even when the supported factor and d vary with n.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGCDData_mem_largeSquareDivisorSet (q r N₂ : ℕ) {N₁ T : ℕ} {Y : ℝ} (hN₁ : N₁ ∈ Finset.Ioc 0 T) (hY : 0 ≤ Y) (hlarge : Y < ↑(wGCDData q r N₁ N₂).d₁) : N₁ ∈ largeSquareDivisorSet T √Y

The actual canonical d₁ cutoff embeds in the same sparse envelope.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.largeSupportPairs (N : Finset ℕ) (Y : ℝ) : Finset (ℕ × ℕ)

Ordered pairs with large canonical d₁, independently of the moduli q,r.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.largeSupportPairs N Y = {p ∈ N ×ˢ N | Y < ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.supportedPart (p.1 / p.1.gcd p.2) (p.1.gcd p.2))}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.largeSupportPairs_subset (N : Finset ℕ) {T : ℕ} {Y : ℝ} (hN : N ⊆ Finset.Ioc 0 T) (hY : 0 ≤ Y) : largeSupportPairs N Y ⊆ largeSquareDivisorSet T √Y ×ˢ N

The large-d₁ pair set is contained in a sparse first-coordinate strip.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.card_largeSupportPairs_le {T Y : ℝ} (hT : 0 ≤ T) (hY : 0 < Y) (N : Finset ℕ) (hN : N ⊆ Finset.Ioc 0 ⌊T⌋₊) : ↑(largeSupportPairs N Y).card ≤ 2 * T ^ 2 / √Y

A finite pair-count input for Cauchy--Schwarz; no coefficient estimates enter.