Global occupied-section estimate for the separated Gram energy

The exact identity precedes the real triangle inequality. In particular no absolute values are inserted into the original signed beta/zeta weights. The zero-numerator branch uses the actual paired-carrier count, not Weil.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramWeight (K : WExtractedKey) (β ζ : ℕ → ℝ) (L : WGramLabel) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramWeight K β ζ L = ζ (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionDeltaPrime K * L.2.1.2.1) * β (K.1.1 * L.2.1.1) * (ζ (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionDeltaPrime K * L.2.2.2.1) * β (K.1.1 * L.2.2.1))

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramModulus (L : WGramLabel) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramModulus L = L.1.2 * L.1.1 * L.2.1.2.1 * L.2.2.2.1

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramNumerator (K : WExtractedKey) (a : ℤ) (L : WGramLabel) : ℤ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramNumerator K a L = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3CorrelationNumerator K.1.2.1 L.1.2 L.2.1.1 L.2.2.1 L.2.1.2.1 L.2.2.2.1 a L.2.1.2.2 L.2.2.2.2

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSpan (R S M Z : ℝ) (K : WExtractedKey) (j cap : Fin 5 → ℕ) (L : WGramLabel) : ℕ

Both paid floor cutoffs enter through the maximum of the two lower endpoints, with their respective local scales unchanged.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramSpan R S M Z K j cap L = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionGridUpper R S K j cap - max (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionGridLower M Z K L.1.1 L.2.1.2.1 L.2.1.2.2 j) (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionGridLower M Z K L.1.1 L.2.2.2.1 L.2.2.2.2 j) + 1

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramPairSum (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (L : WGramLabel) : ℂ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramPairSum N a x η R S M Z K b j cap positive c L = MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionPairSum N a x η R S M Z K L.1.1 L.1.2 L.2.1.1 L.2.2.1 L.2.1.2.1 L.2.2.2.1 L.2.1.2.2 L.2.2.2.2 b j cap positive c

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramPairCount (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (L : WGramLabel) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramPairCount N a x η R S M Z K b j cap positive c L = (MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionCarrier N a x η R S M Z K L.1.1 L.1.2 L.2.1.1 L.2.1.2.1 L.2.1.2.2 b j cap positive c ∩ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionCarrier N a x η R S M Z K L.1.1 L.1.2 L.2.2.1 L.2.2.2.1 L.2.2.2.2 b j cap positive c).card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramPairSum_norm_le_count (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (L : WGramLabel) : ‖wGramPairSum N a x η R S M Z K b j cap positive c L‖ ≤ ↑(wGramPairCount N a x η R S M Z K b j cap positive c L)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramPairCount_le_interval (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (L : WGramLabel) : wGramPairCount N a x η R S M Z K b j cap positive c L ≤ (Finset.Icc (max (wKSectionGridLower M Z K L.1.1 L.2.1.2.1 L.2.1.2.2 j) (wKSectionGridLower M Z K L.1.1 L.2.2.2.1 L.2.2.2.2 j)) (wKSectionGridUpper R S K j cap)).card

The zero-branch count is bounded by the cardinal of the actual intersection interval, which is zero if the upper endpoint is too small.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wSeparatedCorrelationEnergy_eq_gram {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 : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (β ζ : ℕ → ℝ) : 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), wGramWeight K β ζ L * (wGramPairSum N a x η R S M Z K b j cap positive c L).re

Exact global reindexing of the previously defined energy. Eligibility is proved only for occupied labels; no canonicality premise is imposed on arbitrary labels, and the empty-carrier case is automatic.