Subconvexity bounds for Dirichlet L-functions

DefinitionCentral-value exponents on a set of levels#✓fully proved

Let \(S\) be a set of natural numbers and \(\theta\) a real number. Then \(\theta\) is a central-value exponent on \(S\) if \(\theta \ge 0\) and for every \(\varepsilon > 0\) there are a real number \(C > 0\) and a natural number \(Q\) such that for every positive \(q \in S\) with \(q \ge Q\) and every primitive Dirichlet character \(\chi\) modulo \(q\), the analytically continued Dirichlet \(L\)-function satisfies \(|L(1/2, \chi)| \le C q^{\theta + \varepsilon}\).

The constants \(C\) and \(Q\) may depend on \(\varepsilon\), but not on the level or the character.

def IsCentralValueExponentOn (levels : Set ℕ) (θ : ℝ) : Prop :=
  0 ≤ θ ∧
    ∀ ε : ℝ, 0 < ε →
      ∃ C : ℝ, 0 < C ∧ ∃ Q : ℕ, ∀ q : ℕ, Q ≤ q → ∀ hq : 0 < q, q ∈ levels →
        letI : NeZero q := ⟨hq.ne'⟩
        ∀ χ : DirichletCharacter ℂ q, χ.IsPrimitive →
          ‖χ.LFunction (1 / 2 : ℂ)‖ ≤ C * Real.rpow (q : ℝ) (θ + ε)

Used by 2

Used byAdmissible exponents for Dirichlet central values · Petrow–Young Weyl bound for central values

DefinitionAdmissible exponents for Dirichlet central values#✓fully proved

A real number \(\theta\) is an admissible conductor-aspect exponent for primitive Dirichlet characters if it is a central-value exponent on the set of all natural numbers: \(\theta \ge 0\), and for every \(\varepsilon > 0\) there are a real number \(C > 0\) and a natural number \(Q\) such that for every positive integer \(q \ge Q\) and every primitive Dirichlet character \(\chi\) modulo \(q\), the analytically continued Dirichlet \(L\)-function satisfies \(|L(1/2, \chi)| \le C q^{\theta + \varepsilon}\).

def IsDirichletSubconvexityExponent (θ : ℝ) : Prop :=
  IsCentralValueExponentOn Set.univ θ

Uses 1 · Used by 4

Statement usesCentral-value exponents on a set of levels

Used byBurgess's bound for Dirichlet central values · The conductor-aspect Dirichlet subconvexity exponent · Admissible exponents bound the Dirichlet subconvexity exponent · The Dirichlet subconvexity exponent is nonnegative

DefinitionThe conductor-aspect Dirichlet subconvexity exponent#✓fully proved

The infimum, taken in the extended real numbers, of the set of all real \(\theta\) that are admissible conductor-aspect exponents for primitive Dirichlet characters. If no real number is admissible, this infimum is \(+\infty\).

noncomputable def dirichletSubconvexityExponent : EReal :=
  sInf ((fun θ : ℝ => (θ : EReal)) '' {θ | IsDirichletSubconvexityExponent θ})

Uses 1 · Used by 3

Statement usesAdmissible exponents for Dirichlet central values

Used byAdmissible exponents bound the Dirichlet subconvexity exponent · The Dirichlet subconvexity exponent is at most 3/16 · The Dirichlet subconvexity exponent is nonnegative

TheoremThe Dirichlet subconvexity exponent is nonnegative#✓fully proved

The conductor-aspect Dirichlet subconvexity exponent, an extended real number, is at least \(0\). This holds by construction: every admissible exponent is nonnegative, and if no real exponent is admissible, the exponent is the infimum of the empty set, which is \(+\infty\).

theorem dirichletSubconvexityExponent_nonneg :
    (0 : EReal) ≤ dirichletSubconvexityExponent

Uses 2

Statement usesThe conductor-aspect Dirichlet subconvexity exponent

Proof usesAdmissible exponents for Dirichlet central values

TheoremAdmissible exponents bound the Dirichlet subconvexity exponent#✓fully proved

If a real number \(\theta\) is an admissible conductor-aspect exponent for primitive Dirichlet characters, then the conductor-aspect Dirichlet subconvexity exponent is at most \(\theta\), as extended real numbers.

