Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvrySecondaryGcdCost

The refined secondary mean for the actual individual-cancellation cost #

Only the nonnegative span and modulus factors are replaced by endpoint envelopes. The arithmetic square-root sum is still averaged in r.

source
noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramRCostEnvelope (ε C : ℝ) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) (n s s' lo hi : ℕ) :
ℝ
Equations
Instances For
    Inspect dependencies

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

    source
    theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramRCostEnvelope_nonneg {C : ℝ} (hC : 0 ≤ C) (ε : ℝ) (a : ℤ) (R S : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) (n s s' lo hi : ℕ) :
    0 ≤ wGramRCostEnvelope ε C a R S K j cap n s s' lo hi
    Inspect dependencies

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

    source
    theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramFouvryCost_le_rEnvelope {ε C : ℝ} (hε : 0 ≤ ε) (hC : 0 ≤ C) (a : ℤ) (R S M Z : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) {n n₂ n₂' s s' r lo hi : ℕ} {h h' : ℤ} (hn : 0 < n) (hs : 0 < s) (hs' : 0 < s') (hr : r ∈ Finset.Ioc lo hi) :
    wGramFouvryCost ε C a R S M Z K j cap ((r, n), (n₂, s, h), n₂', s', h') ≤ wGramRCostEnvelope ε C a R S K j cap n s s' lo hi * √↑((n * r * s * s').gcd (iv3CorrelationNumerator K.1.2.1 n n₂ n₂' s s' a h h').natAbs)
    Inspect dependencies

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

    source
    theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramFouvryCost_secondary_sum_refined {ε C : ℝ} (hε : 0 ≤ ε) (hC : 0 ≤ C) (a : ℤ) (R S M Z : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) {n n₂ n₂' s s' : ℕ} {h h' : ℤ} (hn : 0 < n) (hs : 0 < s) (hs' : 0 < s') (hsec : h' * ↑s = h * ↑s') (hl : iv3CorrelationNumerator K.1.2.1 n n₂ n₂' s s' a h h' ≠ 0) (lo hi : ℕ) :
    ∑ r ∈ Finset.Ioc lo hi, wGramFouvryCost ε C a R S M Z K j cap ((r, n), (n₂, s, h), n₂', s', h') ≤ wGramRCostEnvelope ε C a R S K j cap n s s' lo hi * (↑hi * √↑(n * s' * (s.gcd (iv3SecondaryNumerator K.1.2.1 n₂ n₂' a h).natAbs * (iv3SecondaryNumerator K.1.2.1 n₂ n₂' a h).natAbs.divisors.card)))
    Inspect dependencies

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