Documentation

MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvryGramAggregateBound

Quantitative full-energy bound with the zero numerator separated #

The same epsilon-dependent constant works for every original cell, key, signed dyadic block, prefix and pair of arbitrary real coefficient sequences. Only occupied labels are tested for canonicality. The resonant branch pays the actual shared-k count; individual cancellation is used on the other branch.

source
noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramFouvryCost (ε C : ℝ) (a : ℤ) (R S M Z : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) (L : WGramLabel) :
ℝ
Equations
Instances For
    Inspect dependencies

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

    source
    theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramWeight_mul_re_le (K : WExtractedKey) (β ζ : ℕ → ℝ) (L : WGramLabel) (z : ℂ) :
    wGramWeight K β ζ L * z.re ≤ |wGramWeight K β ζ L| * ‖z‖

    This is the real triangle step: signs survive until this inequality.

    Inspect dependencies

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

    source
    theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSeparatedCorrelationEnergy_fouvry {ε : ℝ} (hε : 0 < ε) :
    ∃ (C : ℝ), 0 < C ∧ ∀ (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (β ζ : ℕ → ℝ), (∀ n ∈ N, 0 < n) → a ≠ 0 → 0 ≤ R → 0 ≤ S → 0 < M → 0 < Z → wSeparatedCorrelationEnergy x N S (wGramPrefix N a x η R S M Z K b j cap positive) c K β ζ a ≤ ∑ L ∈ wGramLabels (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c) with wGramNumerator K a L = 0, |wGramWeight K β ζ L| * ↑(wGramPairCount N a x η R S M Z K b j cap positive c L) + ∑ L ∈ wGramLabels (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c) with wGramNumerator K a L ≠ 0, |wGramWeight K β ζ L| * wGramFouvryCost ε C a R S M Z K j cap L

    An unconditional finite global estimate, beyond the original positivity and domain hypotheses. The two sums are over actual occupied ordered labels, not arbitrary canonical tuples. Zero numerators do not invoke Weil.

    Inspect dependencies

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