trans (∑ d in P.divisors, x * if ↑d ≤ x then (h : ℝ) ^ ω d / d else (0 : ℝ))
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (∑ d ∈ P.divisors, if ↑d ≤ x then ↑h ^ ω d else 0) ≤ x * (1 + x.log) ^ h
P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (∑ d ∈ P.divisors, if ↑d ≤ x then ↑h ^ ω d else 0) ≤ ∑ d ∈ P.divisors, x * if ↑d ≤ x then ↑h ^ ω d / ↑d else 0

P h : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (∑ d ∈ P.divisors, x * if ↑d ≤ x then ↑h ^ ω d / ↑d else 0) ≤ x * (1 + x.log) ^ h