Convolution across disjoint prime boxes

Disjoint prime ranges, unlike arbitrary bounded coefficients, give a unique nonzero factorization at each integer. This controls convolutions of normalized boxes and also allows an already constructed small-prime weight as a factor.

def MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSupported (B : Finset ℕ) (f : ArithmeticFunction ℝ) : Prop

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.PrimeSupported B f = ∀ (n : ℕ), f n ≠ 0 → n.primeFactors ⊆ B

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeSupported_mono {B C : Finset ℕ} {f : ArithmeticFunction ℝ} (hf : PrimeSupported B f) (hBC : B ⊆ C) : PrimeSupported C f

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeSupported_smul {B : Finset ℕ} {f : ArithmeticFunction ℝ} (hf : PrimeSupported B f) (r : ℝ) : PrimeSupported B (r • f)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeSupported_one (B : Finset ℕ) : PrimeSupported B 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeSupported_mul {B C : Finset ℕ} {f g : ArithmeticFunction ℝ} (hf : PrimeSupported B f) (hg : PrimeSupported C g) : PrimeSupported (B ∪ C) (f * g)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.coprime_of_separated_primes {B C : Finset ℕ} (hBC : Disjoint B C) {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) (hmB : m.primeFactors ⊆ B) (hnC : n.primeFactors ⊆ C) : m.Coprime n

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.separated_factorization_unique {B C : Finset ℕ} (hBC : Disjoint B C) {f g : ArithmeticFunction ℝ} (hf : PrimeSupported B f) (hg : PrimeSupported C g) {d e : ℕ × ℕ} (hd : f d.1 * g d.2 ≠ 0) (he : f e.1 * g e.2 ≠ 0) (hprod : d.1 * d.2 = e.1 * e.2) : d = e

Two nonzero decompositions into the same disjoint prime ranges agree, even when prime powers occur in either factor.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boundedOne_mul_of_disjoint {B C : Finset ℕ} (hBC : Disjoint B C) {f g : ArithmeticFunction ℝ} (hf : PrimeSupported B f) (hg : PrimeSupported C g) (hfb : BoundedOne f) (hgb : BoundedOne g) : BoundedOne (f * g)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeBox_primeSupported (B : Finset ℕ) : PrimeSupported B ↑(primeBox B)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeSupported_pow {B : Finset ℕ} {f : ArithmeticFunction ℝ} (hf : PrimeSupported B f) (k : ℕ) : PrimeSupported B (f ^ k)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxWeight_primeSupported (B : Finset ℕ) (k : ℕ) : PrimeSupported B (boxWeight B k)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeSupported_prod {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (f : ι → ArithmeticFunction ℝ) (hf : ∀ i ∈ s, PrimeSupported (B i) (f i)) : PrimeSupported (s.biUnion B) (∏ i ∈ s, f i)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boundedOne_prod_of_pairwise_disjoint {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (f : ι → ArithmeticFunction ℝ) (hdisj : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → i ≠ j → Disjoint (B i) (B j)) (hf : ∀ i ∈ s, PrimeSupported (B i) (f i)) (hb : ∀ i ∈ s, BoundedOne (f i)) : BoundedOne (∏ i ∈ s, f i)

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.boxProduct {ι : Type u_1} (s : Finset ι) (B : ι → Finset ℕ) (k : ι → ℕ) : ArithmeticFunction ℝ

The normalized multi-box weight, fixed independently of all slot splits.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.boxProduct s B k = ∏ i ∈ s, MathlibNt.SieveTheory.LiLiuPrereqWF.boxWeight (B i) (k i)

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.boxLeftProduct {ι : Type u_1} (s : Finset ι) (B : ι → Finset ℕ) (a b : ι → ℕ) : ArithmeticFunction ℝ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.boxLeftProduct s B a b = ∏ i ∈ s, (↑(a i).factorial * ↑(b i).factorial / ↑(a i + b i).factorial) • MathlibNt.SieveTheory.LiLiuPrereqWF.boxWeight (B i) (a i)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProduct_primeSupported {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (k : ι → ℕ) : PrimeSupported (s.biUnion B) (boxProduct s B k)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProduct_boundedOne {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (k : ι → ℕ) (hdisj : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → i ≠ j → Disjoint (B i) (B j)) : BoundedOne (boxProduct s B k)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxLeftProduct_primeSupported {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (a b : ι → ℕ) : PrimeSupported (s.biUnion B) (boxLeftProduct s B a b)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxLeftProduct_boundedOne {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (a b : ι → ℕ) (hdisj : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → i ≠ j → Disjoint (B i) (B j)) : BoundedOne (boxLeftProduct s B a b)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProduct_split {ι : Type u_1} (s : Finset ι) (B : ι → Finset ℕ) (k a b : ι → ℕ) (hab : ∀ i ∈ s, a i + b i = k i) : boxProduct s B k = boxLeftProduct s B a b * boxProduct s B b

Exact multi-box convolution, without any squarefree restriction.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.smallWeight_boxProduct_bounded_split {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (k a b : ι → ℕ) (hab : ∀ i ∈ s, a i + b i = k i) (hdisj : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → i ≠ j → Disjoint (B i) (B j)) (B₀ : Finset ℕ) (ψ : ArithmeticFunction ℝ) (hsep : Disjoint B₀ (s.biUnion B)) (hψ : PrimeSupported B₀ ψ) (hψb : BoundedOne ψ) : ψ * boxProduct s B k = ψ * boxLeftProduct s B a b * boxProduct s B b ∧ BoundedOne (ψ * boxLeftProduct s B a b) ∧ BoundedOne (boxProduct s B b)

The small-prime factor is supplied as an actual function with bounded coefficients and separated prime support, not as a sieve conclusion record.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.prod_smul_convolution {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (r : ι → ℝ) (f : ι → ArithmeticFunction ℝ) : (∏ i ∈ s, r i) • ∏ i ∈ s, f i = ∏ i ∈ s, r i • f i

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.factorial_mul_boxProduct {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (k : ι → ℕ) : ↑(∏ i ∈ s, (k i).factorial) • boxProduct s B k = ∏ i ∈ s, ↑(primeBox (B i)) ^ k i

Factorial copies recover the original product of labelled-slot powers.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.sum_copies_boxProduct {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (k : ι → ℕ) (n : ℕ) : ∑ _j ∈ Finset.range (∏ i ∈ s, (k i).factorial), (boxProduct s B k) n = (∏ i ∈ s, ↑(primeBox (B i)) ^ k i) n