Canonical extraction of a divisor from two positive factors

Fouvry (1987), p. 627, §III.5, the finite identity immediately before (3.12). Here the extracted divisor is called D; in that identity it is δ δ₂, not the three-factor phase modulus δ δ₁ δ₂. The split is determined by Δ' = gcd D s, using gcd cancellation only.

@[reducible, inline]

abbrev MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.FactorExtractionTuple : Type

Coordinates ((Δ, Δ'), (r', s')).

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.FactorExtractionTuple = ((ℕ × ℕ) × ℕ × ℕ)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorExtraction (D r s : ℕ) : FactorExtractionTuple

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorExtraction D r s = ((D / D.gcd s, D.gcd s), r / (D / D.gcd s), s / D.gcd s)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.FactorExtractionValid (D r s : ℕ) (e : FactorExtractionTuple) : Prop

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.FactorExtractionValid D r s e = (0 < e.1.1 ∧ 0 < e.1.2 ∧ 0 < e.2.1 ∧ 0 < e.2.2 ∧ D = e.1.1 * e.1.2 ∧ r = e.1.1 * e.2.1 ∧ s = e.1.2 * e.2.2 ∧ e.2.2.Coprime e.1.1)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorExtraction_valid {D r s : ℕ} (hD : 0 < D) (hr : 0 < r) (hs : 0 < s) (hd : D ∣ r * s) : FactorExtractionValid D r s (factorExtraction D r s)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorExtraction_unique {D r s : ℕ} {e : FactorExtractionTuple} (he : FactorExtractionValid D r s e) : e = factorExtraction D r s

Reconstruction and the single coprimality condition force all four coordinates, so the change of variables has no multiplicity.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorExtraction_existsUnique {D r s : ℕ} (hD : 0 < D) (hr : 0 < r) (hs : 0 < s) (hd : D ∣ r * s) : ∃! e : FactorExtractionTuple, FactorExtractionValid D r s e

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorExtractionSource {ι : Type u_1} (R S : ℕ) (U : Finset ι) (P : ℕ → ℕ → ι → Prop) : Finset ((ℕ × ℕ) × ι)

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorExtractionSource R S U P = {z ∈ (Finset.Ioc 0 R ×ˢ Finset.Ioc 0 S) ×ˢ U | P z.1.1 z.1.2 z.2}

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorExtractionReconstruct {ι : Type u_1} (z : FactorExtractionTuple × ι) : (ℕ × ℕ) × ι

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorExtractionReconstruct z = ((z.1.1.1 * z.1.2.1, z.1.1.2 * z.1.2.2), z.2)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorExtractionTarget {ι : Type u_1} (R S : ℕ) (U : Finset ι) (D : ℕ → ℕ → ι → ℕ) (P : ℕ → ℕ → ι → Prop) : Finset (FactorExtractionTuple × ι)

An explicit broad four-dimensional box with the original support and mask, the divisor equation, and the primitive condition as exact filters. In particular this is not defined as the image of the old index set.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.factorExtractionTarget R S U D P = {z ∈ ((Finset.Ioc 0 R ×ˢ Finset.Ioc 0 S) ×ˢ Finset.Ioc 0 R ×ˢ Finset.Ioc 0 S) ×ˢ U | have r := z.1.1.1 * z.1.2.1; have s := z.1.1.2 * z.1.2.2; r ≤ R ∧ s ≤ S ∧ P r s z.2 ∧ D r s z.2 = z.1.1.1 * z.1.1.2 ∧ z.1.2.2.Coprime z.1.1.1}

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_factorExtraction {ι : Type u_1} {A : Type u_2} [AddCommMonoid A] (R S : ℕ) (U : Finset ι) (D : ℕ → ℕ → ι → ℕ) (P : ℕ → ℕ → ι → Prop) (hD : ∀ z ∈ factorExtractionSource R S U P, 0 < D z.1.1 z.1.2 z.2 ∧ D z.1.1 z.1.2 z.2 ∣ z.1.1 * z.1.2) (F : (ℕ × ℕ) × ι → A) : ∑ z ∈ factorExtractionSource R S U P, F z = ∑ z ∈ factorExtractionTarget R S U D P, F (factorExtractionReconstruct z)

A finite bijection for a divisor which may depend on the reconstructed factors and every surviving auxiliary variable. All original masks remain.