Uniform local-scale count and coefficient payment on occupied zero labels

For a base v, put P=h*n₂'*s', A=|P|, and B=d₁*n₁+|P|. One constant depending only on epsilon bounds every actual fiber by C*A^(2*epsilon)*B^epsilon. Coefficients are bounded only on their original supports; no envelope on the enlarged divisor carrier is assumed.

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScale (K : WExtractedKey) (ε : ℝ) (v : WGramResonanceBase) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScale K ε v = ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceProduct v).natAbs ^ (2 * ε) * ↑(K.1.2.1 * v.1.2 + (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceProduct v).natAbs) ^ ε

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceFiber_card_le_local_scales {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (N : Finset ℕ) (a : ℤ) (x η R S M Z T : ℝ) (K : WExtractedKey) (b : ℕ) (V : Finset (WExtractedTuple × ℤ)), (∀ n ∈ N, 0 < n) → a ≠ 0 → 0 ≤ R → 0 ≤ S → 0 < M → 0 < Z → (∀ n ∈ N, T ≤ ↑n) → x ^ η < T → V ⊆ wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K → ∀ v ∈ wGramResonanceBases (wGramZeroLabels K a V), ↑(wGramResonanceFiber (wGramZeroLabels K a V) v).card ≤ C * wGramResonanceScale K ε v

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramWeight_abs_le_of_support {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} {b : ℕ} {V : Finset (WExtractedTuple × ℤ)} (hV : V ⊆ wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) (β ζ : ℕ → ℝ) {Bβ Bζ : ℝ} (hBβ : 0 ≤ Bβ) (hBζ : 0 ≤ Bζ) (hβ : ∀ n ∈ N, |β n| ≤ Bβ) (hζ : ∀ s ∈ Finset.Ioc 0 ⌊S⌋₊, |ζ s| ≤ Bζ) {L : WGramLabel} (hL : L ∈ wGramLabels V) : |wGramWeight K β ζ L| ≤ (Bβ * Bζ) ^ 2

The coefficient envelope is used only at the original beta indices in N and original zeta indices in (0,floor S], derived from occupied witnesses.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramZeroLabels_sum_le_local_scales {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (N : Finset ℕ) (a : ℤ) (x η R S M Z T : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (V : Finset (WExtractedTuple × ℤ)) (β ζ : ℕ → ℝ) (Bβ Bζ : ℝ), (∀ n ∈ N, 0 < n) → a ≠ 0 → 0 ≤ R → 0 ≤ S → 0 < M → 0 < Z → (∀ n ∈ N, T ≤ ↑n) → x ^ η < T → V ⊆ wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K → 0 ≤ Bβ → 0 ≤ Bζ → (∀ n ∈ N, |β n| ≤ Bβ) → (∀ s ∈ Finset.Ioc 0 ⌊S⌋₊, |ζ s| ≤ Bζ) → ∑ L ∈ wGramZeroLabels K a V, |wGramWeight K β ζ L| * ↑(wGramPairCount N a x η R S M Z K b j cap positive c L) ≤ (Bβ * Bζ) ^ 2 * ↑(2 ^ j 1) * C * ∑ v ∈ wGramResonanceBases (wGramZeroLabels K a V), wGramResonanceScale K ε v

Quantitative whole-zero-mass bound, with one epsilon constant before every support, key, prefix, cell and coefficient sequence is chosen.