Quantitatively eliminating the occupied-base sum

The two power envelopes use only local dyadic highs and the original beta upper support divided by d. Monotonicity is valid for every nonnegative exponent, including empty carriers and degenerate arbitrary keys.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleProductMax (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleProductMax K F j = 2 ^ (j 0 + 1) * (F / K.1.1) * 2 ^ (j 4 + 1)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleDivisorMax (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleDivisorMax K F j = K.1.2.1 * 2 ^ (j 2 + 1) + MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleProductMax K F j

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleEnvelope (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) (ε : ℝ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleEnvelope K F j ε = ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleProductMax K F j) ^ (2 * ε) * ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleDivisorMax K F j) ^ ε

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleEnvelope_nonneg (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) (ε : ℝ) : 0 ≤ wGramResonanceScaleEnvelope K F j ε

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScaleBox_bounds {K : WExtractedKey} {F : ℕ} {j : Fin 5 → ℕ} {positive : Bool} {v : WGramResonanceBase} (hv : v ∈ wGramResonanceScaleBox K F j positive) : (wGramResonanceProduct v).natAbs ≤ wGramResonanceScaleProductMax K F j ∧ K.1.2.1 * v.1.2 + (wGramResonanceProduct v).natAbs ≤ wGramResonanceScaleDivisorMax K F j

Both power bases are bounded before taking any real powers.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceScale_le_envelope {K : WExtractedKey} {F : ℕ} {j : Fin 5 → ℕ} {positive : Bool} {v : WGramResonanceBase} (hv : v ∈ wGramResonanceScaleBox K F j positive) {ε : ℝ} (hε : 0 ≤ ε) : wGramResonanceScale K ε v ≤ wGramResonanceScaleEnvelope K F j ε

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wGramResonanceScale_le_box {K : WExtractedKey} {F : ℕ} {j : Fin 5 → ℕ} {positive : Bool} {G : Finset WGramResonanceBase} (hG : G ⊆ wGramResonanceScaleBox K F j positive) {ε : ℝ} (hε : 0 ≤ ε) : ∑ v ∈ G, wGramResonanceScale K ε v ≤ ↑(wGramResonanceScaleBoxCard K F j) * wGramResonanceScaleEnvelope K F j ε

A proved cardinal-times-envelope estimate, not a hypothesis on the sum.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramResonanceBases_sum_le_scaleBox {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {F : ℕ} (hNF : ∀ n ∈ N, n ≤ F) {a : ℤ} {x η R S M Z : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < Z) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) {ε : ℝ} (hε : 0 ≤ ε) : ∑ v ∈ wGramResonanceBases (wGramZeroLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c)), wGramResonanceScale K ε v ≤ ↑(wGramResonanceScaleBoxCard K F j) * wGramResonanceScaleEnvelope K F j ε

The actual local prefix supplies every box condition, including the independent n₂' ≤ F/d; no positivity of an unoccupied key is required.