Type II sums: the flat part $\Lambda^\flat$

noncomputable def S [ProofData] {q : ℕ} (r : ℕ) (y : ℝ) (ξ : DirichletCharacter ℂ q) : ℝ

$S_r(y, \xi) := \left|\sum_{n \le y} \Lambda_r^\flat(n)\,\xi(n)\right|$

Equations

• S r y ξ = ‖summatory (fun (n : ℕ) => ↑(onCoprime r (⇑LambdaFlat) n) * ξ ↑n) y‖

noncomputable def T [ProofData] (C : ℝ) (r : ℕ) (Q : ℝ) : ℝ

$T_r(x, Q) := \sum_{(\log x)^C < d \le Q/r} \frac{1}{\varphi(d)} \sum_{\xi \pmod{d}}^* \max_{\sqrt{x} \le y \le x} S_r(y, \xi)$

Equations

• T C r Q = ∑ d ∈ Nat.Icc (Real.log ProofData.x ^ C) (Q / ↑r), (↑d.totient)⁻¹ * ∑ ξ : DirichletCharacter ℂ d with ξ.IsPrimitive, maxy fun (y : ℝ) => S r y ξ

Reduction to character sums

theorem character_sum_by_conductor {R : Type u_1} [AddCommMonoid R] {q : ℕ} (f : DirichletCharacter ℂ q → R) : ∑ χ : DirichletCharacter ℂ q with χ ≠ 1, f χ = ∑ d ∈ q.divisors.attach, ∑ ξ : DirichletCharacter ℂ ↑d with ξ.IsPrimitive, f ((DirichletCharacter.changeLevel ⋯) ξ)

theorem character_sum_Mobius (f : ArithmeticFunction ℝ) {r q : ℕ} {x : ℝ} {a : ZMod q} (hq : 1 < q) (hrx : ↑r ≤ x) (ha : IsUnit a) : ∑ ξ : DirichletCharacter ℂ q with ξ.IsPrimitive, star (ξ a) * summatory (fun (n : ℕ) => ξ ↑n * ↑(onCoprime r (⇑f) n)) x = ↑(∑ p ∈ q.divisorsAntidiagonal, ↑(ArithmeticFunction.moebius p.2) * ↑p.1.totient * Δ_[onCoprime (r * q) ⇑f](x; q, a))

theorem Delta_LambdaFlat_decomp [ProofData] {C : ℕ} {y : ℝ} (q : ℕ) (a : ZMod q) (ha : IsUnit a) : |Δ_[⇑LambdaFlat](y; q, a)| ≤ (↑q.totient)⁻¹ * |∑ d ∈ q.divisors with 1 < d ∧ ↑d ≤ Real.log ProofData.x ^ C, ∑ p ∈ d.divisorsAntidiagonal, ↑(ArithmeticFunction.moebius p.2) * ↑p.1.totient * Δ_[onCoprime q ⇑LambdaFlat](y; p.1, a.cast)|

def C_DLF (A C : ℝ) : ℝ

Equations

• C_DLF A C = sorry

theorem Delta_LambdaFlat_small_conductor [ProofData] (A C : ℕ) {y : ℝ} (q : ℕ) (a : ZMod q) (ha : IsUnit a) : |∑ d ∈ q.divisors with 1 < d ∧ ↑d ≤ Real.log ProofData.x ^ C, ∑ p ∈ d.divisorsAntidiagonal, ↑(ArithmeticFunction.moebius p.2) * ↑p.1.totient * Δ_[onCoprime q ⇑LambdaFlat](y; p.1, a.cast)| ≤ C_DLF ↑A ↑C * ProofData.x / Real.log ProofData.x ^ (A + 1)

def C_BV_LFT : ℝ

Equations

• C_BV_LFT = sorry

