Squarefree coefficients of the existing normalized box product

Each box multiplicity contributes one coefficient, not factorially many copies. The identities below concern the already defined full-integer arithmetic functions. No squarefree mask or density-transfer hypothesis is introduced.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.mul_apply_of_primeSupported {B C : Finset ℕ} (hBC : Disjoint B C) {f g : ArithmeticFunction ℝ} (hf : PrimeSupported B f) (hg : PrimeSupported C g) {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) (hmB : m.primeFactors ⊆ B) (hnC : n.primeFactors ⊆ C) : (f * g) (m * n) = f m * g n

Separated prime support determines the convolution factorization even when one of its coefficients vanishes. No squarefreeness is needed here.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxWeight_squarefree_eq_indicator (B : Finset ℕ) (k : ℕ) {n : ℕ} (hn : Squarefree n) : (boxWeight B k) n = if n.primeFactors ⊆ B ∧ n.primeFactors.card = k then 1 else 0

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProduct_primeProduct_eq_indicator {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (k : ι → ℕ) (hdisj : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → i ≠ j → Disjoint (B i) (B j)) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) : (boxProduct s B k) (P.prod id) = if P ⊆ s.biUnion B ∧ ∀ i ∈ s, (P ∩ B i).card = k i then 1 else 0

On a finite product of distinct primes, the normalized box product is the indicator of complete box support and the prescribed multiplicity in every box. The boxes themselves may contain nonprimes, which the existing weight ignores.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProduct_squarefree_eq_indicator {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (k : ι → ℕ) (hdisj : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → i ≠ j → Disjoint (B i) (B j)) {n : ℕ} (hn : Squarefree n) : (boxProduct s B k) n = if n.primeFactors ⊆ s.biUnion B ∧ ∀ i ∈ s, (n.primeFactors ∩ B i).card = k i then 1 else 0

The existing full-integer boxProduct has coefficient exactly one on the squarefree integers with the prescribed box counts, and zero on all other squarefree integers.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProduct_squarefree_eq_one_iff {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (k : ι → ℕ) (hdisj : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → i ≠ j → Disjoint (B i) (B j)) {n : ℕ} (hn : Squarefree n) : (boxProduct s B k) n = 1 ↔ n.primeFactors ⊆ s.biUnion B ∧ ∀ i ∈ s, (n.primeFactors ∩ B i).card = k i

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProduct_squarefree_eq_zero_iff {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (k : ι → ℕ) (hdisj : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → i ≠ j → Disjoint (B i) (B j)) {n : ℕ} (hn : Squarefree n) : (boxProduct s B k) n = 0 ↔ ¬(n.primeFactors ⊆ s.biUnion B ∧ ∀ i ∈ s, (n.primeFactors ∩ B i).card = k i)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.smallWeight_boxProduct_primeProduct_eq_indicator {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (k : ι → ℕ) (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₀ ψ) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) : (ψ * boxProduct s B k) (P.prod id) = if P ⊆ B₀ ∪ s.biUnion B ∧ ∀ i ∈ s, (P ∩ B i).card = k i then ψ ((P ∩ B₀).prod id) else 0

The actual small-prime coefficient survives the canonical small/big split. Only its prime support is assumed; no boundedness, sign, or sieve conclusion is required. A prescribed box multiplicity contributes once, not ∏ i, (k i)! times.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.smallWeight_boxProduct_squarefree_eq_indicator {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (k : ι → ℕ) (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₀ ψ) {n : ℕ} (hn : Squarefree n) : (ψ * boxProduct s B k) n = if n.primeFactors ⊆ B₀ ∪ s.biUnion B ∧ ∀ i ∈ s, (n.primeFactors ∩ B i).card = k i then ψ ((n.primeFactors ∩ B₀).prod id) else 0

Canonical small/big prime-factor splitting at every squarefree integer, including integers outside the combined prime support (where the value is zero).