theorem LambdaLEU_le_log [ProofData] {n : ℕ} : LambdaLEU n ≤ Real.log ↑n

theorem summatory_mono_fun (f g : ℕ → ℝ) (x : ℝ) (hfg : ∀ (n : ℕ), ↑n ≤ x → f n ≤ g n) : summatory f x ≤ summatory g x

theorem summatory_mono {f : ℕ → ℝ} {x y : ℝ} (hxy : x ≤ y) (hf : ∀ (n : ℕ), ↑n ≤ y → 0 ≤ f n) : summatory f x ≤ summatory f y

theorem sum_LambdaLEU_le [ProofData] {y : ℝ} : summatory (⇑LambdaLEU) y ≤ ProofData.U * Real.log ProofData.x

theorem Delta_LambdaLEU_bound [ProofData] {y : ℝ} {q : ℕ} (hq : 0 < q) {a : ZMod q} : |Δ_[⇑LambdaLEU](y; q, a)| ≤ 2 * ProofData.U * Real.log ProofData.x

theorem BV_LambdaLE [ProofData] {A : ℕ} (Q : ℝ) (hQ_nonneg : 0 ≤ Q) (hQ : Q ≤ √ProofData.x / Real.log ProofData.x ^ (A + 3)) : (∑ q ∈ Nat.Icc 1 Q, maxya q fun (y : ℝ) (a : ZMod q) => |Δ_[⇑LambdaLEU](y; q, a)|) ≤ 2 * ProofData.x / Real.log ProofData.x ^ (A + 2)