Aux.sum_pow_cardDistinctFactors_le_self_mul_log_pow

theorem sum_pow_cardDistinctFactors_le_self_mul_log_pow {P h : ℕ} (x : ℝ) (hx : 1 ≤ x)    (hP : Squarefree P) :    (∑ d ∈ P.divisors, if ↑d ≤ x then (h : ℝ) ^ ω d else (0 : ℝ)) ≤      x * (1 + Real.log x) ^ h := by  trans (∑ d ∈ P.divisors, x * if ↑d ≤ x then (h : ℝ) ^ ω d / d else (0 : ℝ))  · simp_rw [mul_ite, mul_zero, ←sum_filter]    gcongr with i hi    rw [div_eq_mul_inv, mul_comm _ (i:ℝ)⁻¹, ←mul_assoc]    trans (1*(h:ℝ)^ω i)    · rw [one_mul]    gcongr    rw [mem_filter] at hi    rw [←div_eq_mul_inv]    apply one_le_div (by norm_cast; apply Nat.pos_of_mem_divisors hi.1) |>.mpr hi.2  rw [←mul_sum];  gcongr  apply sum_pow_cardDistinctFactors_div_self_le_log_pow x hx hP