A signed factorization and its high-omega deletion

The original weight is well-factorable at its original level, with closed factor supports. Only one legitimate split is chosen. Deleting high omega from the second factor produces a convolution, not a new well-factorable weight. Its discarded part has an actual divisor majorant and high-omega modulus support.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorConvolution (γ ζ : ℕ → ℝ) (q : ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorConvolution γ ζ q = ∑ p ∈ q.divisorsAntidiagonal, γ p.1 * ζ p.2

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorSupported (R : ℝ) (γ : ℕ → ℝ) : Prop

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorSupported R γ = ∀ (n : ℕ), γ n ≠ 0 → 0 < n ∧ ↑n ≤ R

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable (k : ℕ) (L : ℝ) (c : ℕ → ℝ) : Prop

The input weight itself has the stated order. The quantifier over splits comes after that single weight, and includes a factor level equal to one.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable k L c = ((∀ (q : ℕ), |c q| ≤ ↑((MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau k) q)) ∧ ∀ (R S : ℝ), 1 ≤ R → 1 ≤ S → R * S = L → ∃ (γ : ℕ → ℝ) (ζ : ℕ → ℝ), MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorSupported R γ ∧ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorSupported S ζ ∧ (∀ (r : ℕ), |γ r| ≤ ↑((MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau k) r)) ∧ (∀ (s : ℕ), |ζ s| ≤ ↑((MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.fouvryTau k) s)) ∧ c = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorConvolution γ ζ)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorConvolution_abs_le (j k : ℕ) (γ ζ : ℕ → ℝ) (hγ : ∀ (r : ℕ), |γ r| ≤ ↑((fouvryTau j) r)) (hζ : ∀ (s : ℕ), |ζ s| ≤ ↑((fouvryTau k) s)) (q : ℕ) : |factorConvolution γ ζ q| ≤ ↑((fouvryTau (j + k)) q)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorConvolution_supported {R S : ℝ} {γ ζ : ℕ → ℝ} (hγ : factorSupported R γ) (hζ : factorSupported S ζ) : factorSupported (R * S) (factorConvolution γ ζ)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorConvolution_eq_low_add_high (γ ζ : ℕ → ℝ) (ξ : ℝ) : factorConvolution γ ζ = fun (q : ℕ) => factorConvolution γ (betaLowOmega ζ ξ) q + factorConvolution γ (betaHighOmega ζ ξ) q

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorConvolution_sub_low (γ ζ : ℕ → ℝ) (ξ : ℝ) : (fun (q : ℕ) => factorConvolution γ ζ q - factorConvolution γ (betaLowOmega ζ ξ) q) = factorConvolution γ (betaHighOmega ζ ξ)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorConvolution_high_nonzero {γ ζ : ℕ → ℝ} {ξ : ℝ} {q : ℕ} (h : factorConvolution γ (betaHighOmega ζ ξ) q ≠ 0) : ξ < ↑q.primeFactors.card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorLowOmega_supported {S : ℝ} {ζ : ℕ → ℝ} (hζ : factorSupported S ζ) (ξ : ℝ) : factorSupported S (betaLowOmega ζ ξ)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorLowOmega_eq_self_at_one {ζ : ℕ → ℝ} (hζ : factorSupported 1 ζ) {ξ : ℝ} (hξ : 0 ≤ ξ) : betaLowOmega ζ ξ = ζ

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.SignedWellFactorable.c2_split {k : ℕ} {x ν ε : ℝ} {c : ℕ → ℝ} (hc : SignedWellFactorable k (x ^ ((5 - 5 * ν) / 9 - ε)) c) (hx : 1 ≤ x) (hε : 0 ≤ ε) (hεν : ε ≤ ν) (hν : ν ≤ 1 / 10) : have R := x ^ c2RExponent ν ε; have S := x ^ c2SExponent ν ε; R * S = x ^ ((5 - 5 * ν) / 9 - ε) ∧ ∃ (γ : ℕ → ℝ) (ζ : ℕ → ℝ), factorSupported R γ ∧ factorSupported S ζ ∧ (∀ (r : ℕ), |γ r| ≤ ↑((fouvryTau k) r)) ∧ (∀ (s : ℕ), |ζ s| ≤ ↑((fouvryTau k) s)) ∧ c = factorConvolution γ ζ

The original level is preserved exactly, including the near-endpoint branch where the second factor is supported only at one.