Multiplicative functions in short intervals

DefinitionExtension of an arithmetic function to the integers#✓fully proved

Let \(R\) be a type with a zero element \(0\) and let \(f\) be an arithmetic function with values in \(R\). The extension of \(f\) to the integers is the function on \(\mathbb{Z}\) that sends an integer \(z\) to \(f(z)\) if \(z > 0\) and to \(0\) if \(z \le 0\).

noncomputable def _root_.ArithmeticFunction.intExtension {R : Type*} [Zero R]
    (f : ArithmeticFunction R) (z : ℤ) : R := if z ≤ 0 then 0 else f ⌊z⌋₊
Used by 1
Used byNon-pretentious multiplicative functions do not correlate with polynomial phases on short intervals on average

Abbreviation1-bounded function#✓fully proved

A function \(f \colon \mathbb{N} \to \mathbb{C}\) is 1-bounded if \(|f(n)| \le 1\) for every natural number \(n\).

abbrev IsOneBounded (f : ℕ → ℂ) : Prop := ∀ n, ‖f n‖ ≤ 1
Used by 1
Used byNon-pretentious multiplicative functions do not correlate with polynomial phases on short intervals on average

TheoremNon-pretentious multiplicative functions do not correlate with polynomial phases on short intervals on average#●ready to prove

Non-pretentious multiplicative functions do not correlate with polynomial phases on short intervals on average. For a function \(g\) on the integers, a natural number \(k\), a real \(x\) and a real \(H > 0\) write

\[ \|g\|_{u^{k+1}[x, x+H]} = \sup_{\deg P \le k} \frac{1}{H} \Bigl| \sum_{\lceil x \rceil \le n \le \lfloor x + H \rfloor} g(n) e^{-2\pi i P(n)} \Bigr|, \]

the supremum taken over real polynomials \(P\) of degree at most \(k\). For functions \(f, g \colon \mathbb{N} \to \mathbb{C}\) and a real \(X\) let

\[ \mathbb{D}(f, g; X) = \Bigl( \sum_{p \le X} \frac{1 - \operatorname{Re}\bigl(f(p) \overline{g(p)}\bigr)}{p} \Bigr)^{1/2}, \]

the sum taken over primes \(p \le X\), and for a positive integer \(Q\) let \(M(f; X, Q)\) be the infimum of \(\mathbb{D}(f, n \mapsto \chi(n) n^{it}; X)\) over real \(t\) with \(|t| \le X\), positive integers \(q \le Q\) and Dirichlet characters \(\chi\) modulo \(q\).

Let \(k\) be a natural number, \(\theta\) a real number with \(0 < \theta < 1/2\) and \(\eta > 0\) a real number. Then there are a positive integer \(Q\) and real numbers \(C > 0\) and \(B\) such that the following holds for every multiplicative arithmetic function \(f \colon \mathbb{N} \to \mathbb{C}\) with \(|f(n)| \le 1\) for all \(n\), extended to the integers by \(f(n) = 0\) for \(n \le 0\), every real \(X \ge 1\) and every real \(H\) with \(X^\theta \le H \le X^{1-\theta}\): if

\[ \int_X^{2X} \|f\|_{u^{k+1}[x, x+H]} \, dx \ge \eta X, \]

then \(M(f; C X^{k+1} / H^{k+1}, Q) \le B\).

public theorem_wanted theorem_1_3 (k : ℕ) (θ : ℝ) (hθ₀ : 0 < θ) (hθ₁ : θ < 1 / 2) (η : ℝ) (hη : η > 0) :
    ∃ (Q : ℕ+) (_hQ : 1 ≤ Q) (C : ℝ) (_hC : 0 < C) (B : ℝ),
      ∀ (f : ArithmeticFunction ℂ) (_hf : f.IsMultiplicative) (_hf' : IsOneBounded f)
        (X : ℝ) (_hX : X ≥ 1) (H : ℝ) (_hXH : X ^ θ ≤ H) (_hHX : H ≤ X ^ (1 - θ)),
          ∫ x in X..(2 * X), weakGowersUniformityNorm k x H f.intExtension ≥ η * X →
            M f (C * X ^ (k + 1) / H ^ (k + 1)) Q ≤ B
Sources
  • K. Matomäki, M. Radziwiłł, T. Tao, J. Teräväinen, and T. Ziegler, Higher uniformity of bounded multiplicative functions in short intervals on average, Annals of Math, 197 (2) 2023. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_bounded_multiplicative_functions of the lean-eval benchmark.
Uses 2
Statement usesExtension of an arithmetic function to the integers · 1-bounded function

TheoremLiouville's function does not correlate with polynomial phases on short intervals on average#●ready to prove

Let \(\lambda\) be the Liouville function, extended to the integers by \(\lambda(n) = 0\) for \(n \le 0\), let \(k\) be a natural number and let \(\theta\) be a real number with \(0 < \theta < 1\). For real \(x\) and \(H > 0\) write

\[ \|\lambda\|_{u^{k+1}[x, x+H]} = \sup_{\deg P \le k} \frac{1}{H} \Bigl| \sum_{\lceil x \rceil \le n \le \lfloor x + H \rfloor} \lambda(n) e^{-2\pi i P(n)} \Bigr|, \]

the supremum taken over real polynomials \(P\) of degree at most \(k\). Then

\[ \int_X^{2X} \|\lambda\|_{u^{k+1}[x, x + X^\theta]} \, dx = o(X) \]

as the real number \(X\) tends to infinity.

public theorem_wanted corollary_1_1 (k : ℕ) (θ : ℝ) (hθ₀ : 0 < θ) (hθ₁ : θ < 1) :
    (fun X ↦ ∫ x in X..(2 * X), weakGowersUniformityNorm k x (X ^ θ) (fun n ↦ liouville ⌊n⌋₊))
      =o[atTop] (fun X ↦ X)
Sources
  • K. Matomäki, M. Radziwiłł, T. Tao, J. Teräväinen, and T. Ziegler, Higher uniformity of bounded multiplicative functions in short intervals on average, Annals of Math, 197 (2) 2023. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_bounded_multiplicative_functions of the lean-eval benchmark.
2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.