theorem ArithmeticFunction.IsMultiplicative.mult_lcm_eq_of_ne_zero {R : Type u_1} [CommGroupWithZero R] (f : ArithmeticFunction R) (h_mult : f.IsMultiplicative) (x y : ℕ) (hf : f (x.gcd y) ≠ 0) : f (x.lcm y) = f x * f y / f (x.gcd y)

theorem ArithmeticFunction.IsMultiplicative.prod_factors_of_mult (f : ArithmeticFunction ℝ) (h_mult : f.IsMultiplicative) {l : ℕ} (hl : Squarefree l) : ∏ a ∈ l.primeFactors, f a = f l

theorem Aux.sum_over_dvd_ite {α : Type u_1} [Ring α] {P : ℕ} (hP : P ≠ 0) {n : ℕ} (hn : n ∣ P) {f : ℕ → α} : ∑ d ∈ n.divisors, f d = ∑ d ∈ P.divisors, if d ∣ n then f d else 0

theorem Aux.sum_intro {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [DecidableEq α] (s : Finset α) {f : α → M} (d : α) (hd : d ∈ s) : f d = ∑ k ∈ s, if k = d then f k else 0

theorem Aux.ite_sum_zero {p : Prop} [Decidable p] (s : Finset ℕ) (f : ℕ → ℝ) : (if p then ∑ x ∈ s, f x else 0) = ∑ x ∈ s, if p then f x else 0

theorem Aux.conv_lambda_sq_larger_sum (f : ℕ → ℕ → ℕ → ℝ) (n : ℕ) : (∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then f d1 d2 d else 0) = ∑ d ∈ n.divisors, ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0

theorem Aux.moebius_inv_dvd_lower_bound (l m : ℕ) (hm : Squarefree m) : (∑ d ∈ m.divisors, if l ∣ d then ArithmeticFunction.moebius d else 0) = if l = m then ArithmeticFunction.moebius l else 0

theorem Aux.moebius_inv_dvd_lower_bound' {P : ℕ} (hP : Squarefree P) (l m : ℕ) (hm : m ∣ P) : (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ m then ArithmeticFunction.moebius d else 0) = if l = m then ArithmeticFunction.moebius l else 0

theorem Aux.moebius_inv_dvd_lower_bound_real {P : ℕ} (hP : Squarefree P) (l m : ℕ) (hm : m ∣ P) : (∑ d ∈ P.divisors, if l ∣ d ∧ d ∣ m then ↑(ArithmeticFunction.moebius d) else 0) = if l = m then ↑(ArithmeticFunction.moebius l) else 0

theorem Aux.gcd_dvd_mul (m n : ℕ) : m.gcd n ∣ m * n

theorem Aux.multiplicative_zero_of_zero_dvd (f : ArithmeticFunction ℝ) (h_mult : f.IsMultiplicative) {m n : ℕ} (h_sq : Squarefree n) (hmn : m ∣ n) (h_zero : f m = 0) : f n = 0

theorem Aux.primeDivisors_nonempty (n : ℕ) (hn : 2 ≤ n) : n.primeFactors.Nonempty

theorem Aux.div_mult_of_dvd_squarefree (f : ArithmeticFunction ℝ) (h_mult : f.IsMultiplicative) (l d : ℕ) (hdl : d ∣ l) (hl : Squarefree l) (hd : f d ≠ 0) : f l / f d = f (l / d)

theorem Aux.inv_sub_antitoneOn_gt {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (c : R) : AntitoneOn (fun (x : R) => (x - c)⁻¹) (Set.Ioi c)

theorem Aux.inv_sub_antitoneOn_Icc {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (a b c : R) (ha : c < a) : AntitoneOn (fun (x : R) => (x - c)⁻¹) (Set.Icc a b)

theorem Aux.inv_antitoneOn_pos {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] : AntitoneOn (fun (x : R) => x⁻¹) (Set.Ioi 0)

theorem Aux.inv_antitoneOn_Icc {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (a b : R) (ha : 0 < a) : AntitoneOn (fun (x : R) => x⁻¹) (Set.Icc a b)

theorem Aux.log_add_one_le_sum_inv (n : ℕ) : Real.log ↑(n + 1) ≤ ∑ d ∈ Finset.Icc 1 n, (↑d)⁻¹

theorem Aux.log_le_sum_inv (y : ℝ) (hy : 1 ≤ y) : Real.log y ≤ ∑ d ∈ Finset.Icc 1 ⌊y⌋₊, (↑d)⁻¹

theorem Aux.sum_inv_le_log (n : ℕ) (hn : 1 ≤ n) : ∑ d ∈ Finset.Icc 1 n, (↑d)⁻¹ ≤ 1 + Real.log ↑n

theorem Aux.sum_inv_le_log_real (y : ℝ) (hy : 1 ≤ y) : ∑ d ∈ Finset.Icc 1 ⌊y⌋₊, (↑d)⁻¹ ≤ 1 + Real.log y

theorem Aux.Nat.le_prod {ι : Type u_1} [DecidableEq ι] {f : ι → ℕ} {s : Finset ι} {i : ι} (hi : i ∈ s) (hf : ∀ i ∈ s, f i ≠ 0) : f i ≤ ∏ j ∈ s, f j

theorem Aux.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 ^ ArithmeticFunction.cardDistinctFactors d / ↑d else 0) ≤ (1 + Real.log x) ^ k

theorem Aux.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 ^ ArithmeticFunction.cardDistinctFactors d else 0) ≤ x * (1 + Real.log x) ^ h