Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvryKSectionCancellation

Individual cancellation on a real IV.3 paired section #

Both floor cutoffs and all original filters are retained. Small-root freezing and the exact sieve reduction connect this carrier to the proved reciprocal interval theorem, with only tau(|a|) as sieve cost.

source
noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionPairResidueSum (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (r n₁ n₂ n₂' s s' : ℕ) (h h' : ℤ) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (v : ℕ) :
ℂ
Equations
Instances For
    Inspect dependencies

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

    source
    noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionPairSum (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (r n₁ n₂ n₂' s s' : ℕ) (h h' : ℤ) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) :
    ℂ
    Equations
    Instances For
      Inspect dependencies

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

      source
      theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionPairSum_eq_residues (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (r n₁ n₂ n₂' s s' : ℕ) (h h' : ℤ) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (hD : 0 < K.D') :
      wKSectionPairSum N a x η R S M Z K r n₁ n₂ n₂' s s' h h' b j cap positive c = ∑ v ∈ Finset.range K.D', wKSectionPairResidueSum N a x η R S M Z K r n₁ n₂ n₂' s s' h h' b j cap positive c v
      Inspect dependencies

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

      source
      theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionPairResidueSum_norm_eq {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} {x η R S M Z : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < Z) {K : WExtractedKey} {r n₁ n₂ n₂' s s' : ℕ} {h h' : ℤ} {b k₀ : ℕ} [NeZero (n₁ * r * s * s')] (hf : wKSectionFixedCanonical K r n₁ n₂ s) (hf' : wKSectionFixedCanonical K r n₁ n₂' s') (hΔ : 0 < K.2) (hΔ' : 0 < wKSectionDeltaPrime K) (he : K.2 * wKSectionDeltaPrime K = K.1.2.2.1 * K.1.2.2.2.2) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (hk₀ : k₀ ∈ wKSectionCarrier N a x η R S M Z K r n₁ n₂ s h b j cap positive c ∩ wKSectionCarrier N a x η R S M Z K r n₁ n₂' s' h' b j cap positive c) :
      ‖wKSectionPairResidueSum N a x η R S M Z K r n₁ n₂ n₂' s s' h h' b j cap positive c k₀‖ = ‖sievedReciprocalInterval (n₁ * r * s * s') (iv3CorrelationNumerator K.1.2.1 n₁ n₂ n₂' s s' a h h' * wPhaseInverse (K.D' * n₂ * n₂') (n₁ * r * s * s')) k₀ K.D' a.natAbs (max (wKSectionGridLower M Z K r s h j) (wKSectionGridLower M Z K r s' h' j)) (wKSectionGridUpper R S K j cap)‖
      Inspect dependencies

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

      source
      theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionPairResidueSum_fouvry {ε : ℝ} (hε : 0 < ε) :
      ∃ (C : ℝ), 0 < C ∧ ∀ (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (r n₁ n₂ n₂' s s' : ℕ) (h h' : ℤ) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (v : ℕ), (∀ n ∈ N, 0 < n) → a ≠ 0 → 0 ≤ R → 0 ≤ S → 0 < M → 0 < Z → wKSectionFixedCanonical K r n₁ n₂ s → wKSectionFixedCanonical K r n₁ n₂' s' → 0 < K.2 → 0 < wKSectionDeltaPrime K → K.2 * wKSectionDeltaPrime K = K.1.2.2.1 * K.1.2.2.2.2 → ‖wKSectionPairResidueSum N a x η R S M Z K r n₁ n₂ n₂' s s' h h' b j cap positive c v‖ ≤ C * ↑a.natAbs.divisors.card * (1 + ↑(wKSectionGridUpper R S K j cap - max (wKSectionGridLower M Z K r s h j) (wKSectionGridLower M Z K r s' h' j) + 1) / (↑K.D' * ↑(n₁ * r * s * s'))) * √↑((n₁ * r * s * s').gcd (iv3CorrelationNumerator K.1.2.1 n₁ n₂ n₂' s s' a h h').natAbs) * ↑(n₁ * r * s * s') ^ (1 / 2 + ε)

      Uniform individual cancellation on every residue section of the actual paired carrier, including empty sections. The common inverse and the admissible progression step are proved from a member, not assumed.

      Inspect dependencies

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

      source
      theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionPairSum_fouvry {ε : ℝ} (hε : 0 < ε) :
      ∃ (C : ℝ), 0 < C ∧ ∀ (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (r n₁ n₂ n₂' s s' : ℕ) (h h' : ℤ) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)), (∀ n ∈ N, 0 < n) → a ≠ 0 → 0 ≤ R → 0 ≤ S → 0 < M → 0 < Z → wKSectionFixedCanonical K r n₁ n₂ s → wKSectionFixedCanonical K r n₁ n₂' s' → 0 < K.2 → 0 < wKSectionDeltaPrime K → K.2 * wKSectionDeltaPrime K = K.1.2.2.1 * K.1.2.2.2.2 → ‖wKSectionPairSum N a x η R S M Z K r n₁ n₂ n₂' s s' h h' b j cap positive c‖ ≤ C * ↑a.natAbs.divisors.card * (↑K.D' + ↑(wKSectionGridUpper R S K j cap - max (wKSectionGridLower M Z K r s h j) (wKSectionGridLower M Z K r s' h' j) + 1) / ↑(n₁ * r * s * s')) * √↑((n₁ * r * s * s').gcd (iv3CorrelationNumerator K.1.2.1 n₁ n₂ n₂' s s' a h h').natAbs) * ↑(n₁ * r * s * s') ^ (1 / 2 + ε)

      The cost of freezing all small-root residues is explicit. After summing them, it is D' + span/q, not a loss of the interval saving.

      Inspect dependencies

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