Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvryWPhaseThreeFactor

The three-factor reciprocal phase of the actual W residue #

Fouvry (1984), p. 238, (8.13)--(8.15), and Fouvry (1987), p. 627, (3.11). The integer parameters describe an already admissible five-gcd piece. We prove the phase transformation, not the partition into such pieces or its error bound. Every inverse below is a signed Bezout inverse modulo its displayed denominator.

source
theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue_phase_threeFactor {q r d d₁ D k₁ k₂ n₁ n₂ : ℕ} (hd : 0 < d) (hd₁ : 0 < d₁) (hDpos : 0 < D) (hk₁ : 0 < k₁) (hk₂ : 0 < k₂) (hn₁ : 0 < n₁) (hL : q.lcm r = D * k₁ * k₂) (hk₁q : k₁ ∣ q) (hk₂r : k₂ ∣ r) (hD : (k₁ * k₂).Coprime D) (hD' : (n₁ * k₁ * k₂).Coprime (d * d₁ * D)) (hk : k₁.Coprime (n₁ * k₂)) (hn₂ : n₂.Coprime (n₁ * k₂)) (hc : WCompatible q r (d * d₁ * n₁) (d * n₂)) (a : ℤ) :
have D' := d * d₁ * D; have b := productCRTResidue q r (d * d₁ * n₁) (d * n₂) a; ↑(↑b / ↑(q.lcm r)) = ↑(↑b * ↑(wPhaseInverse (k₁ * k₂) D) / ↑D - ↑a * ↑(wPhaseInverse (n₁ * k₁ * k₂) D') / ↑D') + ↑(↑a / (↑n₁ * ↑k₁ * ↑k₂ * ↑D')) + ↑(↑a * (↑d₁ * ↑n₁ - ↑n₂) * ↑(wPhaseInverse (D' * n₂ * k₁) (n₁ * k₂)) / (↑n₁ * ↑k₂))

Exact source three-factor phase of the existing product CRT residue. D' = d*d₁*D; the genuine reciprocal denominator is n₁*k₂. The original multipliers are d*d₁*n₁ and d*n₂, and the original moduli can be noncoprime. The hypotheses are arithmetic factorization/coprimality conditions, not supplied phase identities.

Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue_phase_threeFactor · compiled type and proof/definition references.

source
theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue_fourier_threeFactor {q r d d₁ D k₁ k₂ n₁ n₂ : ℕ} (hd : 0 < d) (hd₁ : 0 < d₁) (hDpos : 0 < D) (hk₁ : 0 < k₁) (hk₂ : 0 < k₂) (hn₁ : 0 < n₁) (hL : q.lcm r = D * k₁ * k₂) (hk₁q : k₁ ∣ q) (hk₂r : k₂ ∣ r) (hD : (k₁ * k₂).Coprime D) (hD' : (n₁ * k₁ * k₂).Coprime (d * d₁ * D)) (hk : k₁.Coprime (n₁ * k₂)) (hn₂ : n₂.Coprime (n₁ * k₂)) (hc : WCompatible q r (d * d₁ * n₁) (d * n₂)) (a h : ℤ) :
have D' := d * d₁ * D; have b := productCRTResidue q r (d * d₁ * n₁) (d * n₂) a; (fourier h) ↑(↑b / ↑(q.lcm r)) = (fourier h) ↑(↑b * ↑(wPhaseInverse (k₁ * k₂) D) / ↑D - ↑a * ↑(wPhaseInverse (n₁ * k₁ * k₂) D') / ↑D') * (fourier h) ↑(↑a / (↑n₁ * ↑k₁ * ↑k₂ * ↑D')) * (fourier h) ↑(↑a * (↑d₁ * ↑n₁ - ↑n₂) * ↑(wPhaseInverse (D' * n₂ * k₁) (n₁ * k₂)) / (↑n₁ * ↑k₂))

The three factors are root-of-unity phases modulo D,D', the slow real phase, and the incomplete reciprocal phase modulo n₁*k₂.

Inspect dependencies

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.productCRTResidue_fourier_threeFactor · compiled type and proof/definition references.

source
noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wThreeFactorPoissonFrequency (M : ℝ) (a : ℤ) (q r d d₁ D k₁ k₂ n₁ n₂ : ℕ) (h : ℤ) :
ℂ

Three-factor representation of the original W frequency on an admissible arithmetic piece. The original Fourier transform, signs, and zero cutoff remain.

Equations
Instances For
    Inspect dependencies

    MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wThreeFactorPoissonFrequency · compiled type and proof/definition references.

    source
    theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency_eq_threeFactor {q r d d₁ D k₁ k₂ n₁ n₂ : ℕ} (hd : 0 < d) (hd₁ : 0 < d₁) (hDpos : 0 < D) (hk₁ : 0 < k₁) (hk₂ : 0 < k₂) (hn₁ : 0 < n₁) (hL : q.lcm r = D * k₁ * k₂) (hk₁q : k₁ ∣ q) (hk₂r : k₂ ∣ r) (hD : (k₁ * k₂).Coprime D) (hD' : (n₁ * k₁ * k₂).Coprime (d * d₁ * D)) (hk : k₁.Coprime (n₁ * k₂)) (hn₂ : n₂.Coprime (n₁ * k₂)) (hc : WCompatible q r (d * d₁ * n₁) (d * n₂)) (M : ℝ) (a h : ℤ) :
    wPoissonFrequency M a q r (d * d₁ * n₁) (d * n₂) h = wThreeFactorPoissonFrequency M a q r d d₁ D k₁ k₂ n₁ n₂ h
    Inspect dependencies

    MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency_eq_threeFactor · compiled type and proof/definition references.

    source
    theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency_threeFactor_piece {q r d d₁ D k₁ k₂ : ℕ} (hd : 0 < d) (hd₁ : 0 < d₁) (hDpos : 0 < D) (hk₁ : 0 < k₁) (hk₂ : 0 < k₂) (hL : q.lcm r = D * k₁ * k₂) (hk₁q : k₁ ∣ q) (hk₂r : k₂ ∣ r) (hD : (k₁ * k₂).Coprime D) (N₁ N₂ : Finset ℕ) (hN₁ : ∀ n₁ ∈ N₁, 0 < n₁ ∧ (n₁ * k₁ * k₂).Coprime (d * d₁ * D) ∧ k₁.Coprime (n₁ * k₂)) (hN₂ : ∀ n₁ ∈ N₁, ∀ n₂ ∈ N₂, n₂.Coprime (n₁ * k₂)) (M : ℝ) (a : ℤ) (H : ℕ) (β c : ℕ → ℝ) :
    (∑ n₁ ∈ N₁, ∑ n₂ ∈ N₂, if WCompatible q r (d * d₁ * n₁) (d * n₂) then c q * c r * β (d * d₁ * n₁) * β (d * n₂) * (∑ h ∈ Finset.Icc (-↑H) ↑H, wPoissonFrequency M a q r (d * d₁ * n₁) (d * n₂) h).re else 0) = ∑ n₁ ∈ N₁, ∑ n₂ ∈ N₂, if WCompatible q r (d * d₁ * n₁) (d * n₂) then c q * c r * β (d * d₁ * n₁) * β (d * n₂) * (∑ h ∈ Finset.Icc (-↑H) ↑H, wThreeFactorPoissonFrequency M a q r d d₁ D k₁ k₂ n₁ n₂ h).re else 0

    Exact finite W piece after the arithmetic partition. The two natural-index sets need not be intervals, and the full signed original coefficients remain. This does not assert that every tuple in raw W satisfies these coprimalities.

    Inspect dependencies

    MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wPoissonFrequency_threeFactor_piece · compiled type and proof/definition references.