theorem dirichletSubconvexityExponent_le_of_admissible {θ : ℝ}
    (hθ : IsDirichletSubconvexityExponent θ) :
    dirichletSubconvexityExponent ≤ (θ : EReal)

Uses 2

Statement usesAdmissible exponents for Dirichlet central values · The conductor-aspect Dirichlet subconvexity exponent

TheoremBurgess's bound for Dirichlet central values#●ready to prove

The number \(3/16\) is an admissible conductor-aspect exponent for primitive Dirichlet characters: for every \(\varepsilon > 0\) there are a real number \(C > 0\) and a natural number \(Q\) such that for every positive integer \(q \ge Q\) and every primitive Dirichlet character \(\chi\) modulo \(q\), the analytically continued Dirichlet \(L\)-function satisfies \(|L(1/2, \chi)| \le C q^{3/16 + \varepsilon}\).

public theorem_wanted burgessThreeSixteenths_admissible :
    IsDirichletSubconvexityExponent ((3 : ℝ) / 16)

Sources

• Petrow and Young, The Weyl bound for Dirichlet L-functions of cube-free conductor, Annals of Mathematics 192 (2020), introduction equation (1.2), quoting Burgess's 1963 theorem.

Uses 1

Statement usesAdmissible exponents for Dirichlet central values

TheoremThe Dirichlet subconvexity exponent is at most 3/16#●ready to prove

The conductor-aspect Dirichlet subconvexity exponent, an extended real number, is at most \(3/16\).

public theorem_wanted dirichletSubconvexityExponent_le_threeSixteenths :
    dirichletSubconvexityExponent ≤ (((3 : ℝ) / 16 : ℝ) : EReal)

Sources

• teorth/optimizationproblems, constant 62b, citing Burgess (1963) through Petrow--Young (2020).

Uses 1

Statement usesThe conductor-aspect Dirichlet subconvexity exponent

TheoremPetrow–Young Weyl bound for central values#●ready to prove

The number \(1/6\) is a central-value exponent on the set of cube-free levels, the natural numbers \(q > 0\) such that \(p^3\) does not divide \(q\) for any prime \(p\): for every \(\varepsilon > 0\) there are a real number \(C > 0\) and a natural number \(Q\) such that for every cube-free \(q \ge Q\) and every primitive Dirichlet character \(\chi\) modulo \(q\), the analytically continued Dirichlet \(L\)-function satisfies \(|L(1/2, \chi)| \le C q^{1/6 + \varepsilon}\).

public theorem_wanted petrowYoungCubeFreeOneSixth_admissible :
    IsCentralValueExponentOn {q | q.IsPowerFree 3} ((1 : ℝ) / 6)

Sources

• Petrow and Young, The Weyl bound for Dirichlet L-functions of cube-free conductor, Annals of Mathematics 192 (2020), abstract and introduction.

Uses 2

Statement usesCentral-value exponents on a set of levels · Power-free natural numbers

TheoremPetrow–Young Weyl bound on the critical line#●ready to prove

For every real \(\varepsilon > 0\) there is a real number \(C\) such that for every cube-free natural number \(q\) (that is, \(q > 0\) and \(p^3\) does not divide \(q\) for any prime \(p\)), every primitive Dirichlet character \(\chi\) modulo \(q\) and every real \(t\), the analytically continued Dirichlet \(L\)-function satisfies

\[|L(1/2 + it, \chi)| \le C \, q^{1/6 + \varepsilon} (1 + |t|)^{1/6 + \varepsilon}.\]

This is Corollary 1.3 of the source.

public theorem_wanted corollary_1_3 (ε : ℝ) (hε : 0 < ε) : ∃ C : ℝ,
    ∀ q (_hq : q.IsPowerFree 3) [NeZero q] (χ : DirichletCharacter ℂ q) (_hχ : χ.IsPrimitive) (t : ℝ),
      ‖χ.LFunction (1 / 2 + I * t)‖ ≤ C * q ^ (1 / 6 + ε) * (1 + |t|) ^ (1 / 6 + ε)

Sources

• I. Petrow and M. P. Young, The Weyl bound for Dirichlet L-functions of cube-free conductor, Annals of Math, 192 (2) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_dirichlet_weyl_bound of the lean-eval benchmark.

Uses 1

Statement usesPower-free natural numbers

5 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.