Documentation

MathlibNt.AnalyticNumberTheory.Chen1973.Chen1973Lemma3WeightedFourthMoment

source
noncomputable def AnalyticNumberTheory.LargeSieve.primitiveWeightedFourthMoment (Q : ℕ) (s : ℂ) :
ℝ
Equations
Instances For
    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.primitiveWeightedFourthMoment · compiled type and proof/definition references.

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

    AnalyticNumberTheory.LargeSieve.primitive_card_le_totient · compiled type and proof/definition references.

    source
    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)
    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.weighted_polynomial_fourth_le · compiled type and proof/definition references.

    source
    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
    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.weighted_truncation_error_scalar · compiled type and proof/definition references.

    source
    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
    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.weighted_fourth_finite_assembly · compiled type and proof/definition references.

    source
    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
    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.primitiveWeightedFourthMoment_corrected_endpoint · compiled type and proof/definition references.