Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow

theorem sum_pow_cardDistinctFactors_div_self_le_log_pow {P k : ℕ} (x : ℝ) (hx : 1 ≤ x)    (hP : Squarefree P) :    (∑ d ∈ P.divisors, if d ≤ x then (k:ℝ) ^ (ω d) / (d : ℝ) else (0 : ℝ))    ≤ (1 + Real.log x) ^ k := by  have hx_pos : 0 < x := by    linarith  calc    _ = ∑ d ∈ P.divisors,          ∑ a ∈ Fintype.piFinset fun _i : Fin k => P.divisors,            if ∏ i, a i = d ∧ d ∣ P then if ↑d ≤ x then (d : ℝ)⁻¹ else 0 else 0 := ?_    _ = ∑ a ∈ Fintype.piFinset fun _i : Fin k => P.divisors,          if ∏ i, a i ∣ P then if ↑(∏ i, a i) ≤ x then ∏ i, (a i : ℝ)⁻¹ else 0 else 0 := ?_    _ ≤ ∑ a ∈ Fintype.piFinset fun _i : Fin k => P.divisors,          if ↑(∏ i, a i) ≤ x then ∏ i, (a i : ℝ)⁻¹ else 0 := ?_ -- do we need this one?    _ ≤ ∑ a ∈ Fintype.piFinset fun _i : Fin k => P.divisors,          ∏ i, if ↑(a i) ≤ x then (a i : ℝ)⁻¹ else 0 := ?_    _ = ∏ _i : Fin k, ∑ d ∈ P.divisors, if ↑d ≤ x then (d : ℝ)⁻¹ else 0 := by rw [prod_univ_sum]    _ = (∑ d ∈ P.divisors, if ↑d ≤ x then (d : ℝ)⁻¹ else 0) ^ k := by      rw [prod_const, Finset.card_fin]    _ ≤ (1 + Real.log x) ^ k := ?_   · apply sum_congr rfl; intro d hd    rw [mem_divisors] at hd    simp_rw [ite_and];    rw [← sum_filter, Finset.sum_const, ← finMulAntidiag_eq_piFinset_divisors_filter hd.1 hd.2,      card_finMulAntidiag_of_squarefree <| hP.squarefree_of_dvd hd.1, if_pos hd.1]    simp only [div_eq_mul_inv, nsmul_eq_mul, cast_pow, mul_ite, mul_zero]  · rw [sum_comm]; apply sum_congr rfl; intro a _; rw [sum_eq_single (∏ i, a i)]    · apply if_ctx_congr _ _ (fun _ => rfl)      · rw [Iff.comm, iff_and_self]; exact fun _ => rfl      · intro; rw [cast_prod, ← prod_inv_distrib]    · exact fun d _ hd_ne ↦ if_neg fun h => hd_ne.symm h.1    · exact fun h ↦ if_neg fun h' => h (mem_divisors.mpr ⟨h'.2, hP.ne_zero⟩)  · apply sum_le_sum; intro a _    by_cases h : (∏ i, a i ∣ P)    · rw [if_pos h]    rw [if_neg h]    split_ifs with h'    · apply prod_nonneg; intro i _; norm_num    · rfl  · apply sum_le_sum; intro a ha    split_ifs with h    · gcongr with i hi      rw [if_pos]      apply le_trans _ h      norm_cast      rw [←prod_erase_mul (a:=i) (h:= hi)]      apply Nat.le_mul_of_pos_left      rw [Fintype.mem_piFinset] at ha      apply prod_pos; intro j _; apply pos_of_mem_divisors (ha j)    · apply prod_nonneg; intro j _      split_ifs      · norm_num      · rfl  · rw [←sum_filter]    gcongr    trans (∑ d ∈ Icc 1 (floor x), (d:ℝ)⁻¹)    · apply sum_le_sum_of_subset_of_nonneg      · intro d; rw[mem_filter, mem_Icc]        intro hd        constructor        · rw [Nat.succ_le_iff]; exact pos_of_mem_divisors hd.1        · rw [le_floor_iff hx_pos.le]          exact hd.2      · norm_num    apply sum_inv_le_log_real    linarith