noncomputable def AnalyticNumberTheory.LargeSieve.primitiveWeightedFourthMoment (Q : ℕ) (s : ℂ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.primitiveWeightedFourthMoment Q s = ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLValue q s χ‖ ^ 4

theorem AnalyticNumberTheory.LargeSieve.primitive_card_le_totient (q : ℕ) (hq : 0 < q) : Fintype.card (PrimitiveCharacter q) ≤ q.totient

theorem AnalyticNumberTheory.LargeSieve.weighted_polynomial_fourth_le (h2 : Chen1973Lemma2EquationTwo) (N Q : ℕ) (s : ℂ) (hs : Chen1973Lemma3Domain s s.re s.im) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖chen1973PrimitivePolynomialValue q N s χ‖ ^ 4 ≤ 2 * ((↑Q ^ 2 + Real.pi * ↑(N * N)) * MathlibNt.SieveTheory.LiuWeight.liuHarmonic (N * N) ^ 4)

theorem AnalyticNumberTheory.LargeSieve.weighted_truncation_error_scalar {Q : ℕ} {s : ℂ} (hQ : 2 ≤ Q) (hs : Chen1973Lemma3Domain s s.re s.im) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖chen1973PrimitiveLValue q s χ - chen1973PrimitivePolynomialValue q (chen1973Lemma3Cutoff Q s) s χ‖ ^ 4 ≤ 2560000 * ↑Q ^ 2 * ‖s‖ ^ 2 * chen1973Lemma3LogScale Q s ^ 4

theorem AnalyticNumberTheory.LargeSieve.weighted_fourth_finite_assembly (h2 : Chen1973Lemma2EquationTwo) (N Q : ℕ) (s : ℂ) (hs : Chen1973Lemma3Domain s s.re s.im) : primitiveWeightedFourthMoment Q s ≤ 16 * ((↑Q ^ 2 + Real.pi * ↑(N * N)) * MathlibNt.SieveTheory.LiuWeight.liuHarmonic (N * N) ^ 4) + 8 * ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖chen1973PrimitiveLValue q s χ - chen1973PrimitivePolynomialValue q N s χ‖ ^ 4

theorem AnalyticNumberTheory.LargeSieve.primitiveWeightedFourthMoment_corrected_endpoint (h2 : Chen1973Lemma2EquationTwo) {Q : ℕ} (s : ℂ) (hQ : 2 ≤ Q) (hs : Chen1973Lemma3Domain s s.re s.im) : primitiveWeightedFourthMoment Q s ≤ 21000000 * ↑Q ^ 2 * ‖s‖ ^ 2 * Real.log (↑Q * (1 + ‖s‖)) ^ 4