Conjugation symmetry for Chen's equation (17)

This file proves the conjugation identities for the actual primitive-character family and the actual finite polynomials occurring in equation (17). It then uses those identities to replace the full vertical-line norm integrals by twice the half-line integrals already used in Chen1973Lemma6Equations16And17.

def AnalyticNumberTheory.LargeSieve.primitiveCharacterConjEquiv (q : ℕ) [NeZero q] : PrimitiveCharacter q ≃ PrimitiveCharacter q

Conjugation is an involutive equivalence of primitive characters of a fixed nonzero modulus.

Equations

• AnalyticNumberTheory.LargeSieve.primitiveCharacterConjEquiv q = { toFun := fun (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) => ⟨star ↑χ, ⋯⟩, invFun := fun (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q) => ⟨star ↑χ, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacterConjEquiv_val (q : ℕ) [NeZero q] (χ : PrimitiveCharacter q) : ↑((primitiveCharacterConjEquiv q) χ) = star ↑χ

@[simp]

theorem AnalyticNumberTheory.LargeSieve.primitiveCharacterConjEquiv_apply_apply (q : ℕ) [NeZero q] (χ : PrimitiveCharacter q) : (primitiveCharacterConjEquiv q) ((primitiveCharacterConjEquiv q) χ) = χ

theorem AnalyticNumberTheory.LargeSieve.conj_sum_range_cpowWeight_character {q : ℕ} [NeZero q] (χ : PrimitiveCharacter q) (s : ℂ) (N : ℕ) : (starRingEnd ℂ) (∑ n ∈ Finset.range N, DirichletLAbelWeightVariation.cpowWeight s ↑n * ↑χ ↑n) = ∑ n ∈ Finset.range N, DirichletLAbelWeightVariation.cpowWeight ((starRingEnd ℂ) s) ↑n * ↑((primitiveCharacterConjEquiv q) χ) ↑n

General (not merely quadratic) conjugation of a natural-order partial Dirichlet sum.

theorem AnalyticNumberTheory.LargeSieve.primitiveLFunction_conj {q : ℕ} [NeZero q] (χ : PrimitiveCharacter q) (hχ : ↑χ ≠ 1) (s : ℂ) (hs : 0 < s.re) : DirichletCharacter.LFunction (↑((primitiveCharacterConjEquiv q) χ)) ((starRingEnd ℂ) s) = (starRingEnd ℂ) (DirichletCharacter.LFunction (↑χ) s)

Conjugation identity for a primitive Dirichlet L-function on the whole conditional-convergence half-plane.

theorem AnalyticNumberTheory.LargeSieve.primitiveLDeriv_conj {q : ℕ} [NeZero q] (χ : PrimitiveCharacter q) (hχ : ↑χ ≠ 1) (s : ℂ) (hs : 0 < s.re) : deriv (DirichletCharacter.LFunction ↑((primitiveCharacterConjEquiv q) χ)) ((starRingEnd ℂ) s) = (starRingEnd ℂ) (deriv (DirichletCharacter.LFunction ↑χ) s)

The derivative of a primitive L-function obeys the same conjugation law. The proof differentiates the locally equal holomorphic functions L(s,star χ) and conj (L(conj s,χ)).

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6MobiusPartialSum_conj {q : ℕ} [NeZero q] (H : ℕ) (s : ℂ) (χ : PrimitiveCharacter q) : chen1973Lemma6MobiusPartialSum H ((starRingEnd ℂ) s) ((primitiveCharacterConjEquiv q) χ) = (starRingEnd ℂ) (chen1973Lemma6MobiusPartialSum H s χ)

Conjugation identity for Chen's natural-order S(H,s,χ).

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17PairPolynomial (x B k m : ℕ) {q : ℕ} (s : ℂ) (χ : PrimitiveCharacter q) : ℂ

The exact pair polynomial in equation (17), made public for the symmetry and subsequent moment arguments.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17PairPolynomial x B k m s χ = ∑ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell x B k m, ↑χ ↑(pp.1 * pp.2) / ((↑pp.1 * ↑pp.2) ^ s * ↑(Real.log (↑x / (↑pp.1 * ↑pp.2))))

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17PairPolynomial_conj {q : ℕ} [NeZero q] (x B k m : ℕ) (s : ℂ) (χ : PrimitiveCharacter q) : chen1973Lemma6Eq17PairPolynomial x B k m ((starRingEnd ℂ) s) ((primitiveCharacterConjEquiv q) χ) = (starRingEnd ℂ) (chen1973Lemma6Eq17PairPolynomial x B k m s χ)

Exact conjugation identity for the pair polynomial.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue_conj {q : ℕ} (s : ℂ) (χ : PrimitiveCharacter q) (hs : 0 < s.re) : chen1973Lemma6PrimitiveLValue q ((starRingEnd ℂ) s) (if hq : 1 < q then (primitiveCharacterConjEquiv q) χ else χ) = (starRingEnd ℂ) (chen1973Lemma6PrimitiveLValue q s χ)

The totalized primitive L value commutes with character and parameter conjugation.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6OneSubLS_conj {q : ℕ} [NeZero q] (H : ℕ) (s : ℂ) (χ : PrimitiveCharacter q) (hχ : ↑χ ≠ 1) (hs : 0 < s.re) : chen1973Lemma6OneSubLS H ((starRingEnd ℂ) s) ((primitiveCharacterConjEquiv q) χ) = (starRingEnd ℂ) (chen1973Lemma6OneSubLS H s χ)

Exact conjugation identity for 1-LS on the positive half-plane.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6LDerivMulS_conj {q : ℕ} [NeZero q] (H : ℕ) (s : ℂ) (χ : PrimitiveCharacter q) (hχ : ↑χ ≠ 1) (hs : 0 < s.re) : deriv (DirichletCharacter.LFunction ↑((primitiveCharacterConjEquiv q) χ)) ((starRingEnd ℂ) s) * chen1973Lemma6MobiusPartialSum H ((starRingEnd ℂ) s) ((primitiveCharacterConjEquiv q) χ) = (starRingEnd ℂ) (deriv (DirichletCharacter.LFunction ↑χ) s * chen1973Lemma6MobiusPartialSum H s χ)

Exact conjugation identity for L' S.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue_conj_of_one_lt {q : ℕ} [NeZero q] (hq : 1 < q) (s : ℂ) (χ : PrimitiveCharacter q) (hχ : ↑χ ≠ 1) (hs : 0 < s.re) : chen1973Lemma6PrimitiveLValue q ((starRingEnd ℂ) s) ((primitiveCharacterConjEquiv q) χ) = (starRingEnd ℂ) (chen1973Lemma6PrimitiveLValue q s χ)

The exact totalized L object used in equation (17) has the expected conjugation identity on the actual conductor range.

theorem AnalyticNumberTheory.LargeSieve.chen1973PrimitiveLDeriv_conj_of_one_lt {q : ℕ} [NeZero q] (hq : 1 < q) (s : ℂ) (χ : PrimitiveCharacter q) (hχ : ↑χ ≠ 1) (hs : 0 < s.re) : chen1973PrimitiveLDeriv q ((starRingEnd ℂ) s) ((primitiveCharacterConjEquiv q) χ) = (starRingEnd ℂ) (chen1973PrimitiveLDeriv q s χ)

The exact totalized L' object used in equation (17) has the expected conjugation identity on the actual conductor range.

theorem AnalyticNumberTheory.LargeSieve.conj_verticalLine (a v : ℝ) : (starRingEnd ℂ) (↑a + ↑v * Complex.I) = ↑a + ↑(-v) * Complex.I

Conjugating the point a+iv on a real vertical line reflects v.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17Kernel_reflection (x : ℕ) (a v : ℝ) : chen1973Lemma6Eq17Kernel x (↑a + -↑v * Complex.I) = chen1973Lemma6Eq17Kernel x (↑a + ↑v * Complex.I)

Chen's real denominator kernel is invariant under reflection of a vertical line.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6A_reflection {x L level B k m H : ℕ} (hlevel : 1 ≤ level) (a v : ℝ) (ha : 0 < a) : chen1973Lemma6A x L level B k m H (↑a + -↑v * Complex.I) = chen1973Lemma6A x L level B k m H (↑a + ↑v * Complex.I)

The first equation-(17) numerator is even on every positive real vertical line. Positive-level conductor blocks contain only nonprincipal primitive characters, so the general conjugation equivalence applies to every summand.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6B_reflection {x L level B k m H : ℕ} (hlevel : 1 ≤ level) (a v : ℝ) (ha : 0 < a) : chen1973Lemma6B x L level B k m H (↑a + -↑v * Complex.I) = chen1973Lemma6B x L level B k m H (↑a + ↑v * Complex.I)

The second equation-(17) numerator is even on every positive real vertical line.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17FirstIntegrand_even {x L level B k m H : ℕ} (hlevel : 1 ≤ level) (hx : 1 < x) (v : ℝ) : chen1973Lemma6A x L level B k m H (↑(chen1973Lemma6Alpha x) + -↑v * Complex.I) / chen1973Lemma6Eq17Kernel x (↑(chen1973Lemma6Alpha x) + -↑v * Complex.I) = chen1973Lemma6A x L level B k m H (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I) / chen1973Lemma6Eq17Kernel x (↑(chen1973Lemma6Alpha x) + ↑v * Complex.I)

The actual first norm integrand in (17) is even.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17SecondIntegrand_even {x L level B k m H : ℕ} (hlevel : 1 ≤ level) (hx : 1 < x) (v : ℝ) : chen1973Lemma6B x L level B k m H (↑(chen1973Lemma6Beta x) + -↑v * Complex.I) / chen1973Lemma6Eq17Kernel x (↑(chen1973Lemma6Beta x) + -↑v * Complex.I) = chen1973Lemma6B x L level B k m H (↑(chen1973Lemma6Beta x) + ↑v * Complex.I) / chen1973Lemma6Eq17Kernel x (↑(chen1973Lemma6Beta x) + ↑v * Complex.I)

The actual second norm integrand in (17) is even.

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17FirstFullIntegral (x L level B k m H : ℕ) : ℝ

Full-line version of the first actual equation-(17) integral.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17FirstFullIntegral x L level B k m H = ∫ (v : ℝ), AnalyticNumberTheory.LargeSieve.chen1973Lemma6A x L level B k m H (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑v * Complex.I) / AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17Kernel x (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Alpha x) + ↑v * Complex.I)

noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17SecondFullIntegral (x L level B k m H : ℕ) : ℝ

Full-line version of the second actual equation-(17) integral.

Equations

• AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17SecondFullIntegral x L level B k m H = ∫ (v : ℝ), AnalyticNumberTheory.LargeSieve.chen1973Lemma6B x L level B k m H (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x) + ↑v * Complex.I) / AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17Kernel x (↑(AnalyticNumberTheory.LargeSieve.chen1973Lemma6Beta x) + ↑v * Complex.I)

theorem AnalyticNumberTheory.LargeSieve.integral_eq_two_mul_Ioi_of_even (f : ℝ → ℝ) (heven : ∀ (v : ℝ), f (-v) = f v) : ∫ (v : ℝ), f v = 2 * ∫ (v : ℝ) in Set.Ioi 0, f v

The integral of an even real function is twice its positive-half-line integral.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17FirstFullIntegral_eq_two_mul_half {x L level B k m H : ℕ} (hlevel : 1 ≤ level) (hx : 1 < x) : chen1973Lemma6Eq17FirstFullIntegral x L level B k m H = 2 * chen1973Lemma6Eq17FirstIntegral x L level B k m H

The full alpha-line norm integral is exactly twice Chen's half-line integral.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq17SecondFullIntegral_eq_two_mul_half {x L level B k m H : ℕ} (hlevel : 1 ≤ level) (hx : 1 < x) : chen1973Lemma6Eq17SecondFullIntegral x L level B k m H = 2 * chen1973Lemma6Eq17SecondIntegral x L level B k m H

The full beta-line norm integral is exactly twice Chen's half-line integral.