Fixed multi-box weights at every real level split

The hypothesis is the explicit numerical prefix-square condition on the list of actual prime upper bounds. Repeated labels retain their slot multiplicity. The subsequent LiLiuPrereqWFGeometry and LiLiuPrereqWFGeometricBoxes derive this condition with Iwaniec's geometric parameter losses. Constructing the complete signed sieve family with its density remains a separate task.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.supportedAt_prod {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (f : ι → ArithmeticFunction ℝ) (U : ι → ℝ) (hf : ∀ i ∈ s, SupportedAt (f i) (U i)) (hU : ∀ i ∈ s, 0 ≤ U i) : SupportedAt (∏ i ∈ s, f i) (∏ i ∈ s, U i)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProduct_supportedAt {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (k : ι → ℕ) (U : ι → ℝ) (hU : ∀ i ∈ s, 0 ≤ U i) (hB : ∀ i ∈ s, ∀ p ∈ B i, Nat.Prime p → ↑p ≤ U i) : SupportedAt (boxProduct s B k) (∏ i ∈ s, U i ^ k i)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxLeftProduct_supportedAt {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (B : ι → Finset ℕ) (a b : ι → ℕ) (U : ι → ℝ) (hU : ∀ i ∈ s, 0 ≤ U i) (hB : ∀ i ∈ s, ∀ p ∈ B i, Nat.Prime p → ↑p ≤ U i) : SupportedAt (boxLeftProduct s B a b) (∏ i ∈ s, U i ^ a i)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.prod_pow_list_count_of_subset {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (l : List ι) (U : ι → ℝ) (hl : l.toFinset ⊆ s) : ∏ i ∈ s, U i ^ List.count i l = (List.map U l).prod

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.list_boxProduct_factors {ι : Type u_1} [DecidableEq ι] (input : List ι) (B : ι → Finset ℕ) (U : ι → ℝ) {Q Q₁ Q₂ : ℝ} (hU : ∀ i ∈ input.toFinset, 0 ≤ U i) (hB : ∀ i ∈ input.toFinset, ∀ p ∈ B i, Nat.Prime p → ↑p ≤ U i) (hdisj : ∀ ⦃i : ι⦄, i ∈ input.toFinset → ∀ ⦃j : ι⦄, j ∈ input.toFinset → i ≠ j → Disjoint (B i) (B j)) (hprefix : LiLiuPrereqWFBoxAllocation.PrefixSquareBound U Q input) (hQ₁ : 1 ≤ Q₁) (hQ₂ : 1 ≤ Q₂) (hsplit : Q₁ * Q₂ = Q) : ∃ (f : ArithmeticFunction ℝ) (g : ArithmeticFunction ℝ), BoundedOne f ∧ SupportedAt f Q₁ ∧ BoundedOne g ∧ SupportedAt g Q₂ ∧ (boxProduct input.toFinset B fun (i : ι) => List.count i input) = f * g

The weight and its multiplicities are fixed by input, before selecting Q1,Q2. Only the occurrence partition and its two factors depend on the split.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.list_boxProduct_wellFactorable {ι : Type u_1} [DecidableEq ι] (input : List ι) (B : ι → Finset ℕ) (U : ι → ℝ) {Q : ℝ} (hQ : 1 ≤ Q) (hU : ∀ i ∈ input.toFinset, 0 ≤ U i) (hB : ∀ i ∈ input.toFinset, ∀ p ∈ B i, Nat.Prime p → ↑p ≤ U i) (hdisj : ∀ ⦃i : ι⦄, i ∈ input.toFinset → ∀ ⦃j : ι⦄, j ∈ input.toFinset → i ≠ j → Disjoint (B i) (B j)) (hprefix : LiLiuPrereqWFBoxAllocation.PrefixSquareBound U Q input) : WellFactorable (boxProduct input.toFinset B fun (a : ι) => List.count a input) Q