def C_DLS : ℝ

Equations

• C_DLS = sorry

theorem Delta_LambdaSharp_bound [ProofData] {q r : ℕ} [NeZero q] {a : ZMod q} (ha : IsUnit a) (hr : ↑r ≤ ProofData.x) {y : ℝ} (hy : y ≤ ProofData.x) : |Δ_[onCoprime r ⇑LambdaSharp](y; q, a)| ≤ C_DLS * ProofData.U * ProofData.V * Real.log ProofData.x

theorem BV_LambdaSharp [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) => |Δ_[⇑LambdaSharp](y; q, a)|) ≤ ProofData.x / Real.log ProofData.x ^ A