theorem BV_LambdaFlat_via_T (Q : ℝ) (A C : ℕ) [ProofData] : |summatory (fun (q : ℕ) => maxya q fun (y : ℝ) (a : ZMod q) => |Δ_[⇑LambdaFlat](y; q, a)|) Q - summatory (fun (r : ℕ) => T (↑C) r Q) Q| ≤ C_BV_LFT * ProofData.x / Real.log ProofData.x ^ A

Large sieve estimates

theorem LargeSieve_convolution {M N : ℕ} (f g : ArithmeticFunction ℝ) (hf : ∀ n > M, f n = 0) (hg : ∀ n > N, g n = 0) {x Q : ℝ} (hx : 1 ≤ x) (hQ : 1 ≤ Q) : summatory (fun (q : ℕ) => ∑ χ : DirichletCharacter ℂ q with χ.IsPrimitive, ↑q * (↑q.totient)⁻¹ * ⨆ y ∈ Set.Icc 1 x, ‖summatory (fun (n : ℕ) => ↑((f * g) n) * χ ↑n) y‖) Q ≤ (√(↑N * ↑M) + √↑M * Q + √↑N * Q + Q ^ 2) * √(∑ n ∈ Finset.Icc 1 M, f n ^ 2) * √(∑ n ∈ Finset.Icc 1 N, g n ^ 2)

noncomputable def pows2Ioc (x y : ℝ) : Finset ℕ

The finset of natural numbers j such that $x < 2^j ≤ y$

Equations

• pows2Ioc x y = if 1 ≤ y ∧ x < y then Finset.Ioc ⌊Real.logb 2 x⌋₊ ⌊Real.logb 2 y⌋₊ else ∅

@[simp]

theorem mem_pows2Ioc (x y : ℝ) (hx : 1 ≤ x) (n : ℕ) : n ∈ pows2Ioc x y ↔ x < 2 ^ n ∧ 2 ^ n ≤ y

theorem LambdaFlat_dyadic [ProofData] (n : ℕ) (hn : ↑n ≤ ProofData.x) : LambdaFlat n = ∑ j ∈ pows2Ioc ProofData.V (2 * ProofData.x / ProofData.V), (f✝ j * g✝ j) n

def C_BV_char_sum : ℝ

Equations

• C_BV_char_sum = sorry

theorem BV_char_sum_bound [ProofData] (r : ℕ) (Q : ℝ) (hQ : 2 ≤ Q) : summatory (fun (q : ℕ) => ∑ ξ : DirichletCharacter ℂ q with ξ.IsPrimitive, ↑q * (↑q.totient)⁻¹ * maxy fun (y : ℝ) => S r y ξ) Q ≤ C_BV_char_sum * (ProofData.x + Q * ProofData.x / √ProofData.U + Q * ProofData.x / √ProofData.V + Q ^ 2 * √ProofData.x) * Real.log ProofData.x ^ 3

def C_Tr : ℝ

Equations

• C_Tr = sorry

theorem T_r_bound [ProofData] (C r : ℕ) (Q : ℝ) (hQ : 2 ≤ Q) : T (↑C) r Q ≤ C_Tr * (ProofData.x / Real.log ProofData.x ^ (C - 3) + ProofData.x * Real.log ProofData.x ^ 4 * √ProofData.U + ProofData.x * Real.log ProofData.x ^ 4 * √ProofData.V + Q * √ProofData.x * Real.log ProofData.x ^ 3 / ↑r)

def C_BV_LF (A : ℝ) : ℝ

Equations

• C_BV_LF A = sorry

theorem BV_LambdaFlat [ProofData] (A : ℕ) (Q : ℝ) (h1Q : 1 ≤ Q) (hQ : Q ≤ √ProofData.x / Real.log ProofData.x ^ (A + 3)) : (∑ q ∈ Nat.Icc 0 Q, maxya q fun (y : ℝ) (a : ZMod q) => |Δ_[⇑LambdaFlat](y; q, a)|) ≤ C_BV_LF ↑A * ProofData.x / Real.log ProofData.x ^ A