The joint main mean on the original occupied labels

The two differences are deduced from canonicality and the original beta support before any extension of the r fiber. Both ordered beta indices and both signed frequencies remain independent coordinates.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainJointCarrier_frequency_data (i : ℕ) (positive : Bool) (h : ℤ) : h ∈ wGramResonanceScaleFrequencies i positive → h ≠ 0 ∧ h.natAbs ≤ 2 ^ (i + 1)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainJointCarrier_scale_data {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 (ℕ × ℕ)} {L : WGramLabel} (hL : L ∈ wGramLabels (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c)) : L.1.2 ∈ wGramResonanceScaleInterval (j 2) ∧ L.2.1.1 ∈ Finset.Ioc 0 (F / K.1.1) ∧ L.2.2.1 ∈ Finset.Ioc 0 (F / K.1.1) ∧ L.2.1.2.1 ∈ wGramResonanceScaleInterval (j 4) ∧ L.2.2.2.1 ∈ wGramResonanceScaleInterval (j 4) ∧ L.2.1.2.2 ∈ wGramResonanceScaleFrequencies (j 0) positive ∧ L.2.2.2.2 ∈ wGramResonanceScaleFrequencies (j 0) positive

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainJointCarrier_data {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {F : ℕ} (hNF : ∀ n ∈ N, n ≤ F) {a : ℤ} {x η R S M Z T : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < Z) (hNT : ∀ n ∈ N, T ≤ ↑n) (hgap : x ^ η < T) {K : WExtractedKey} {b : ℕ} {j cap : Fin 5 → ℕ} {positive : Bool} {c : Finset (ℕ × ℕ)} {L : WGramLabel} (hL : L ∈ wGramMainLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c)) : mainRestrictedData K.1.2.1 a (2 ^ (j 2 + 1)) (F / K.1.1) (2 ^ (j 4 + 1)) (wGramResonanceScaleFrequencies (j 0) positive) (wGramSecondaryBase L)

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainJointMean (δ Cτ Cjoint : ℝ) (a : ℤ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) : ℝ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainJointMean δ Cτ Cjoint a K F j = ↑(2 ^ (j 3 + 1) - 1) * (√(↑(2 ^ (j 2 + 1)) * ↑(F / K.1.1) ^ 2 * ↑(2 ^ (j 4 + 1)) ^ 2 * ↑(2 ^ j 0) ^ 2 * (Cτ * ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestrictedMax a K.1.2.1 (2 ^ (j 2 + 1)) (F / K.1.1) (2 ^ (j 0 + 1)) (2 ^ (j 4 + 1))) ^ δ)) * √(↑(2 ^ (j 2 + 1)) * ↑(F / K.1.1) ^ 2 * ↑(2 ^ j 0) ^ 2 * (Cjoint * ↑(2 ^ (j 4 + 1)) ^ 2 * (1 + Real.log ↑(2 ^ (j 4 + 1))) * ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.mainRestrictedMax a K.1.2.1 (2 ^ (j 2 + 1)) (F / K.1.1) (2 ^ (j 0 + 1)) (2 ^ (j 4 + 1))) ^ δ)))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainJointMean_nonneg (δ Cτ Cjoint : ℝ) (a : ℤ) (K : WExtractedKey) (F : ℕ) (j : Fin 5 → ℕ) : 0 ≤ wGramMainJointMean δ Cτ Cjoint a K F j

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wGramMainJointCarrier_sqrt_sum {δ : ℝ} (hδ : 0 < δ) : ∃ (Cτ : ℝ) (Cjoint : ℝ), 0 < Cτ ∧ 0 < Cjoint ∧ ∀ (N : Finset ℕ) (F : ℕ) (a : ℤ) (x η R S M Z T : ℝ) (K : WExtractedKey) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)), a ≠ 0 → (∀ n ∈ N, 0 < n) → (∀ n ∈ N, n ≤ F) → 0 ≤ R → 0 ≤ S → 0 < M → 0 < Z → (∀ n ∈ N, T ≤ ↑n) → x ^ η < T → ∑ L ∈ wGramMainLabels K a (wCoprimeFiber x N S (wGramPrefix N a x η R S M Z K b j cap positive) c), √↑((wGramModulus L).gcd (wGramNumerator K a L).natAbs) ≤ wGramMainJointMean δ Cτ Cjoint a K F j

This estimate starts again at the occupied labels, not at the previously expanded iv3MainResidual. Only nonnegative r summands are extended.