Divided Dirichlet powers of a prime box

The normalization is performed on the full arithmetic function, not just its squarefree coefficients. Multiplicity is retained by taking factorially many copies when recovering the unnormalized power.

def MathlibNt.SieveTheory.LiLiuPrereqWF.primeBox (B : Finset ℕ) : ArithmeticFunction ℕ

The indicator of the primes in a finite box, including an explicit prime filter.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.primeBox B = { toFun := fun (n : ℕ) => if n ∈ B ∧ Nat.Prime n then 1 else 0, map_zero' := ⋯ }

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeBox_apply (B : Finset ℕ) (n : ℕ) : (primeBox B) n = if n ∈ B ∧ Nat.Prime n then 1 else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeBox_mul_apply (B : Finset ℕ) (g : ArithmeticFunction ℕ) (n : ℕ) : (primeBox B * g) n = ∑ p ∈ n.primeFactors, if p ∈ B then g (n / p) else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.cardFactors_div_prime_add_one {n p : ℕ} (hp : p ∈ n.primeFactors) : ArithmeticFunction.cardFactors n = 1 + ArithmeticFunction.cardFactors (n / p)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeBox_pow_eq_zero_of_cardFactors_ne (B : Finset ℕ) (k n : ℕ) (h : ArithmeticFunction.cardFactors n ≠ k) : (primeBox B ^ k) n = 0

A nonzero coefficient of the k-fold prime convolution has exactly k prime factors with multiplicity. This includes nonsquarefree integers.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeBox_pow_le_factorial (B : Finset ℕ) (k n : ℕ) : (primeBox B ^ k) n ≤ k.factorial

Factorial domination for every integer, proved by the prime-divisor recurrence and the distinction between distinct and repeated prime factors.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.dividedPower (f : ArithmeticFunction ℝ) (k : ℕ) : ArithmeticFunction ℝ

The real divided Dirichlet power; multiplication here is convolution.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.dividedPower f k = (↑k.factorial)⁻¹ • f ^ k

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.dividedPower_apply (f : ArithmeticFunction ℝ) (k n : ℕ) : (dividedPower f k) n = (f ^ k) n / ↑k.factorial

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.factorial_mul_dividedPower (f : ArithmeticFunction ℝ) (k : ℕ) : ↑k.factorial • dividedPower f k = f ^ k

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.smul_convolution (r s : ℝ) (f g : ArithmeticFunction ℝ) : r • f * s • g = (r * s) • (f * g)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.dividedPower_split (f : ArithmeticFunction ℝ) (a b : ℕ) : dividedPower f (a + b) = (↑a.factorial * ↑b.factorial / ↑(a + b).factorial) • dividedPower f a * dividedPower f b

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.factorial_ratio_pos (a b : ℕ) : 0 < ↑a.factorial * ↑b.factorial / ↑(a + b).factorial

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.factorial_ratio_le_one (a b : ℕ) : ↑a.factorial * ↑b.factorial / ↑(a + b).factorial ≤ 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.real_natCast_pow (f : ArithmeticFunction ℕ) (k : ℕ) : ↑f ^ k = ↑(f ^ k)

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.boxWeight (B : Finset ℕ) (k : ℕ) : ArithmeticFunction ℝ

The fixed normalized box weight. No split occurs in its definition.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.boxWeight B k = MathlibNt.SieveTheory.LiLiuPrereqWF.dividedPower (↑(MathlibNt.SieveTheory.LiLiuPrereqWF.primeBox B)) k

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxWeight_apply (B : Finset ℕ) (k n : ℕ) : (boxWeight B k) n = ↑((primeBox B ^ k) n) / ↑k.factorial

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxWeight_nonneg (B : Finset ℕ) (k n : ℕ) : 0 ≤ (boxWeight B k) n

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxWeight_le_one (B : Finset ℕ) (k n : ℕ) : (boxWeight B k) n ≤ 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxWeight_abs_le_one (B : Finset ℕ) (k n : ℕ) : |(boxWeight B k) n| ≤ 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeBox_pow_prime_pow (B : Finset ℕ) {p : ℕ} (hp : Nat.Prime p) (hpB : p ∈ B) (k : ℕ) : (primeBox B ^ k) (p ^ k) = 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxWeight_prime_pow (B : Finset ℕ) {p : ℕ} (hp : Nat.Prime p) (hpB : p ∈ B) (k : ℕ) : (boxWeight B k) (p ^ k) = (↑k.factorial)⁻¹

In particular the square of a box prime has coefficient 1/2, not zero.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.sum_copies_boxWeight (B : Finset ℕ) (k n : ℕ) : ∑ _j ∈ Finset.range k.factorial, (boxWeight B k) n = ↑((primeBox B ^ k) n)

The factorially many copies restore the original coefficient at every n, so any subsequent finite weighted sum is preserved as well.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxWeight_bounded_split (B : Finset ℕ) (a b : ℕ) : have left := (↑a.factorial * ↑b.factorial / ↑(a + b).factorial) • boxWeight B a; have right := boxWeight B b; boxWeight B (a + b) = left * right ∧ (∀ (n : ℕ), |left n| ≤ 1) ∧ ∀ (n : ℕ), |right n| ≤ 1

Explicit bounded factors for each division of the slots of the same box.