Inverse-totient mass of moduli divisible by large prime squares

These finite estimates concern the canonical mass 1 / φ(n), independently of any sieve weight or choice of a well-factorable family.

The divisor identity ∑ d ∣ n, φ(d) = n gives the majorant τ(n) / n; enlarging the divisor-pair region to a square gives the bound H(T)^2. Supermultiplicativity of the totient then handles each prime square, and a finite inverse-square tail gives 4 H(T)^2 / u for primes at least u > 0. No assertion about the support or coefficients of a sieve family is used.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.harmonicSum (T : ℕ) : ℝ

The finite harmonic sum over positive integers at most T.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.harmonicSum T = ∑ n ∈ Finset.Icc 1 T, (↑n)⁻¹

def MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.badModuli (T : ℕ) (R : Finset ℕ) : Finset ℕ

Positive moduli at most T with a repeated prime from R.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.badModuli T R = {n ∈ Finset.Icc 1 T | ∃ p ∈ R, p ^ 2 ∣ n}

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.sum_multiples_le (T d : ℕ) (hd : 0 < d) (f : ℕ → ℝ) (hf : ∀ (n : ℕ), 0 ≤ f n) : ∑ n ∈ Finset.Icc 1 T with d ∣ n, f n ≤ ∑ m ∈ Finset.Icc 1 T, f (d * m)

Enlarging the quotient range bounds a nonnegative sum over multiples.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.inv_totient_le_divisor_sum (n : ℕ) (hn : 0 < n) : (↑n.totient)⁻¹ ≤ ∑ _d ∈ n.divisors, (↑n)⁻¹

The divisor-count majorant for the inverse totient.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.sum_inv_totient_le_harmonic_sq (T : ℕ) : ∑ n ∈ Finset.Icc 1 T, (↑n.totient)⁻¹ ≤ harmonicSum T ^ 2

A finite, elementary mean bound, without an asymptotic constant.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.sum_inv_totient_multiples_le (T d : ℕ) (hd : 0 < d) : ∑ n ∈ Finset.Icc 1 T with d ∣ n, (↑n.totient)⁻¹ ≤ (↑d.totient)⁻¹ * harmonicSum T ^ 2

A fixed divisor costs at most its inverse totient in the finite mean bound.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.badModuli_mass_le_totient_tail (T : ℕ) (R : Finset ℕ) (hR : ∀ p ∈ R, Nat.Prime p) : ∑ n ∈ badModuli T R, (↑n.totient)⁻¹ ≤ (∑ p ∈ R, (↑(p ^ 2).totient)⁻¹) * harmonicSum T ^ 2

The union bound retains the sharper exact finite inverse-totient prime tail.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.inv_totient_prime_sq_le {p : ℕ} (hp : Nat.Prime p) : (↑(p ^ 2).totient)⁻¹ ≤ 2 * (↑p ^ 2)⁻¹

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.badModuli_mass_le_prime_sq_tail (T : ℕ) (R : Finset ℕ) (hR : ∀ p ∈ R, Nat.Prime p) : ∑ n ∈ badModuli T R, (↑n.totient)⁻¹ ≤ (2 * ∑ p ∈ R, (↑p ^ 2)⁻¹) * harmonicSum T ^ 2

The explicit prime-square tail form of the bad-modulus mass estimate.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.sum_inv_sq_le_of_lower_bound (R : Finset ℕ) (u : ℝ) (hu : 0 < u) (hR : ∀ p ∈ R, u ≤ ↑p) : ∑ p ∈ R, (↑p ^ 2)⁻¹ ≤ 2 / u

An inverse-square tail estimate for any finite set above a positive real cutoff.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.badModuli_mass_le_harmonic (T : ℕ) (R : Finset ℕ) (u : ℝ) (hu : 0 < u) (hprime : ∀ p ∈ R, Nat.Prime p) (hlower : ∀ p ∈ R, u ≤ ↑p) : ∑ n ∈ badModuli T R, (↑n.totient)⁻¹ ≤ 4 / u * harmonicSum T ^ 2

Large repeated primes have total inverse-totient mass at most 4 H(T)^2 / u.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.harmonicSum_nonneg (T : ℕ) : 0 ≤ harmonicSum T

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.harmonicSum_le_one_add_log (T : ℕ) : harmonicSum T ≤ 1 + Real.log ↑T

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSquareMass.badModuli_mass_le_log (T : ℕ) (R : Finset ℕ) (u : ℝ) (hu : 0 < u) (hprime : ∀ p ∈ R, Nat.Prime p) (hlower : ∀ p ∈ R, u ≤ ↑p) : ∑ n ∈ badModuli T R, (↑n.totient)⁻¹ ≤ 4 / u * (1 + Real.log ↑T) ^ 2

The logarithmic form, valid also for T = 0 under Lean's log 0 = 0 convention.