Sieve.prod_factors_one_div_compMult_ge

theorem prod_factors_one_div_compMult_ge (M : ℕ) (f : ArithmeticFunction ℝ)    (hf : CompletelyMultiplicative f) (hf_nonneg : ∀ n, 0 ≤ f n) (d : ℕ) (hd : Squarefree d)    (hf_size : ∀ n, n.Prime → n ∣ d → f n < 1) :    f d * ∏ p ∈ d.primeFactors, 1 / (1 - f p)    ≥ ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f (p^n) := by  calc f d * ∏ p ∈ d.primeFactors, 1 / (1 - f p)    = ∏ p ∈ d.primeFactors, f p / (1 - f p)                 := by        conv => { lhs; congr; rw [←Nat.prod_primeFactors_of_squarefree hd] }        rw [hf.isMultiplicative.map_prod_of_subset_primeFactors _ _ subset_rfl,          ←Finset.prod_mul_distrib]        simp_rw[one_div, div_eq_mul_inv]  _ ≥ ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, (f p)^n  := by    gcongr with p hp    · exact fun p _ => Finset.sum_nonneg fun n _ => pow_nonneg (hf_nonneg p) n    rw [Nat.mem_primeFactors_of_ne_zero hd.ne_zero] at hp    rw [← Finset.Ico_add_one_right_eq_Icc, geom_sum_Ico,      ← mul_div_mul_left (c := (-1 : ℝ)) (f p ^ (M + 1) - f p ^ 1)]    · gcongr      · apply hf_nonneg      · linarith [hf_size p hp.1 hp.2]      · rw [pow_one]        have : 0 ≤ f p ^ (M + 1) := by          apply pow_nonneg          apply hf_nonneg        linarith only [this]      · linarith only    · norm_num    · apply ne_of_lt <| hf_size p hp.1 hp.2    · apply Nat.succ_le_iff.mpr (Nat.succ_pos _)   _ = ∏ p ∈ d.primeFactors, ∑ n ∈ Finset.Icc 1 M, f (p^n)  := by     simp_rw [hf.apply_pow]