Closed-support common well-factorability

The function is fixed before all real level splits. The constructed example is one normalized prime box with one extra box-width of support slack; it is not the Iwaniec upper/lower sieve family and asserts no sieve density estimate.

def MathlibNt.SieveTheory.LiLiuPrereqWF.SupportedAt (f : ArithmeticFunction ℝ) (Q : ℝ) : Prop

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.SupportedAt f Q = ∀ (n : ℕ), f n ≠ 0 → ↑n ≤ Q

def MathlibNt.SieveTheory.LiLiuPrereqWF.BoundedOne (f : ArithmeticFunction ℝ) : Prop

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.BoundedOne f = ∀ (n : ℕ), |f n| ≤ 1

def MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable (f : ArithmeticFunction ℝ) (Q : ℝ) : Prop

Closed support, including the identity split. Equality of arithmetic functions is Dirichlet convolution equality on all natural numbers.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.WellFactorable f Q = (1 ≤ Q ∧ MathlibNt.SieveTheory.LiLiuPrereqWF.BoundedOne f ∧ MathlibNt.SieveTheory.LiLiuPrereqWF.SupportedAt f Q ∧ ∀ (Q₁ Q₂ : ℝ), 1 ≤ Q₁ → 1 ≤ Q₂ → Q₁ * Q₂ = Q → ∃ (a : ArithmeticFunction ℝ) (b : ArithmeticFunction ℝ), MathlibNt.SieveTheory.LiLiuPrereqWF.BoundedOne a ∧ MathlibNt.SieveTheory.LiLiuPrereqWF.SupportedAt a Q₁ ∧ MathlibNt.SieveTheory.LiLiuPrereqWF.BoundedOne b ∧ MathlibNt.SieveTheory.LiLiuPrereqWF.SupportedAt b Q₂ ∧ f = a * b)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.supportedAt_mono {f : ArithmeticFunction ℝ} {Q R : ℝ} (hf : SupportedAt f Q) (hQR : Q ≤ R) : SupportedAt f R

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.supportedAt_smul (r : ℝ) {f : ArithmeticFunction ℝ} {Q : ℝ} (hf : SupportedAt f Q) : SupportedAt (r • f) Q

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.supportedAt_mul {f g : ArithmeticFunction ℝ} {Q R : ℝ} (hf : SupportedAt f Q) (hg : SupportedAt g R) (hQ : 0 ≤ Q) : SupportedAt (f * g) (Q * R)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.supportedAt_one : SupportedAt 1 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.supportedAt_pow {f : ArithmeticFunction ℝ} {U : ℝ} (hf : SupportedAt f U) (hU : 0 ≤ U) (k : ℕ) : SupportedAt (f ^ k) (U ^ k)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeBox_supportedAt (B : Finset ℕ) {U : ℝ} (hB : ∀ p ∈ B, Nat.Prime p → ↑p ≤ U) : SupportedAt (↑(primeBox B)) U

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxWeight_supportedAt (B : Finset ℕ) {U : ℝ} (hU : 0 ≤ U) (hB : ∀ p ∈ B, Nat.Prime p → ↑p ≤ U) (k : ℕ) : SupportedAt (boxWeight B k) (U ^ k)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.exists_slot_split {U Q₁ Q₂ : ℝ} (hU : 1 ≤ U) (hQ₁ : 1 ≤ Q₁) (hQ₂ : 1 ≤ Q₂) (k : ℕ) (hsplit : Q₁ * Q₂ = U ^ (k + 1)) : ∃ (a : ℕ) (b : ℕ), a + b = k ∧ U ^ a ≤ Q₁ ∧ U ^ b ≤ Q₂

Allocation of k identical box widths with one extra width of slack.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxWeight_wellFactorable (B : Finset ℕ) {U : ℝ} (hU : 1 ≤ U) (hB : ∀ p ∈ B, Nat.Prime p → ↑p ≤ U) (k : ℕ) : WellFactorable (boxWeight B k) (U ^ (k + 1))

A concrete common WF weight. B and k are fixed before every level split; the only split-dependent objects are the two explicitly normalized factors.