Weighted sums of Dirichlet convolutions
DefinitionIndicator of \(B_\kappa\)-free integers#✓fully proved
Let \(\kappa\) be a function from the natural numbers to the natural numbers (only its values \(\kappa(p)\) at primes \(p\) matter) and let \(B_\kappa\) be the set of prime powers \(p^{\kappa(p)}\). A natural number \(n\) is \(B_\kappa\)-free if \(n \ge 1\) and no \(p^{\kappa(p)}\) with \(p\) prime divides \(n\). The indicator \(q_{B_\kappa}\) is the integer-valued arithmetic function with \(q_{B_\kappa}(n) = 1\) if \(n\) is \(B_\kappa\)-free and \(q_{B_\kappa}(n) = 0\) otherwise.
The paper indexes the exponents by the position of the prime (\(b_i = p_i^{\kappa_i}\)); here \(\kappa\) is indexed by the prime itself. For constant \(\kappa = k\) this is the indicator \(q_k\) of \(k\)-free integers.
public noncomputable def bFreeIndicator (κ : ℕ → ℕ) : ArithmeticFunction ℤ :=
⟨fun n => if n ≠ 0 ∧ ∀ p : ℕ, p.Prime → ¬ p ^ κ p ∣ n then 1 else 0, by simp⟩
Sources
- André Pierro de Camargo, Weighted Summation of Dirichlet Convolutions and Applications to Some Divisor Problems over k-Free and B-Free Integers, INTEGERS 24 (2024), Article A75, Equations (2), (11), (12).
Used by 8
TheoremValues of the \(B_\kappa\)-free indicator#✓fully proved
Let \(\kappa\) be a function from the natural numbers to the natural numbers. For every natural number \(n\), the indicator \(q_{B_\kappa}\) of \(B_\kappa\)-free integers satisfies \(q_{B_\kappa}(n) = 1\) if \(n \ne 0\) and no \(p^{\kappa(p)}\) with \(p\) prime divides \(n\), and \(q_{B_\kappa}(n) = 0\) otherwise.
public theorem bFreeIndicator_apply (κ : ℕ → ℕ) (n : ℕ) :
bFreeIndicator κ n = if n ≠ 0 ∧ ∀ p : ℕ, p.Prime → ¬ p ^ κ p ∣ n then 1 else 0
public noncomputable def bFreeIndicator (κ : ℕ → ℕ) : ArithmeticFunction ℤ :=
⟨fun n => if n ≠ 0 ∧ ∀ p : ℕ, p.Prime → ¬ p ^ κ p ∣ n then 1 else 0, by simp⟩
WantedExt/NumberTheory/WeightedDirichletConvolutionWanted.lean:35
Sources
- André Pierro de Camargo, Weighted Summation of Dirichlet Convolutions and Applications to Some Divisor Problems over k-Free and B-Free Integers, INTEGERS 24 (2024), Article A75, Equations (11), (12).
Uses 1 · Used by 2
TheoremThe integer \(1\) is \(B_\kappa\)-free#✓fully proved
Let \(\kappa\) be a function from the natural numbers to the natural numbers with \(\kappa(p) \ge 1\) for every prime \(p\). Then the indicator \(q_{B_\kappa}\) of \(B_\kappa\)-free integers satisfies \(q_{B_\kappa}(1) = 1\).
public theorem bFreeIndicator_one {κ : ℕ → ℕ} (hκ : ∀ p : ℕ, p.Prime → 1 ≤ κ p) :
bFreeIndicator κ 1 = 1
public noncomputable def bFreeIndicator (κ : ℕ → ℕ) : ArithmeticFunction ℤ :=
⟨fun n => if n ≠ 0 ∧ ∀ p : ℕ, p.Prime → ¬ p ^ κ p ∣ n then 1 else 0, by simp⟩
WantedExt/NumberTheory/WeightedDirichletConvolutionWanted.lean:35
Sources
- André Pierro de Camargo, Weighted Summation of Dirichlet Convolutions and Applications to Some Divisor Problems over k-Free and B-Free Integers, INTEGERS 24 (2024), Article A75, Equation (12).
Uses 2
TheoremThe prime power \(p^{\kappa(p)}\) is not \(B_\kappa\)-free#✓fully proved
Let \(\kappa\) be a function from the natural numbers to the natural numbers and let \(p\) be a prime. Then the indicator \(q_{B_\kappa}\) of \(B_\kappa\)-free integers satisfies \(q_{B_\kappa}(p^{\kappa(p)}) = 0\).
No positivity of \(\kappa(p)\) is assumed; for \(\kappa(p) = 0\) the statement is \(q_{B_\kappa}(1) = 0\).
public theorem bFreeIndicator_prime_pow {κ : ℕ → ℕ} {p : ℕ} (hp : p.Prime) :
bFreeIndicator κ (p ^ κ p) = 0
public noncomputable def bFreeIndicator (κ : ℕ → ℕ) : ArithmeticFunction ℤ :=
⟨fun n => if n ≠ 0 ∧ ∀ p : ℕ, p.Prime → ¬ p ^ κ p ∣ n then 1 else 0, by simp⟩
WantedExt/NumberTheory/WeightedDirichletConvolutionWanted.lean:35
Sources
- André Pierro de Camargo, Weighted Summation of Dirichlet Convolutions and Applications to Some Divisor Problems over k-Free and B-Free Integers, INTEGERS 24 (2024), Article A75, Equation (12).
Uses 2
TheoremProduct formula for homogeneous sums of powers#●ready to prove
Let \(R\) be a commutative ring, let \(a, b \in R\) and let \(\tau, \xi\) be natural numbers. Then
where a sum with upper limit \(-1\) is zero.
In the source, \(a\) and \(b\) are the values \(u(n)\) and \(v(n)\) of complex arithmetic functions.
public theorem_wanted sum_pow_mul_pow_add_eq {R : Type*} [CommRing R] (a b : R) (τ ξ : ℕ) :
∑ j ∈ Finset.range (τ + ξ + 1), a ^ j * b ^ (τ + ξ - j) =
(∑ j ∈ Finset.range (τ + 1), a ^ j * b ^ (τ - j)) *
(∑ i ∈ Finset.range (ξ + 1), a ^ i * b ^ (ξ - i)) -
a * b * (∑ j ∈ Finset.range τ, a ^ j * b ^ (τ - 1 - j)) *
(∑ i ∈ Finset.range ξ, a ^ i * b ^ (ξ - 1 - i))
Sources
- André Pierro de Camargo, Weighted Summation of Dirichlet Convolutions and Applications to Some Divisor Problems over k-Free and B-Free Integers, INTEGERS 24 (2024), Article A75, Lemma 1, Equation (16).
TheoremGcd expansion of a convolution of completely multiplicative functions at a product#●ready to prove
Let \(u\) and \(v\) be complex-valued completely multiplicative arithmetic functions, meaning \(u(mn) = u(m) u(n)\) and \(v(mn) = v(m) v(n)\) for all natural numbers \(m\) and \(n\). Let \(u * v\) be their Dirichlet convolution and \(\mu\) the Möbius function. Then for all natural numbers \(r\) and \(s\),
the sum running over the positive divisors \(m\) of \(\gcd(r, s)\) (it is empty when \(r = s = 0\)).
The paper takes \(r, s\) positive; the identity also holds (both sides vanish) when \(r\) or \(s\) is \(0\), so no positivity hypothesis is imposed.
public theorem_wanted dirichletConvolution_mul_eq_sum_gcd {u v : ArithmeticFunction ℂ}
(hu : u.IsCompletelyMultiplicative) (hv : v.IsCompletelyMultiplicative) (r s : ℕ) :
(u * v) (r * s) = ∑ m ∈ (Nat.gcd r s).divisors,
(μ m : ℂ) * u m * v m * (u * v) (r / m) * (u * v) (s / m)
Sources
- André Pierro de Camargo, Weighted Summation of Dirichlet Convolutions and Applications to Some Divisor Problems over k-Free and B-Free Integers, INTEGERS 24 (2024), Article A75, Lemma 2, Equation (17).
Uses 1
TheoremSums of a Dirichlet convolution over multiples of \(r\)#●ready to prove
Let \(u\) and \(v\) be completely multiplicative arithmetic functions with complex values, let \(u * v\) be their Dirichlet convolution, let \(\mu\) be the Möbius function, and for real \(y\) put \(D(y) = \sum_{1 \le j \le y} (u * v)(j)\). Then for every natural number \(r\) and every real \(x\),
where \(d\) and \(m\) run over positive divisors and \(x/0 = 0\), so both sides vanish for \(r = 0\).
Both sides also vanish for \(x < 1\); the source assumes \(r \ge 1\) and \(x \ge 1\).
public theorem_wanted sum_dirichletConvolution_mul_eq {u v : ArithmeticFunction ℂ}
(hu : u.IsCompletelyMultiplicative) (hv : v.IsCompletelyMultiplicative) (r : ℕ) (x : ℝ) :
∑ j ∈ Finset.Icc 1 ⌊x / r⌋₊, (u * v) (r * j) =
∑ d ∈ r.divisors, u d * v (r / d) * ∑ m ∈ d.divisors, (μ m : ℂ) * v m *
∑ j ∈ Finset.Icc 1 ⌊x / (m * r)⌋₊, (u * v) j
Sources
- André Pierro de Camargo, Weighted Summation of Dirichlet Convolutions and Applications to Some Divisor Problems over k-Free and B-Free Integers, INTEGERS 24 (2024), Article A75, Lemma 3, Equation (20).
Uses 1
TheoremMöbius expansion of weighted sums of a Dirichlet convolution#●ready to prove
Let \(w\), \(u\) and \(v\) be arithmetic functions with complex values, let \(*\) denote Dirichlet convolution, let \(\mu\) be the Möbius function and put \(g = w * \mu\). Then for every real \(x\),
where \(j\) and \(r\) run over positive integers.
Both sides vanish for \(x < 1\); the source assumes \(x \ge 1\).
public theorem_wanted sum_mul_dirichletConvolution_eq_sum_moebius (w u v : ArithmeticFunction ℂ)
(x : ℝ) :
∑ j ∈ Finset.Icc 1 ⌊x⌋₊, w j * (u * v) j =
∑ r ∈ Finset.Icc 1 ⌊x⌋₊, (w * (μ : ArithmeticFunction ℂ)) r *
∑ j ∈ Finset.Icc 1 ⌊x / r⌋₊, (u * v) (r * j)
Sources
- André Pierro de Camargo, Weighted Summation of Dirichlet Convolutions and Applications to Some Divisor Problems over k-Free and B-Free Integers, INTEGERS 24 (2024), Article A75, Lemma 4.
TheoremWeighted summation of Dirichlet convolutions#●ready to prove
Let \(u\) and \(v\) be completely multiplicative arithmetic functions with complex values, let \(w\) be any arithmetic function with complex values, let \(*\) denote Dirichlet convolution, let \(\mu\) be the Möbius function, put \(g = w * \mu\), and for real \(y\) put \(D(y) = \sum_{1 \le j \le y} (u * v)(j)\). Then for every real \(x\),
where \(r\), \(d\) and \(m\) run over positive integers.
Both sides vanish for \(x < 1\); the source assumes \(x \ge 1\).
public theorem_wanted weighted_sum_dirichletConvolution_eq {u v : ArithmeticFunction ℂ}
(hu : u.IsCompletelyMultiplicative) (hv : v.IsCompletelyMultiplicative)
(w : ArithmeticFunction ℂ) (x : ℝ) :
∑ j ∈ Finset.Icc 1 ⌊x⌋₊, w j * (u * v) j =
∑ r ∈ Finset.Icc 1 ⌊x⌋₊, (w * (μ : ArithmeticFunction ℂ)) r *
∑ d ∈ r.divisors, u d * v (r / d) * ∑ m ∈ d.divisors, (μ m : ℂ) * v m *
∑ j ∈ Finset.Icc 1 ⌊x / (m * r)⌋₊, (u * v) j
Sources
- André Pierro de Camargo, Weighted Summation of Dirichlet Convolutions and Applications to Some Divisor Problems over k-Free and B-Free Integers, INTEGERS 24 (2024), Article A75, Theorem 1, Equation (8).
Uses 1
TheoremThe \(B_\kappa\)-free indicator convolved with the Möbius function#●ready to prove
Let \(\kappa\) be a function from the natural numbers to the natural numbers with \(\kappa(p) \ge 1\) for every prime \(p\), let \(q_{B_\kappa}\) be the indicator of \(B_\kappa\)-free integers, let \(\mu\) be the Möbius function and let \(*\) denote Dirichlet convolution. Let \(n \ge 1\) be a natural number with prime factorization \(n = \prod_p p^{e_p}\). If \(\kappa(p)\) divides \(e_p\) for every prime \(p\), then \((q_{B_\kappa} * \mu)(n) = \mu(n^{1/\kappa})\), where \(n^{1/\kappa} = \prod_p p^{e_p/\kappa(p)}\); otherwise \((q_{B_\kappa} * \mu)(n) = 0\).
The source indexes the exponents by the position of the prime (\(\kappa_i\) for the \(i\)-th prime \(p_i\)) and requires \(b_i = p_i^{\kappa_i} > 1\), which is the hypothesis \(\kappa(p) \ge 1\).
public theorem_wanted bFreeIndicator_mul_moebius_apply {κ : ℕ → ℕ}
(hκ : ∀ p : ℕ, p.Prime → 1 ≤ κ p) {n : ℕ} (hn : 1 ≤ n) :
(bFreeIndicator κ * μ) n =
if ∀ p : ℕ, κ p ∣ n.factorization p then
μ (n.factorization.prod fun p e => p ^ (e / κ p))
else 0
public noncomputable def bFreeIndicator (κ : ℕ → ℕ) : ArithmeticFunction ℤ :=
⟨fun n => if n ≠ 0 ∧ ∀ p : ℕ, p.Prime → ¬ p ^ κ p ∣ n then 1 else 0, by simp⟩
WantedExt/NumberTheory/WeightedDirichletConvolutionWanted.lean:35
Sources
- André Pierro de Camargo, Weighted Summation of Dirichlet Convolutions and Applications to Some Divisor Problems over k-Free and B-Free Integers, INTEGERS 24 (2024), Article A75, Lemma 5, Equation (22).
Uses 1
TheoremThe \(B_\kappa\)-free indicator twisted by the principal character, convolved with \(\mu\)#●ready to prove
Let \(\kappa\) be a function from the natural numbers to the natural numbers with \(\kappa(p) \ge 1\) for every prime \(p\), let \(\xi\) be a natural number, let \(q_{B_\kappa}\) be the indicator of \(B_\kappa\)-free integers and let \(\mu\) be the Möbius function. Put \(w(d) = q_{B_\kappa}(d)\) if \(\gcd(d, \xi) = 1\) and \(w(d) = 0\) otherwise, so that \(w = q_{B_\kappa} \chi_\xi\) with \(\chi_\xi\) the principal character modulo \(\xi\), and let \((w * \mu)(n) = \sum_{d \mid n} w(d) \mu(n/d)\), the sum running over the positive divisors \(d\) of \(n\) (it is empty for \(n = 0\)). For \(r \ge 1\) with prime factorization \(r = \prod_p p^{e_p}\) write \(r^\kappa = \prod_p p^{\kappa(p) e_p}\), and set \(0^\kappa = 1\). Then for every natural number \(n\) with \((w * \mu)(n) \ne 0\) there are natural numbers \(\ell\) and \(r\) with \(\ell \mid \xi\), \(\gcd(r, \xi) = 1\) and \(n = \ell r^\kappa\). Moreover, for all natural numbers \(\ell\) and \(r\) with \(\ell \mid \xi\), \(\gcd(r, \xi) = 1\) and \(r \ge 1\), \((w * \mu)(\ell r^\kappa) = \mu(\ell) \mu(r)\).
The hypothesis \(r \ge 1\) in the evaluation is needed: for \(r = 0\) the formula is false. No positivity of \(\xi\) is assumed.
public theorem_wanted bFreeCoprimeIndicator_mul_moebius {κ : ℕ → ℕ}
(hκ : ∀ p : ℕ, p.Prime → 1 ≤ κ p) (ξ : ℕ) :
(∀ n : ℕ, ∑ d ∈ n.divisors, (if d.Coprime ξ then bFreeIndicator κ d else 0) * μ (n / d) ≠ 0 →
∃ ℓ r : ℕ, ℓ ∣ ξ ∧ r.Coprime ξ ∧ n = ℓ * r.factorization.prod fun p e => p ^ (κ p * e)) ∧
∀ ℓ r : ℕ, ℓ ∣ ξ → r.Coprime ξ → 0 < r →
∑ d ∈ (ℓ * r.factorization.prod fun p e => p ^ (κ p * e)).divisors,
(if d.Coprime ξ then bFreeIndicator κ d else 0) *
μ ((ℓ * r.factorization.prod fun p e => p ^ (κ p * e)) / d) = μ ℓ * μ r
public noncomputable def bFreeIndicator (κ : ℕ → ℕ) : ArithmeticFunction ℤ :=
⟨fun n => if n ≠ 0 ∧ ∀ p : ℕ, p.Prime → ¬ p ^ κ p ∣ n then 1 else 0, by simp⟩
WantedExt/NumberTheory/WeightedDirichletConvolutionWanted.lean:35
Sources
- André Pierro de Camargo, Weighted Summation of Dirichlet Convolutions and Applications to Some Divisor Problems over k-Free and B-Free Integers, INTEGERS 24 (2024), Article A75, Lemma 6, Equation (23).
Uses 1
TheoremAsymptotic for the divisor function summed over \(k\)-free integers#●ready to prove
Let \(k \ge 2\) be a natural number, let \(q_k\) be the indicator of \(k\)-free integers (the indicator of \(B_\kappa\)-free integers for the constant function \(\kappa = k\)), let \(\tau(n)\) be the number of positive divisors of \(n\), let \(\gamma\) be the Euler–Mascheroni constant, let \(\Delta(x) = \sum_{1 \le n \le x} \tau(n) - x \log x - (2\gamma - 1) x\) be the Dirichlet divisor error term, and put
the product running over all primes \(p\). Then there is a real constant \(\beta_k\) such that \(E(x) = \sum_{1 \le n \le x} q_k(n) \tau(n) - c_k x \log x - \beta_k x\) satisfies the following as \(x \to \infty\). If \(k \le 3\), then \(E(x) = O(x^{1/k + \varepsilon})\) for every \(\varepsilon > 0\). If \(k \ge 4\), then for every real \(\eta \ge 1/4\) with \(\Delta(x) = O(x^\eta)\), \(E(x) = O(x^{\eta + \varepsilon})\) for every \(\varepsilon > 0\).
public theorem_wanted kFree_divisor_sum_asymptotic {k : ℕ} (hk : 2 ≤ k) :
∃ β : ℝ,
let err : ℝ → ℝ := fun x =>
(∑ n ∈ Finset.Icc 1 ⌊x⌋₊, (bFreeIndicator (fun _ => k) n : ℝ) * n.divisors.card) -
(∏' p : Nat.Primes, (1 - (k + 1) / (p : ℝ) ^ k + k / (p : ℝ) ^ (k + 1))) *
x * Real.log x - β * x
(k ≤ 3 → ∀ ε : ℝ, 0 < ε → err =O[atTop] fun x => x ^ ((1 : ℝ) / k + ε)) ∧
(4 ≤ k → ∀ η : ℝ, 1 / 4 ≤ η →
((fun x : ℝ => (∑ n ∈ Finset.Icc 1 ⌊x⌋₊, (n.divisors.card : ℝ)) - x * Real.log x -
(2 * Real.eulerMascheroniConstant - 1) * x) =O[atTop] fun x => x ^ η) →
∀ ε : ℝ, 0 < ε → err =O[atTop] fun x => x ^ (η + ε))
public noncomputable def bFreeIndicator (κ : ℕ → ℕ) : ArithmeticFunction ℤ :=
⟨fun n => if n ≠ 0 ∧ ∀ p : ℕ, p.Prime → ¬ p ^ κ p ∣ n then 1 else 0, by simp⟩
WantedExt/NumberTheory/WeightedDirichletConvolutionWanted.lean:35
Sources
- André Pierro de Camargo, Weighted Summation of Dirichlet Convolutions and Applications to Some Divisor Problems over k-Free and B-Free Integers, INTEGERS 24 (2024), Article A75, Corollary 1.
Uses 1
TheoremAsymptotic for the divisor function summed over \(B_\kappa\)-free integers#●ready to prove
Let \(\kappa\) be a function from the natural numbers to the natural numbers and let \(K \ge 2\) be the minimum of \(\kappa(p)\) over the primes \(p\): \(\kappa(p) \ge K\) for every prime \(p\), with equality for some prime. Let \(q_{B_\kappa}\) be the indicator of \(B_\kappa\)-free integers, \(\tau(n)\) the number of positive divisors of \(n\), \(\gamma\) the Euler–Mascheroni constant and \(\Delta(x) = \sum_{1 \le n \le x} \tau(n) - x \log x - (2\gamma - 1) x\) the Dirichlet divisor error term, and put
the product running over all primes \(p\). Then there is a real constant \(\beta_\kappa\) such that \(E(x) = \sum_{1 \le n \le x} q_{B_\kappa}(n) \tau(n) - C_\kappa x \log x - \beta_\kappa x\) satisfies the following as \(x \to \infty\). If \(K \le 3\), then \(E(x) = O(x^{1/K + \varepsilon})\) for every \(\varepsilon > 0\). If \(K \ge 4\), then for every real \(\eta \ge 1/4\) with \(\Delta(x) = O(x^\eta)\), \(E(x) = O(x^{\eta + \varepsilon})\) for every \(\varepsilon > 0\).
public theorem_wanted bFree_divisor_sum_asymptotic {κ : ℕ → ℕ} {K : ℕ} (hK : 2 ≤ K)
(hmin : ∀ p : ℕ, p.Prime → K ≤ κ p) (hatt : ∃ p : ℕ, p.Prime ∧ κ p = K) :
∃ β : ℝ,
let err : ℝ → ℝ := fun x =>
(∑ n ∈ Finset.Icc 1 ⌊x⌋₊, (bFreeIndicator κ n : ℝ) * n.divisors.card) -
(∏' p : Nat.Primes, (1 - (κ p + 1) / (p : ℝ) ^ κ p + κ p / (p : ℝ) ^ (κ p + 1))) *
x * Real.log x - β * x
(K ≤ 3 → ∀ ε : ℝ, 0 < ε → err =O[atTop] fun x => x ^ ((1 : ℝ) / K + ε)) ∧
(4 ≤ K → ∀ η : ℝ, 1 / 4 ≤ η →
((fun x : ℝ => (∑ n ∈ Finset.Icc 1 ⌊x⌋₊, (n.divisors.card : ℝ)) - x * Real.log x -
(2 * Real.eulerMascheroniConstant - 1) * x) =O[atTop] fun x => x ^ η) →
∀ ε : ℝ, 0 < ε → err =O[atTop] fun x => x ^ (η + ε))
public noncomputable def bFreeIndicator (κ : ℕ → ℕ) : ArithmeticFunction ℤ :=
⟨fun n => if n ≠ 0 ∧ ∀ p : ℕ, p.Prime → ¬ p ^ κ p ∣ n then 1 else 0, by simp⟩
WantedExt/NumberTheory/WeightedDirichletConvolutionWanted.lean:35
Sources
- André Pierro de Camargo, Weighted Summation of Dirichlet Convolutions and Applications to Some Divisor Problems over k-Free and B-Free Integers, INTEGERS 24 (2024), Article A75, Corollary 2.
Uses 1
TheoremAsymptotic for the divisor function summed over \(B_\kappa\)-free integers in a progression#●ready to prove
Let \(\kappa\) be a function from the natural numbers to the natural numbers and let \(K\) be the minimum of \(\kappa(p)\) over the primes \(p\): \(\kappa(p) \ge K\) for every prime \(p\), with equality for some prime. Assume \(K \ge 2\) and \(K \ne 3\). Let \(a\) and \(\xi\) be natural numbers with \(a < \xi\) and \(\gcd(a, \xi) = 1\). Let \(q_{B_\kappa}\) be the indicator of \(B_\kappa\)-free integers, \(\tau(n)\) the number of positive divisors of \(n\) and \(\varphi\) Euler's totient function, and put
the product running over the primes \(p\) that do not divide \(\xi\). Let \(\eta = 1/2\) if \(K = 2\) and \(\eta = 1/3\) if \(K \ge 4\). Then there is a real constant \(\tilde c\) such that for every \(\varepsilon > 0\), as \(x \to \infty\),
The case \(K = 3\) is not covered by the paper's statement and is excluded.
public theorem_wanted bFree_divisor_sum_progression_asymptotic {κ : ℕ → ℕ} {K : ℕ} (hK : 2 ≤ K)
(hK3 : K ≠ 3) (hmin : ∀ p : ℕ, p.Prime → K ≤ κ p) (hatt : ∃ p : ℕ, p.Prime ∧ κ p = K)
{a ξ : ℕ} (haξ : a < ξ) (hcop : a.Coprime ξ) :
∃ c : ℝ, ∀ ε : ℝ, 0 < ε →
(fun x : ℝ =>
(∑ n ∈ (Finset.Icc 1 ⌊x⌋₊).filter (fun n => n % ξ = a),
(bFreeIndicator κ n : ℝ) * n.divisors.card) -
(Nat.totient ξ : ℝ) / (ξ : ℝ) ^ 2 *
(∏' p : Nat.Primes, if (p : ℕ).Coprime ξ then
(1 - (κ p + 1) / (p : ℝ) ^ κ p + κ p / (p : ℝ) ^ (κ p + 1)) else 1) *
x * Real.log x - c * x) =O[atTop]
fun x => x ^ ((if K = 2 then (1 : ℝ) / 2 else 1 / 3) + ε)
public noncomputable def bFreeIndicator (κ : ℕ → ℕ) : ArithmeticFunction ℤ :=
⟨fun n => if n ≠ 0 ∧ ∀ p : ℕ, p.Prime → ¬ p ^ κ p ∣ n then 1 else 0, by simp⟩
WantedExt/NumberTheory/WeightedDirichletConvolutionWanted.lean:35
Sources
- André Pierro de Camargo, Weighted Summation of Dirichlet Convolutions and Applications to Some Divisor Problems over k-Free and B-Free Integers, INTEGERS 24 (2024), Article A75, Corollary 3, Equation (15).
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.