Divisor problems for B-free polynomials

DefinitionDirichlet convolution over monic divisors#✓fully proved

Let \(F\) be a field. The Dirichlet convolution of functions \(\alpha\) and \(\beta\) from \(F[T]\) to \(\mathbb{C}\) is the function \(\alpha * \beta\) given at \(f \in F[T]\) by

\[(\alpha * \beta)(f) = \sum_{g \text{ monic},\ g \mid f} \alpha(g)\, \beta(f/g),\]

the sum running over the monic divisors \(g\) of \(f\).

When \(f = 0\) every monic polynomial divides \(f\); the sum is then the sum of its nonzero terms if there are finitely many, and \(0\) otherwise.

public noncomputable def monicDirichletConv {F : Type*} [Field F] (α β : F[X] → ℂ)
    (f : F[X]) : ℂ :=
  ∑ᶠ g ∈ {g : F[X] | g.Monic ∧ g ∣ f}, α g * β (f /ₘ g)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 3, definition of the Dirichlet convolution.
Used by 13
Used byPartial sums of a Dirichlet convolution over monic polynomials · \(D(\alpha, \beta)\) vanishes at negative arguments · The partial sum \(D(\alpha, \beta)(0)\) · Shifted partial sums of a Dirichlet convolution · Shifted partial sums vanish below \(\deg f\) · Convolution of the \(B_\kappa\)-free indicator with the Möbius function · Dirichlet convolution of completely multiplicative functions at a product · Dirichlet convolution at \(1\) · Summatory divisor function for monic polynomials over a finite field · Weighted convolution sum · Camargo's identity over \(F(T)\) · Weighted convolution sums as sums of shifted sums · The weighted convolution sum at degree zero

TheoremDirichlet convolution at \(1\)#✓fully proved

Let \(F\) be a field and let \(\alpha\) and \(\beta\) be functions from \(F[T]\) to \(\mathbb{C}\). Their Dirichlet convolution over monic divisors satisfies \((\alpha * \beta)(1) = \alpha(1) \beta(1)\), since the only monic divisor of \(1\) is \(1\).

public theorem monicDirichletConv_one {F : Type*} [Field F] (α β : F[X] → ℂ) :
    monicDirichletConv α β 1 = α 1 * β 1
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 3, definition of the Dirichlet convolution.
Uses 1 · Used by 2
Statement usesDirichlet convolution over monic divisors
Used byThe partial sum \(D(\alpha, \beta)(0)\) · The weighted convolution sum at degree zero

TheoremPerron's formula for monic polynomials over a finite field#●ready to prove

Let \(F\) be a finite field, let \(a\) be a complex-valued function on \(F[T]\), and let \(\rho\) be a real number with \(0 < \rho < 1\) such that the series \(\sum_f |a(f)| \rho^{\deg f}\) over all monic \(f \in F[T]\) converges. Put \(A(u) = \sum_f a(f) u^{\deg f}\), the sum again over all monic \(f\). Then for every natural number \(n\), with the circle \(|u| = \rho\) traversed counterclockwise,

\[\sum_{f \text{ monic},\ \deg f \le n} a(f) = \frac{1}{2 \pi i} \oint_{|u| = \rho} \frac{A(u)}{u^n (1 - u)} \, \frac{du}{u}.\]
public theorem_wanted monic_perron_formula {F : Type*} [Field F] [Finite F]
    (a : F[X] → ℂ) {ρ : ℝ} (hρ0 : 0 < ρ) (hρ1 : ρ < 1)
    (habs : Summable fun f : {f : F[X] // f.Monic} => ‖a f‖ * ρ ^ (f : F[X]).natDegree)
    (n : ℕ) :
    ∑ᶠ f ∈ {f : F[X] | f.Monic ∧ f.natDegree ≤ n}, a f =
      (2 * Real.pi * Complex.I)⁻¹ •
        ∮ u in C(0, ρ),
          (∑' f : {f : F[X] // f.Monic}, a f * u ^ (f : F[X]).natDegree) /
            (u ^ n * (1 - u)) * u⁻¹
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Lemma 1 (Perron's Formula).

TheoremDirichlet convolution of completely multiplicative functions at a product#●ready to prove

Let \(F\) be a field and let \(\alpha, \beta : F[T] \to \mathbb{C}\) be completely multiplicative, that is, monoid homomorphisms from the multiplicative monoid of \(F[T]\) to \(\mathbb{C}\). Write \(\gamma = \alpha * \beta\) for their Dirichlet convolution over monic divisors and \(\mu\) for the Möbius function. Then for all monic \(f, g \in F[T]\),

\[\gamma(fg) = \sum_{\ell} \mu(\ell) \alpha(\ell) \beta(\ell) \gamma(f/\ell) \gamma(g/\ell),\]

where \(\ell\) runs over the monic common divisors of \(f\) and \(g\).

Every completely multiplicative function on monic polynomials extends to such a homomorphism (send nonzero constants to \(1\) and \(0\) to \(0\)), and only values at monic polynomials enter.

public theorem_wanted monicDirichletConv_mul_of_completelyMultiplicative {F : Type*} [Field F]
    (α β : F[X] →* ℂ) {f g : F[X]} (hf : f.Monic) (hg : g.Monic) :
    monicDirichletConv α β (f * g) =
      ∑ᶠ ℓ ∈ {ℓ : F[X] | ℓ.Monic ∧ ℓ ∣ f ∧ ℓ ∣ g},
        (moebius ℓ : ℂ) * α ℓ * β ℓ * monicDirichletConv α β (f /ₘ ℓ) *
          monicDirichletConv α β (g /ₘ ℓ)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Lemma 2.
Uses 1
Statement usesDirichlet convolution over monic divisors

TheoremMöbius sum over the monic divisors of a polynomial over a finite field#●ready to prove

Let \(F\) be a finite field with \(q\) elements and let \(\mu\) be the Möbius function of \(F[T]\). For every monic \(f \in F[T]\),

\[\sum_{g \text{ monic},\ g \mid f} \frac{\mu(g)}{q^{\deg g}} = \prod_{P \text{ monic irreducible},\ P \mid f} \left(1 - \frac{1}{q^{\deg P}}\right).\]

The right side is \(\Phi(f) / q^{\deg f}\), where \(\Phi\) is Euler's totient function on \(F[T]\).

public theorem_wanted monic_sum_moebius_div_norm {F : Type*} [Field F] [Fintype F] {f : F[X]}
    (hf : f.Monic) :
    ∑ᶠ g ∈ {g : F[X] | g.Monic ∧ g ∣ f},
        (moebius g : ℝ) / (Fintype.card F : ℝ) ^ g.natDegree =
      ∏ᶠ P ∈ {P : F[X] | P.Monic ∧ Irreducible P ∧ P ∣ f},
        (1 - 1 / (Fintype.card F : ℝ) ^ P.natDegree)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Lemma 6; Φ as defined after Theorem 3.

TheoremDegree-weighted Möbius sum over the monic divisors of a polynomial over a finite field#●ready to prove

Let \(F\) be a finite field with \(q\) elements and let \(\mu\) be the Möbius function of \(F[T]\). For every monic \(f \in F[T]\),

\[\sum_{g \text{ monic},\ g \mid f} \frac{\mu(g) \deg g}{q^{\deg g}} = \prod_{P \mid f} \left(1 - \frac{1}{q^{\deg P}}\right) \sum_{P \mid f} \frac{\deg P}{1 - q^{\deg P}},\]

where in the product and in the sum \(P\) runs over the monic irreducible divisors of \(f\).

The product is \(\Phi(f) / q^{\deg f}\), where \(\Phi\) is Euler's totient function on \(F[T]\).

public theorem_wanted monic_sum_moebius_mul_natDegree_div_norm {F : Type*} [Field F] [Fintype F]
    {f : F[X]} (hf : f.Monic) :
    ∑ᶠ g ∈ {g : F[X] | g.Monic ∧ g ∣ f},
        (moebius g : ℝ) * g.natDegree / (Fintype.card F : ℝ) ^ g.natDegree =
      (∏ᶠ P ∈ {P : F[X] | P.Monic ∧ Irreducible P ∧ P ∣ f},
          (1 - 1 / (Fintype.card F : ℝ) ^ P.natDegree)) *
        ∑ᶠ P ∈ {P : F[X] | P.Monic ∧ Irreducible P ∧ P ∣ f},
          (P.natDegree : ℝ) / (1 - (Fintype.card F : ℝ) ^ P.natDegree)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Lemma 7; Φ as defined after Theorem 3.

TheoremNumber of monic polynomials of bounded degree#●ready to prove

Let \(F\) be a finite field with \(q\) elements and let \(N\) be a natural number. The number of monic polynomials in \(F[T]\) of degree at most \(N\) is \((q^{N+1} - 1)/(q - 1)\).

public theorem_wanted monic_count_natDegree_le {F : Type*} [Field F] [Fintype F] (N : ℕ) :
    (Nat.card {f : F[X] // f.Monic ∧ f.natDegree ≤ N} : ℚ) =
      ((Fintype.card F : ℚ) ^ (N + 1) - 1) / (Fintype.card F - 1)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Proposition 4, case h = 1, m = 1.

TheoremSummatory divisor function for monic polynomials over a finite field#●ready to prove

Let \(F\) be a finite field with \(q\) elements. For monic \(f \in F[T]\), the Dirichlet convolution \((1 * 1)(f)\) of the constant function \(1\) with itself is the number of monic divisors of \(f\). Then for every natural number \(N\),

\[\sum_{f \text{ monic},\ \deg f \le N} (1 * 1)(f) = \frac{(N + 1) q^{N + 2} - (N + 2) q^{N + 1} + 1}{(q - 1)^2}.\]
public theorem_wanted monic_sum_divisorCount_natDegree_le {F : Type*} [Field F] [Fintype F]
    (N : ℕ) :
    ∑ᶠ f ∈ {f : F[X] | f.Monic ∧ f.natDegree ≤ N},
        monicDirichletConv (fun _ => (1 : ℂ)) (fun _ => 1) f =
      (((N + 1 : ℂ) * (Fintype.card F : ℂ) ^ (N + 2) - (N + 2) * (Fintype.card F : ℂ) ^ (N + 1)
          + 1) / ((Fintype.card F : ℂ) - 1) ^ 2)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Proposition 4, case h = 2, m = 1.
Uses 1
Statement usesDirichlet convolution over monic divisors

DefinitionNorm of a polynomial over a finite field#✓fully proved

Let \(F\) be a finite field with \(q\) elements. The norm of a nonzero \(f \in F[T]\) is the real number \(|f| = q^{\deg f}\), and \(|0| = 0\).

public noncomputable def fqNorm {F : Type*} [Field F] [Fintype F] (f : F[X]) : ℝ :=
  open scoped Classical in
  if f = 0 then 0 else (Fintype.card F : ℝ) ^ f.natDegree
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 1, definition of the norm.
Used by 13
Used byAsymptotic for B-free divisor sums when h is at most 2 · Asymptotic for B-free divisor sums in progressions when h is at most 2 · Asymptotic count of B-free polynomials in an arithmetic progression · Asymptotic for the B-free divisor function in an arithmetic progression · Asymptotic count of B-free polynomials · B-free polynomials in short intervals · The B-free divisor function in short intervals · Asymptotic for the \(B_\kappa\)-free sum of the divisor function · Multiplicativity of the norm · The norm of a nonzero polynomial · Euler-product asymptotic with the \((h-1)\)-divisor function over \(\kappa\)-th powers · Euler-product asymptotic for a degree-weighted Möbius sum over \(\kappa\)-th powers · Euler-product asymptotic for a Möbius sum weighted by \(\deg r^\kappa\)

TheoremThe norm of a nonzero polynomial#✓fully proved

Let \(F\) be a finite field with \(q\) elements. For every nonzero \(f \in F[T]\), the norm of \(f\) is \(|f| = q^{\deg f}\).

public theorem fqNorm_of_ne_zero {F : Type*} [Field F] [Fintype F] {f : F[X]} (hf : f ≠ 0) :
    fqNorm f = (Fintype.card F : ℝ) ^ f.natDegree
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 1, definition of the norm.
Uses 1 · Used by 1
Statement usesNorm of a polynomial over a finite field
Used byMultiplicativity of the norm

TheoremMultiplicativity of the norm#✓fully proved

Let \(F\) be a finite field with \(q\) elements, and let \(|f| = q^{\deg f}\) be the norm of a nonzero \(f \in F[T]\). For all nonzero \(f, g \in F[T]\), \(|fg| = |f| \, |g|\).

public theorem fqNorm_mul {F : Type*} [Field F] [Fintype F] {f g : F[X]} (hf : f ≠ 0)
    (hg : g ≠ 0) : fqNorm (f * g) = fqNorm f * fqNorm g
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 1, definition of the norm.
Uses 2
Statement usesNorm of a polynomial over a finite field
Proof usesThe norm of a nonzero polynomial

TheoremMonic polynomials of degree zero#✓fully proved

Let \(F\) be a field. A polynomial \(f \in F[T]\) is monic of degree at most \(0\) if and only if \(f = 1\).

public theorem monic_natDegree_le_zero_iff {F : Type*} [Field F] {f : F[X]} :
    f.Monic ∧ f.natDegree ≤ 0 ↔ f = 1
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 2, the set M_{≤ 0}.
Used by 3
Used byThe \(B_\kappa\)-free divisor sum at degree zero · The partial sum \(D(\alpha, \beta)(0)\) · The weighted convolution sum at degree zero

Definition\(B_\kappa\)-free polynomials#✓fully proved

Let \(F\) be a field and let \(\kappa\) assign a natural number to each polynomial in \(F[T]\). A polynomial \(f \in F[T]\) is \(B_\kappa\)-free when \(P^{\kappa(P)}\) does not divide \(f\) for any monic irreducible \(P \in F[T]\).

public def IsBFree {F : Type*} [Field F] (κ : F[X] → ℕ) (f : F[X]) : Prop :=
  ∀ P : F[X], P.Monic → Irreducible P → ¬ P ^ κ P ∣ f
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 1, definition of B_κ-free polynomials.
Used by 9
Used byThe \(B_\kappa\)-free divisor sum · B-free divisor sum in an arithmetic progression · The progression sum modulo 1 is the full sum · Divisor sums over \(B_\kappa\)-free polynomials in short intervals · B-free polynomials in short intervals · The B-free divisor function in short intervals · The \(B_\kappa\)-free divisor sum at degree zero · The polynomial \(1\) is \(B_\kappa\)-free · Convolution of the \(B_\kappa\)-free indicator with the Möbius function

TheoremThe polynomial \(1\) is \(B_\kappa\)-free#✓fully proved

Let \(F\) be a field and let \(\kappa\) assign to each polynomial in \(F[T]\) a natural number, with \(\kappa(P) \ne 0\) for every monic irreducible \(P\). Then \(1\) is \(B_\kappa\)-free: \(P^{\kappa(P)}\) does not divide \(1\) for any monic irreducible \(P\).

public theorem isBFree_one {F : Type*} [Field F] (κ : F[X] → ℕ)
    (hκ : ∀ P : F[X], P.Monic → Irreducible P → κ P ≠ 0) : IsBFree κ (1 : F[X])
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 1, definition of B_κ-free polynomials.
Uses 1 · Used by 1
Statement uses\(B_\kappa\)-free polynomials
Used byThe \(B_\kappa\)-free divisor sum at degree zero

DefinitionThe minimal exponent \(\kappa_{\min}\)#✓fully proved

Let \(F\) be a field and let \(\kappa\) be a function from \(F[T]\) to the natural numbers. Then \(\kappa_{\min}\) is the minimum of \(\kappa(P)\) over all monic irreducible polynomials \(P \in F[T]\).

public noncomputable def kappaMin {F : Type*} [Field F] (κ : F[X] → ℕ) : ℕ :=
  ⨅ P : {P : F[X] // P.Monic ∧ Irreducible P}, κ P
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 1, definition of κ_min.
Used by 13
Used byBound on the Möbius sum over κ-th powers · Asymptotic count of B-free polynomials in an arithmetic progression · Asymptotic for the B-free divisor function in an arithmetic progression · Asymptotic count of B-free polynomials · Divisor sums over \(B_\kappa\)-free polynomials in short intervals · B-free polynomials in short intervals · The B-free divisor function in short intervals · Asymptotic for the \(B_\kappa\)-free sum of the divisor function · \(\kappa_{\min}\) is a lower bound for \(\kappa\) · Divisor-count bound over \(\kappa\)-th powers of monic polynomials · Euler-product asymptotic with the \((h-1)\)-divisor function over \(\kappa\)-th powers · Euler-product asymptotic for a degree-weighted Möbius sum over \(\kappa\)-th powers · Euler-product asymptotic for a Möbius sum weighted by \(\deg r^\kappa\)

Theorem\(\kappa_{\min}\) is a lower bound for \(\kappa\)#✓fully proved

Let \(F\) be a field, let \(\kappa\) assign a natural number to each polynomial in \(F[T]\), and let \(\kappa_{\min}\) be the minimum of \(\kappa(P)\) over the monic irreducible \(P \in F[T]\). Then \(\kappa_{\min} \le \kappa(P)\) for every monic irreducible \(P \in F[T]\).

public theorem kappaMin_le {F : Type*} [Field F] (κ : F[X] → ℕ) {P : F[X]} (hm : P.Monic)
    (hP : Irreducible P) : kappaMin κ ≤ κ P
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 1, definition of κ_min.
Uses 1
Statement usesThe minimal exponent \(\kappa_{\min}\)

DefinitionThe \(\kappa\)-power of a polynomial#✓fully proved

Let \(F\) be a field and let \(\kappa\) be a function from \(F[T]\) to the natural numbers. For nonzero \(f \in F[T]\) and a monic irreducible \(P\), write \(\nu_P(f)\) for the multiplicity of \(P\) in \(f\). The \(\kappa\)-power of \(f\) is \(f^\kappa = \prod_P P^{\nu_P(f)\, \kappa(P)}\), the product over the monic irreducible \(P\) dividing \(f\); it does not depend on the leading coefficient of \(f\). For \(f = 0\) the product is empty and \(0^\kappa = 1\).

public noncomputable def kappaPow {F : Type*} [Field F] (κ : F[X] → ℕ) (f : F[X]) : F[X] :=
  open scoped Classical in
  ((normalizedFactors f).map fun P => P ^ κ P).prod
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 3, definition of f ^ κ.
Used by 8
Used byBound on the Möbius sum over κ-th powers · The \(\kappa\)-power of a monic irreducible polynomial · The \(\kappa\)-power of \(1\) · Convolution of the \(B_\kappa\)-free indicator with the Möbius function · Divisor-count bound over \(\kappa\)-th powers of monic polynomials · Euler-product asymptotic with the \((h-1)\)-divisor function over \(\kappa\)-th powers · Euler-product asymptotic for a degree-weighted Möbius sum over \(\kappa\)-th powers · Euler-product asymptotic for a Möbius sum weighted by \(\deg r^\kappa\)

TheoremThe \(\kappa\)-power of \(1\)#✓fully proved

Let \(F\) be a field and let \(\kappa\) be a function from \(F[T]\) to the natural numbers. Then the \(\kappa\)-power of the constant polynomial \(1\) is \(1^\kappa = 1\).

public theorem kappaPow_one {F : Type*} [Field F] (κ : F[X] → ℕ) :
    kappaPow κ (1 : F[X]) = 1
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 3, definition of f ^ κ.
Uses 1
Statement usesThe \(\kappa\)-power of a polynomial

TheoremThe \(\kappa\)-power of a monic irreducible polynomial#✓fully proved

Let \(F\) be a field and let \(\kappa\) be a function from \(F[T]\) to the natural numbers. For every monic irreducible \(P \in F[T]\), the \(\kappa\)-power of \(P\) is \(P^\kappa = P^{\kappa(P)}\).

public theorem kappaPow_of_irreducible {F : Type*} [Field F] (κ : F[X] → ℕ) {P : F[X]}
    (hm : P.Monic) (hP : Irreducible P) : kappaPow κ P = P ^ κ P
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 3, definition of f ^ κ.
Uses 1
Statement usesThe \(\kappa\)-power of a polynomial

DefinitionThe \(h\)-fold divisor function#✓fully proved

Let \(F\) be a field and \(h\) a natural number. For \(f \in F[T]\), \(d_h(f)\) is the number of \(h\)-tuples \((g_1, \dots, g_h)\) of monic polynomials in \(F[T]\) with \(g_1 \cdots g_h = f\).

public noncomputable def monicDivisorCount {F : Type*} [Field F] (h : ℕ) (f : F[X]) : ℕ :=
  Nat.card {v : Fin h → F[X] // (∀ i, (v i).Monic) ∧ ∏ i, v i = f}
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 1, definition of d_h.
Used by 12
Used byThe \(B_\kappa\)-free divisor sum · B-free divisor sum in an arithmetic progression · The progression sum modulo 1 is the full sum · Divisor sums over \(B_\kappa\)-free polynomials in short intervals · B-free polynomials in short intervals · The B-free divisor function in short intervals · The \(B_\kappa\)-free divisor sum at degree zero · The divisor functions at \(1\) · The divisor function \(d_1\) on monic polynomials · The divisor function \(d_0\) vanishes away from \(1\) · Character sums of the \(h\)-divisor function over monic polynomials · Euler-product asymptotic with the \((h-1)\)-divisor function over \(\kappa\)-th powers

TheoremThe divisor functions at \(1\)#✓fully proved

Let \(F\) be a field and \(h\) a natural number. Then \(d_h(1) = 1\), where \(d_h(f)\) is the number of \(h\)-tuples of monic polynomials in \(F[T]\) whose product is \(f\): the only such tuple for \(f = 1\) has every entry equal to \(1\).

public theorem monicDivisorCount_one {F : Type*} [Field F] (h : ℕ) :
    monicDivisorCount h (1 : F[X]) = 1
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 1, definition of d_h.
Uses 1 · Used by 1
Statement usesThe \(h\)-fold divisor function
Used byThe \(B_\kappa\)-free divisor sum at degree zero

TheoremThe divisor function \(d_0\) vanishes away from \(1\)#✓fully proved

Let \(F\) be a field and let \(f \in F[T]\) with \(f \ne 1\). Then \(d_0(f) = 0\), where \(d_h(f)\) is the number of \(h\)-tuples of monic polynomials in \(F[T]\) whose product is \(f\): the only \(0\)-tuple is the empty one, whose product is \(1\).

public theorem monicDivisorCount_zero_of_ne_one {F : Type*} [Field F] {f : F[X]} (hf : f ≠ 1) :
    monicDivisorCount 0 f = 0
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 1, definition of d_h.
Uses 1
Statement usesThe \(h\)-fold divisor function

TheoremThe divisor function \(d_1\) on monic polynomials#✓fully proved

Let \(F\) be a field. For every monic \(f \in F[T]\), \(d_1(f) = 1\), where \(d_h(f)\) is the number of \(h\)-tuples of monic polynomials in \(F[T]\) whose product is \(f\).

public theorem monicDivisorCount_one_left {F : Type*} [Field F] {f : F[X]} (hf : f.Monic) :
    monicDivisorCount 1 f = 1
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 1, definition of d_h.
Uses 1
Statement usesThe \(h\)-fold divisor function

DefinitionShifted partial sums of a Dirichlet convolution#✓fully proved

Let \(F\) be a field, let \(\alpha, \beta \colon F[T] \to \mathbb{C}\), let \(\alpha * \beta\) be their Dirichlet convolution over monic divisors, let \(f \in F[T]\) and let \(n\) be a natural number. Then \(S_f[\alpha, \beta](n) = \sum_g (\alpha * \beta)(fg)\), the sum over the monic \(g \in F[T]\) with \(\deg f + \deg g \le n\), where \(\deg 0 = 0\). This is the paper's sum over \(g\) of degree at most \(n - \deg f\).

The sum is a finitary sum: it is \(0\) when infinitely many of its terms are nonzero, which can happen only for infinite \(F\).

public noncomputable def monicConvShiftedSum {F : Type*} [Field F] (α β : F[X] → ℂ)
    (f : F[X]) (n : ℕ) : ℂ :=
  ∑ᶠ g ∈ {g : F[X] | g.Monic ∧ f.natDegree + g.natDegree ≤ n}, monicDirichletConv α β (f * g)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 3, eq. (3).
Uses 1 · Used by 3
Statement usesDirichlet convolution over monic divisors
Used byShifted partial sums for completely multiplicative functions · Shifted partial sums vanish below \(\deg f\) · Weighted convolution sums as sums of shifted sums

TheoremShifted partial sums vanish below \(\deg f\)#✓fully proved

Let \(F\) be a field, let \(\alpha, \beta \colon F[T] \to \mathbb{C}\) and let \(f \in F[T]\). For every natural number \(n < \deg f\), the shifted partial sum of the Dirichlet convolution satisfies \(S_f[\alpha, \beta](n) = 0\).

public theorem monicConvShiftedSum_of_lt {F : Type*} [Field F] (α β : F[X] → ℂ) {f : F[X]}
    {n : ℕ} (hn : n < f.natDegree) : monicConvShiftedSum α β f n = 0
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 3, eq. (3).
Uses 2
Statement usesShifted partial sums of a Dirichlet convolution
Proof usesDirichlet convolution over monic divisors

DefinitionPartial sums of a Dirichlet convolution over monic polynomials#✓fully proved

Let \(F\) be a field, let \(\alpha, \beta \colon F[T] \to \mathbb{C}\), and let \(\alpha * \beta\) be their Dirichlet convolution over monic divisors. For an integer \(n\), \(D[\alpha, \beta](n) = \sum_g (\alpha * \beta)(g)\), the sum over the monic \(g \in F[T]\) of degree at most \(n\). For \(n < 0\) the sum is empty, so \(D[\alpha, \beta](n) = 0\); this is how the paper's Lemma 3 uses \(D\) at \(n - \deg(f \ell)\).

The sum is a finitary sum: it is \(0\) when infinitely many of its terms are nonzero, which can happen only for infinite \(F\).

public noncomputable def monicConvPartialSum {F : Type*} [Field F] (α β : F[X] → ℂ) (n : ℤ) : ℂ :=
  ∑ᶠ g ∈ {g : F[X] | g.Monic ∧ (g.natDegree : ℤ) ≤ n}, monicDirichletConv α β g
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 3, definition of D[α, β](n).
Uses 1 · Used by 4
Statement usesDirichlet convolution over monic divisors
Used by\(D(\alpha, \beta)\) vanishes at negative arguments · The partial sum \(D(\alpha, \beta)(0)\) · Shifted partial sums for completely multiplicative functions · Camargo's identity over \(F(T)\)

Theorem\(D(\alpha, \beta)\) vanishes at negative arguments#✓fully proved

Let \(F\) be a field and let \(\alpha, \beta \colon F[T] \to \mathbb{C}\). For every integer \(n < 0\), the partial sum of the Dirichlet convolution of \(\alpha\) and \(\beta\) satisfies \(D[\alpha, \beta](n) = 0\).

public theorem monicConvPartialSum_of_neg {F : Type*} [Field F] (α β : F[X] → ℂ) {n : ℤ}
    (hn : n < 0) : monicConvPartialSum α β n = 0
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 3, definition of D[α, β](n).
Uses 2
Statement usesPartial sums of a Dirichlet convolution over monic polynomials
Proof usesDirichlet convolution over monic divisors

TheoremThe partial sum \(D(\alpha, \beta)(0)\)#✓fully proved

Let \(F\) be a field and let \(\alpha, \beta \colon F[T] \to \mathbb{C}\). The partial sum of the Dirichlet convolution of \(\alpha\) and \(\beta\) at \(0\) is \(D[\alpha, \beta](0) = \alpha(1)\, \beta(1)\).

public theorem monicConvPartialSum_zero {F : Type*} [Field F] (α β : F[X] → ℂ) :
    monicConvPartialSum α β 0 = α 1 * β 1
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 3, definition of D[α, β](n).
Uses 4
Statement usesPartial sums of a Dirichlet convolution over monic polynomials
Proof usesDirichlet convolution over monic divisors · Dirichlet convolution at \(1\) · Monic polynomials of degree zero

DefinitionWeighted convolution sum#✓fully proved

Let \(F\) be a field, let \(\gamma, \alpha, \beta\) be functions from \(F[T]\) to \(\mathbb{C}\), and write \(\alpha * \beta\) for the monic Dirichlet convolution of \(\alpha\) and \(\beta\). For a natural number \(n\), let \(M_{\le n}\) be the set of monic polynomials in \(F[T]\) of degree at most \(n\). The weighted convolution sum is

\[D(\gamma, \alpha, \beta; n) = \sum_{f \in M_{\le n}} \gamma(f)\,(\alpha * \beta)(f).\]

When \(F\) is infinite and this sum has infinitely many nonzero terms, its value is taken to be \(0\).

public noncomputable def weightedMonicConvSum {F : Type*} [Field F] (γ α β : F[X] → ℂ)
    (n : ℕ) : ℂ :=
  ∑ᶠ f ∈ {f : F[X] | f.Monic ∧ f.natDegree ≤ n}, γ f * monicDirichletConv α β f
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 3, definition of D[γ, α, β](n).
Uses 1 · Used by 3
Statement usesDirichlet convolution over monic divisors
Used byCamargo's identity over \(F(T)\) · Weighted convolution sums as sums of shifted sums · The weighted convolution sum at degree zero

TheoremThe weighted convolution sum at degree zero#✓fully proved

Let \(F\) be a field and let \(\gamma, \alpha, \beta\) be functions from \(F[T]\) to \(\mathbb{C}\), and write \(\alpha * \beta\) for the monic Dirichlet convolution. The weighted convolution sum \(D(\gamma, \alpha, \beta; 0)\), the sum of \(\gamma(f)\,(\alpha * \beta)(f)\) over the monic \(f \in F[T]\) of degree at most \(0\), equals \(\gamma(1)\,\alpha(1)\,\beta(1)\).

public theorem weightedMonicConvSum_zero {F : Type*} [Field F] (γ α β : F[X] → ℂ) :
    weightedMonicConvSum γ α β 0 = γ 1 * (α 1 * β 1)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 3, definition of D[γ, α, β](n).
Uses 4
Statement usesWeighted convolution sum
Proof usesDirichlet convolution over monic divisors · Dirichlet convolution at \(1\) · Monic polynomials of degree zero

TheoremShifted partial sums for completely multiplicative functions#●ready to prove

Let \(F\) be a finite field and let \(\alpha, \beta \colon F[T] \to \mathbb{C}\) be completely multiplicative, that is, monoid homomorphisms from the multiplicative monoid of \(F[T]\) to \(\mathbb{C}\). Write \(\mu\) for the Möbius function of \(F[T]\). For \(f \in F[T]\), a natural number \(n\) and an integer \(k\), write \(S_f[\alpha, \beta](n)\) and \(D[\alpha, \beta](k)\) for the shifted partial sums and the partial sums of the Dirichlet convolution of \(\alpha\) and \(\beta\) over monic divisors, where \(D[\alpha, \beta](k) = 0\) for \(k < 0\). Then for every monic \(f \in F[T]\) and every natural number \(n\),

\[S_f[\alpha, \beta](n) = \sum_{d \mid f} \alpha(d)\, \beta(f/d) \sum_{\ell \mid d} \mu(\ell)\, \beta(\ell)\, D[\alpha, \beta](n - \deg(f \ell)),\]

where \(d\) runs over the monic divisors of \(f\), \(\ell\) over the monic divisors of \(d\), and \(n - \deg(f \ell)\) is computed in the integers.

The paper states this for every \(f \in F[T]\), monic or not; its proof applies Lemma 2, which needs \(f\) monic.

public theorem_wanted monicConvShiftedSum_eq_of_completelyMultiplicative {F : Type*} [Field F]
    [Finite F] (α β : F[X] →* ℂ) {f : F[X]} (hf : f.Monic) (n : ℕ) :
    monicConvShiftedSum α β f n =
      ∑ᶠ d ∈ {d : F[X] | d.Monic ∧ d ∣ f}, α d * β (f /ₘ d) *
        ∑ᶠ ℓ ∈ {ℓ : F[X] | ℓ.Monic ∧ ℓ ∣ d},
          (moebius ℓ : ℂ) * β ℓ * monicConvPartialSum α β ((n : ℤ) - (f * ℓ).natDegree)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Lemma 3.
Uses 2
Statement usesPartial sums of a Dirichlet convolution over monic polynomials · Shifted partial sums of a Dirichlet convolution

TheoremWeighted convolution sums as sums of shifted sums#●ready to prove

Let \(F\) be a finite field and let \(\gamma, \alpha, \beta\) be functions from \(F[T]\) to \(\mathbb{C}\). Write \(\alpha * \beta\) for the monic Dirichlet convolution, \(\mu\) for the Möbius function of \(F[T]\), and \(\lambda = \gamma * \mu\). For a natural number \(n\) let \(M_{\le n}\) be the set of monic polynomials in \(F[T]\) of degree at most \(n\), let \(D(\gamma, \alpha, \beta; n) = \sum_{f \in M_{\le n}} \gamma(f)\,(\alpha * \beta)(f)\) and, for monic \(f\), let \(S_f(\alpha, \beta; n) = \sum_{g \text{ monic},\ \deg f + \deg g \le n} (\alpha * \beta)(fg)\). Then

\[D(\gamma, \alpha, \beta; n) = \sum_{f \in M_{\le n}} \lambda(f)\, S_f(\alpha, \beta; n).\]
public theorem_wanted weightedMonicConvSum_eq_sum_shifted {F : Type*} [Field F] [Finite F]
    (γ α β : F[X] → ℂ) (n : ℕ) :
    weightedMonicConvSum γ α β n =
      ∑ᶠ f ∈ {f : F[X] | f.Monic ∧ f.natDegree ≤ n},
        monicDirichletConv γ (fun g => (moebius g : ℂ)) f * monicConvShiftedSum α β f n
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Lemma 4.
Uses 3
Statement usesShifted partial sums of a Dirichlet convolution · Dirichlet convolution over monic divisors · Weighted convolution sum

TheoremCamargo's identity over \(F(T)\)#●ready to prove

Let \(F\) be a finite field and let \(\mu\) be the Möbius function of \(F[T]\). For functions \(\alpha, \beta \colon F[T] \to \mathbb{C}\) let \((\alpha * \beta)(f) = \sum_{g \mid f} \alpha(g) \beta(f/g)\), over monic divisors \(g\), be their Dirichlet convolution, and let \(D[\alpha, \beta](k)\) be the sum of \((\alpha * \beta)(g)\) over the monic \(g\) of degree at most \(k\), which is \(0\) for \(k < 0\). For a further function \(\gamma\) let \(D[\gamma, \alpha, \beta](n)\) be the sum of \(\gamma(f) (\alpha * \beta)(f)\) over the monic \(f\) of degree at most \(n\). Suppose \(\alpha\) and \(\beta\) are completely multiplicative, that is, \(\alpha(1) = 1\) and \(\alpha(f g) = \alpha(f) \alpha(g)\) for all \(f, g \in F[T]\), and likewise for \(\beta\), and let \(\gamma \colon F[T] \to \mathbb{C}\) be arbitrary. Then for every natural number \(n\),

\[D[\gamma, \alpha, \beta](n) = \sum_{f \text{ monic},\ \deg f \le n} (\gamma * \mu)(f) \sum_{d \mid f} \alpha(d) \beta(f/d) \sum_{\ell \mid d} \mu(\ell) \beta(\ell) \, D[\alpha, \beta](n - \deg(f \ell)),\]

where \(d\) runs over the monic divisors of \(f\) and \(\ell\) over the monic divisors of \(d\).

public theorem_wanted weightedMonicConvSum_eq_of_completelyMultiplicative {F : Type*} [Field F]
    [Finite F] (γ : F[X] → ℂ) (α β : F[X] →* ℂ) (n : ℕ) :
    weightedMonicConvSum γ α β n =
      ∑ᶠ f ∈ {f : F[X] | f.Monic ∧ f.natDegree ≤ n},
        monicDirichletConv γ (fun g => (moebius g : ℂ)) f *
          ∑ᶠ d ∈ {d : F[X] | d.Monic ∧ d ∣ f}, α d * β (f /ₘ d) *
            ∑ᶠ ℓ ∈ {ℓ : F[X] | ℓ.Monic ∧ ℓ ∣ d},
              (moebius ℓ : ℂ) * β ℓ * monicConvPartialSum α β ((n : ℤ) - (f * ℓ).natDegree)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Theorem 6.
Uses 3
Statement usesPartial sums of a Dirichlet convolution over monic polynomials · Dirichlet convolution over monic divisors · Weighted convolution sum

TheoremConvolution of the \(B_\kappa\)-free indicator with the Möbius function#●ready to prove

Let \(F\) be a field and let \(\kappa\) assign a natural number to each polynomial in \(F[T]\), with \(\kappa(P) \ne 0\) for every monic irreducible \(P \in F[T]\). Let \(\mathbf{1}_{B_\kappa} \colon F[T] \to \mathbb{C}\) be the indicator function of the \(B_\kappa\)-free polynomials, let \(\mu\) be the Möbius function of \(F[T]\), and write \(r^\kappa\) for the \(\kappa\)-power of a polynomial \(r\). Then for every monic \(f \in F[T]\), the Dirichlet convolution of \(\mathbf{1}_{B_\kappa}\) and \(\mu\) over monic divisors satisfies

\[(\mathbf{1}_{B_\kappa} * \mu)(f) = \sum_{r} \mu(r),\]

the sum running over the monic \(r \in F[T]\) with \(r^\kappa = f\).

There is at most one such \(r\), so the right side is \(\mu(r)\) if \(f = r^\kappa\) for a monic \(r\), and \(0\) if there is no such \(r\).

public theorem_wanted monicDirichletConv_bFreeIndicator_moebius {F : Type*} [Field F]
    (κ : F[X] → ℕ) (hκ : ∀ P : F[X], P.Monic → Irreducible P → κ P ≠ 0) {f : F[X]}
    (hf : f.Monic) :
    monicDirichletConv ({g : F[X] | IsBFree κ g}.indicator 1) (fun g => (moebius g : ℂ)) f =
      ∑ᶠ r ∈ {r : F[X] | r.Monic ∧ kappaPow κ r = f}, (moebius r : ℂ)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Lemma 5.
Uses 3
Statement uses\(B_\kappa\)-free polynomials · The \(\kappa\)-power of a polynomial · Dirichlet convolution over monic divisors

TheoremBound on the Möbius sum over κ-th powers#●ready to prove

Let \(F\) be a finite field with \(q\) elements and let \(\kappa\) assign a natural number to each polynomial in \(F[T]\), with \(\kappa(P) \ge 2\) for every monic irreducible \(P\). Let \(\kappa_{\min}\) be the minimum of \(\kappa(P)\) over the monic irreducible \(P\), and for monic \(r = \prod_P P^{\nu_P}\) write \(r^\kappa = \prod_P P^{\nu_P \kappa(P)}\). Then for every natural number \(N \ge 1\),

\[ \Bigl|\sum_{r} \mu(r) \sum_{f \mid r^\kappa} \sum_{\ell \mid f} \mu(\ell)\Bigr| \le q^{N/\kappa_{\min}}, \]

where \(r\) runs over the monic polynomials with \(\deg r^\kappa \le N\), \(f\) and \(\ell\) run over monic divisors, \(\mu\) is the Möbius function, and the exponent \(N/\kappa_{\min}\) is a real number.

public theorem_wanted abs_sum_moebius_kappaPow_le {F : Type*} [Field F] [Fintype F]
    (κ : F[X] → ℕ) (hκ : ∀ P : F[X], P.Monic → Irreducible P → 2 ≤ κ P) {N : ℕ} (hN : 1 ≤ N) :
    |∑ᶠ r ∈ {r : F[X] | r.Monic ∧ (kappaPow κ r).natDegree ≤ N},
        (moebius r : ℝ) * ∑ᶠ f ∈ {f : F[X] | f.Monic ∧ f ∣ kappaPow κ r},
          ∑ᶠ ℓ ∈ {ℓ : F[X] | ℓ.Monic ∧ ℓ ∣ f}, (moebius ℓ : ℝ)| ≤
      (Fintype.card F : ℝ) ^ ((N : ℝ) / kappaMin κ)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Lemma 8, eq. (6).
Uses 2
Statement usesThe minimal exponent \(\kappa_{\min}\) · The \(\kappa\)-power of a polynomial

TheoremDivisor-count bound over \(\kappa\)-th powers of monic polynomials#●ready to prove

Let \(F\) be a finite field with \(q\) elements and let \(\kappa\) assign a natural number to each polynomial in \(F[T]\), with \(\kappa(P) \ge 2\) for every monic irreducible \(P\). For monic \(r = \prod_P P^{\nu_P}\) write \(r^\kappa = \prod_P P^{\nu_P \kappa(P)}\), and let \(\kappa_{\min}\) be the minimum of \(\kappa(P)\) over the monic irreducible \(P\). Then for every \(\varepsilon > 0\), as \(N \to \infty\),

\[\sum_{r \text{ monic},\ \deg r^\kappa \le N} \ \sum_{f \mid r^\kappa} \ \sum_{\ell \mid f} 1 = O\left(q^{(1/\kappa_{\min} + \varepsilon) N}\right),\]

where \(f\) runs over the monic divisors of \(r^\kappa\) and \(\ell\) over the monic divisors of \(f\).

public theorem_wanted sum_divisors_kappaPow_isBigO {F : Type*} [Field F] [Fintype F]
    (κ : F[X] → ℕ) (hκ : ∀ P : F[X], P.Monic → Irreducible P → 2 ≤ κ P) {ε : ℝ} (hε : 0 < ε) :
    (fun N : ℕ => ((∑ᶠ r ∈ {r : F[X] | r.Monic ∧ (kappaPow κ r).natDegree ≤ N},
        ∑ᶠ f ∈ {f : F[X] | f.Monic ∧ f ∣ kappaPow κ r},
          Nat.card {ℓ : F[X] // ℓ.Monic ∧ ℓ ∣ f} : ℕ) : ℝ)) =O[atTop]
      fun N : ℕ => (Fintype.card F : ℝ) ^ ((1 / (kappaMin κ : ℝ) + ε) * N)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Lemma 8, eq. (7).
Uses 2
Statement usesThe minimal exponent \(\kappa_{\min}\) · The \(\kappa\)-power of a polynomial

TheoremEuler-product asymptotic with the \((h-1)\)-divisor function over \(\kappa\)-th powers#●ready to prove

Let \(F\) be a finite field with \(q\) elements, write \(|f| = q^{\deg f}\) for nonzero \(f \in F[T]\), and let \(\mu\) be the Möbius function of \(F[T]\). Let \(\kappa\) assign a natural number to each polynomial in \(F[T]\), with \(\kappa(P) \ge 2\) for every monic irreducible \(P\). For monic \(r = \prod_P P^{\nu_P}\) write \(r^\kappa = \prod_P P^{\nu_P \kappa(P)}\), and let \(\kappa_{\min}\) be the minimum of \(\kappa(P)\) over the monic irreducible \(P\). Let \(m \in F[T]\) be monic, let \(h \ge 1\), let \(d_{h-1}\) be the \((h-1)\)-divisor function, and put \(C_P = \binom{h + \kappa(P) - 1}{\kappa(P)}\). Then for every \(\varepsilon > 0\), as \(N \to \infty\),

\[\sum_{\substack{r \text{ monic},\ \deg r^\kappa \le N \\ \gcd(r, m) = 1}} \frac{\mu(r)}{|r^\kappa|} \sum_{f \mid r^\kappa} d_{h-1}(f) \sum_{g \mid f} \frac{\mu(g)}{|g|} = \prod_{P \nmid m} \left(1 - \frac{1}{|P|^{\kappa(P)}} \left(C_P + \frac{1}{|P|} (1 - C_P)\right)\right) + O\left(q^{(1/\kappa_{\min} + \varepsilon - 1)(N + 1)}\right),\]

where \(f\) runs over the monic divisors of \(r^\kappa\), \(g\) over the monic divisors of \(f\), and \(P\) over the monic irreducible polynomials not dividing \(m\).

public theorem_wanted sum_moebius_kappaPow_divisorCount_isBigO {F : Type*} [Field F] [Fintype F]
    (κ : F[X] → ℕ) (hκ : ∀ P : F[X], P.Monic → Irreducible P → 2 ≤ κ P) {m : F[X]}
    (hm : m.Monic) {h : ℕ} (hh : 1 ≤ h) {ε : ℝ} (hε : 0 < ε) :
    (fun N : ℕ =>
      (∑ᶠ r ∈ {r : F[X] | r.Monic ∧ (kappaPow κ r).natDegree ≤ N ∧ IsCoprime r m},
          (moebius r : ℝ) / fqNorm (kappaPow κ r) *
            ∑ᶠ f ∈ {f : F[X] | f.Monic ∧ f ∣ kappaPow κ r}, (monicDivisorCount (h - 1) f : ℝ) *
              ∑ᶠ g ∈ {g : F[X] | g.Monic ∧ g ∣ f}, (moebius g : ℝ) / fqNorm g) -
        ∏' P : {P : F[X] // P.Monic ∧ Irreducible P ∧ ¬ P ∣ m},
          (1 - 1 / fqNorm (P : F[X]) ^ κ P *
            ((Nat.choose (h + κ P - 1) (κ P) : ℝ) +
              1 / fqNorm (P : F[X]) * (1 - (Nat.choose (h + κ P - 1) (κ P) : ℝ))))) =O[atTop]
      fun N : ℕ => (Fintype.card F : ℝ) ^ ((1 / (kappaMin κ : ℝ) + ε - 1) * (N + 1))
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Proposition 1.
Uses 4
Statement usesNorm of a polynomial over a finite field · The minimal exponent \(\kappa_{\min}\) · The \(\kappa\)-power of a polynomial · The \(h\)-fold divisor function

TheoremEuler-product asymptotic for a degree-weighted Möbius sum over \(\kappa\)-th powers#●ready to prove

Let \(F\) be a finite field with \(q\) elements, write \(|f| = q^{\deg f}\) for nonzero \(f \in F[T]\), and let \(\mu\) be the Möbius function of \(F[T]\). Let \(\kappa\) assign a natural number to each polynomial in \(F[T]\), with \(\kappa(P) \ge 2\) for every monic irreducible \(P\). For monic \(r = \prod_P P^{\nu_P}\) write \(r^\kappa = \prod_P P^{\nu_P \kappa(P)}\), and let \(\kappa_{\min}\) be the minimum of \(\kappa(P)\) over the monic irreducible \(P\). Let \(m \in F[T]\) be monic. Then for every \(\varepsilon > 0\), as \(N \to \infty\),

\[\sum_{\substack{r \text{ monic},\ \deg r^\kappa \le N \\ \gcd(r, m) = 1}} \frac{\mu(r)}{|r^\kappa|} \sum_{f \mid r^\kappa} \sum_{g \mid f} \frac{\mu(g) \deg g}{|g|} = \prod_{P \nmid m} \left(1 - \frac{\kappa(P) + 1}{|P|^{\kappa(P)}} + \frac{\kappa(P)}{|P|^{\kappa(P) + 1}}\right) \sum_{P \nmid m} \frac{\kappa(P) \deg P}{|P|^{\kappa(P) + 1} - |P| (\kappa(P) + 1) + \kappa(P)} + O\left(q^{(1/\kappa_{\min} + \varepsilon - 1)(N + 1)}\right),\]

where \(f\) runs over the monic divisors of \(r^\kappa\), \(g\) over the monic divisors of \(f\), and \(P\) in the product and in the sum over the monic irreducible polynomials not dividing \(m\).

MetaMathlibExt.sum_moebius_kappaPow_moebius_natDegree_isBigO · 15 lines 
public theorem_wanted sum_moebius_kappaPow_moebius_natDegree_isBigO {F : Type*} [Field F]
    [Fintype F] (κ : F[X] → ℕ) (hκ : ∀ P : F[X], P.Monic → Irreducible P → 2 ≤ κ P) {m : F[X]}
    (hm : m.Monic) {ε : ℝ} (hε : 0 < ε) :
    (fun N : ℕ =>
      (∑ᶠ r ∈ {r : F[X] | r.Monic ∧ (kappaPow κ r).natDegree ≤ N ∧ IsCoprime r m},
          (moebius r : ℝ) / fqNorm (kappaPow κ r) *
            ∑ᶠ f ∈ {f : F[X] | f.Monic ∧ f ∣ kappaPow κ r},
              ∑ᶠ g ∈ {g : F[X] | g.Monic ∧ g ∣ f}, (moebius g : ℝ) * g.natDegree / fqNorm g) -
        (∏' P : {P : F[X] // P.Monic ∧ Irreducible P ∧ ¬ P ∣ m},
            (1 - (κ P + 1 : ℝ) / fqNorm (P : F[X]) ^ κ P +
              (κ P : ℝ) / fqNorm (P : F[X]) ^ (κ P + 1))) *
          ∑' P : {P : F[X] // P.Monic ∧ Irreducible P ∧ ¬ P ∣ m},
            (κ P : ℝ) * (P : F[X]).natDegree /
              (fqNorm (P : F[X]) ^ (κ P + 1) - fqNorm (P : F[X]) * (κ P + 1) + κ P)) =O[atTop]
      fun N : ℕ => (Fintype.card F : ℝ) ^ ((1 / (kappaMin κ : ℝ) + ε - 1) * (N + 1))
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Proposition 2.
Uses 3
Statement usesNorm of a polynomial over a finite field · The minimal exponent \(\kappa_{\min}\) · The \(\kappa\)-power of a polynomial

TheoremEuler-product asymptotic for a Möbius sum weighted by \(\deg r^\kappa\)#●ready to prove

Let \(F\) be a finite field with \(q\) elements, write \(|f| = q^{\deg f}\) for nonzero \(f \in F[T]\), and let \(\mu\) be the Möbius function of \(F[T]\). Let \(\kappa\) assign a natural number to each polynomial in \(F[T]\), with \(\kappa(P) \ge 2\) for every monic irreducible \(P\). For monic \(r = \prod_P P^{\nu_P}\) write \(r^\kappa = \prod_P P^{\nu_P \kappa(P)}\), and let \(\kappa_{\min}\) be the minimum of \(\kappa(P)\) over the monic irreducible \(P\). Let \(m \in F[T]\) be monic. Then for every \(\varepsilon > 0\), as \(N \to \infty\),

\[\sum_{\substack{r \text{ monic},\ \deg r^\kappa \le N \\ \gcd(r, m) = 1}} \frac{\mu(r) \deg r^\kappa}{|r^\kappa|} \sum_{f \mid r^\kappa} \sum_{g \mid f} \frac{\mu(g)}{|g|} = -\prod_{P \nmid m} \left(1 - \frac{\kappa(P) + 1}{|P|^{\kappa(P)}} + \frac{\kappa(P)}{|P|^{\kappa(P) + 1}}\right) \sum_{P \nmid m} \frac{\kappa(P) \deg P \, (|P| (\kappa(P) + 1) - \kappa(P))} {|P|^{\kappa(P) + 1} - |P| (\kappa(P) + 1) + \kappa(P)} + O\left(q^{(1/\kappa_{\min} + \varepsilon - 1)(N + 1)}\right),\]

where \(f\) runs over the monic divisors of \(r^\kappa\), \(g\) over the monic divisors of \(f\), and \(P\) in the product and in the sum over the monic irreducible polynomials not dividing \(m\).

MetaMathlibExt.sum_moebius_natDegree_kappaPow_isBigO · 15 lines 
public theorem_wanted sum_moebius_natDegree_kappaPow_isBigO {F : Type*} [Field F] [Fintype F]
    (κ : F[X] → ℕ) (hκ : ∀ P : F[X], P.Monic → Irreducible P → 2 ≤ κ P) {m : F[X]}
    (hm : m.Monic) {ε : ℝ} (hε : 0 < ε) :
    (fun N : ℕ =>
      (∑ᶠ r ∈ {r : F[X] | r.Monic ∧ (kappaPow κ r).natDegree ≤ N ∧ IsCoprime r m},
          (moebius r : ℝ) * (kappaPow κ r).natDegree / fqNorm (kappaPow κ r) *
            ∑ᶠ f ∈ {f : F[X] | f.Monic ∧ f ∣ kappaPow κ r},
              ∑ᶠ g ∈ {g : F[X] | g.Monic ∧ g ∣ f}, (moebius g : ℝ) / fqNorm g) +
        (∏' P : {P : F[X] // P.Monic ∧ Irreducible P ∧ ¬ P ∣ m},
            (1 - (κ P + 1 : ℝ) / fqNorm (P : F[X]) ^ κ P +
              (κ P : ℝ) / fqNorm (P : F[X]) ^ (κ P + 1))) *
          ∑' P : {P : F[X] // P.Monic ∧ Irreducible P ∧ ¬ P ∣ m},
            (κ P : ℝ) * (P : F[X]).natDegree * (fqNorm (P : F[X]) * (κ P + 1) - κ P) /
              (fqNorm (P : F[X]) ^ (κ P + 1) - fqNorm (P : F[X]) * (κ P + 1) + κ P)) =O[atTop]
      fun N : ℕ => (Fintype.card F : ℝ) ^ ((1 / (kappaMin κ : ℝ) + ε - 1) * (N + 1))
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Proposition 3.
Uses 3
Statement usesNorm of a polynomial over a finite field · The minimal exponent \(\kappa_{\min}\) · The \(\kappa\)-power of a polynomial

TheoremCharacter sums of the \(h\)-divisor function over monic polynomials#●ready to prove

Let \(F\) be a finite field with \(q\) elements, let \(m \in F[T]\) be monic, and let \(\chi\) be a non-principal Dirichlet character modulo \(m\): a multiplicative character of \(F[T]/(m)\), vanishing off the units, other than the principal one, evaluated at \(f \in F[T]\) through the class of \(f\) modulo \(m\). Let \(h \ge 1\) be a natural number and let \(d_h\) be the \(h\)-divisor function, so that \(d_h(f)\) is the number of \(h\)-tuples of monic polynomials with product \(f\). Then for every natural number \(N\),

\[\left| \sum_{f \text{ monic},\ \deg f \le N} \chi(f) \, d_h(f) \right| \le (\sqrt{q} + 1)^{h (\deg m - 1)}.\]
public theorem_wanted norm_sum_mulChar_divisorCount_le {F : Type*} [Field F] [Fintype F]
    {m : F[X]} (hm : m.Monic) (χ : MulChar (F[X] ⧸ Ideal.span {m}) ℂ) (hχ : χ ≠ 1) {h : ℕ}
    (hh : 1 ≤ h) (N : ℕ) :
    ‖∑ᶠ f ∈ {f : F[X] | f.Monic ∧ f.natDegree ≤ N},
        χ (Ideal.Quotient.mk (Ideal.span {m}) f) * (monicDivisorCount h f : ℂ)‖ ≤
      (Real.sqrt (Fintype.card F) + 1) ^ (h * (m.natDegree - 1))
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Proposition 5; χ^{(h)} as in eq. (8).
Uses 1
Statement usesThe \(h\)-fold divisor function

DefinitionThe \(B_\kappa\)-free divisor sum#✓fully proved

Let \(F\) be a field, let \(\kappa\) assign a natural number to each polynomial in \(F[T]\), and let \(h\) and \(N\) be natural numbers. Then \(\tilde D_{B_\kappa,h}(N)\) is the sum of \(d_h(f)\) over the monic \(B_\kappa\)-free polynomials \(f \in F[T]\) of degree at most \(N\), where \(d_h(f)\) is the number of \(h\)-tuples of monic polynomials with product \(f\), and \(f\) is \(B_\kappa\)-free when \(P^{\kappa(P)}\) does not divide \(f\) for any monic irreducible \(P\).

The sum is meant for finite \(F\); if it has infinitely many nonzero terms, its value is \(0\).

public noncomputable def bFreeDivisorSum {F : Type*} [Field F] (κ : F[X] → ℕ) (h N : ℕ) : ℕ :=
  ∑ᶠ f ∈ {f : F[X] | f.Monic ∧ f.natDegree ≤ N ∧ IsBFree κ f}, monicDivisorCount h f
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 1, definition of D̃_{B_κ,h}(N).
Uses 2 · Used by 6
Statement uses\(B_\kappa\)-free polynomials · The \(h\)-fold divisor function
Used byAsymptotic for B-free divisor sums when h is at most 2 · The progression sum modulo 1 is the full sum · Asymptotic count of B-free polynomials · Divisor sums over \(B_\kappa\)-free polynomials in short intervals · Asymptotic for the \(B_\kappa\)-free sum of the divisor function · The \(B_\kappa\)-free divisor sum at degree zero

TheoremThe \(B_\kappa\)-free divisor sum at degree zero#✓fully proved

Let \(F\) be a field and let \(\kappa\) assign to each polynomial in \(F[T]\) a natural number, with \(\kappa(P) \ne 0\) for every monic irreducible \(P\). Call \(f \in F[T]\) \(B_\kappa\)-free when \(P^{\kappa(P)}\) does not divide \(f\) for any monic irreducible \(P\), let \(d_h(f)\) be the number of \(h\)-tuples of monic polynomials with product \(f\), and let \(\tilde D_{B_\kappa,h}(N)\) be the sum of \(d_h(f)\) over the \(B_\kappa\)-free monic \(f \in F[T]\) of degree at most \(N\). Then \(\tilde D_{B_\kappa,h}(0) = 1\) for every natural number \(h\).

public theorem bFreeDivisorSum_zero {F : Type*} [Field F] (κ : F[X] → ℕ)
    (hκ : ∀ P : F[X], P.Monic → Irreducible P → κ P ≠ 0) (h : ℕ) :
    bFreeDivisorSum κ h 0 = 1
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 1, definition of D̃_{B_κ,h}(N).
Uses 6
Statement usesThe \(B_\kappa\)-free divisor sum
Proof uses\(B_\kappa\)-free polynomials · The polynomial \(1\) is \(B_\kappa\)-free · The \(h\)-fold divisor function · The divisor functions at \(1\) · Monic polynomials of degree zero

DefinitionB-free divisor sum in an arithmetic progression#✓fully proved

For a field \(F\), a function \(\kappa : F[T] \to \mathbb{N}\), natural numbers \(h\) and \(N\), and \(a, m \in F[T]\), the natural number \(\tilde D_{\kappa,h}(N, a, m)\) is the sum of \(d_h(f)\) over the monic \(B_\kappa\)-free \(f \in F[T]\) of degree at most \(N\) with \(f \equiv a \pmod m\), that is, with \(m\) dividing \(f - a\). Here \(d_h(f)\) is the number of \(h\)-tuples of monic polynomials with product \(f\), and \(f\) is \(B_\kappa\)-free when no \(P^{\kappa(P)}\) with \(P\) monic irreducible divides it. The sum is finite when \(F\) is finite; it is taken to be \(0\) if infinitely many of its terms are nonzero.

public noncomputable def bFreeDivisorSumMod {F : Type*} [Field F] (κ : F[X] → ℕ) (h N : ℕ)
    (a m : F[X]) : ℕ :=
  ∑ᶠ f ∈ {f : F[X] | f.Monic ∧ f.natDegree ≤ N ∧ IsBFree κ f ∧ m ∣ f - a}, monicDivisorCount h f
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 1, definition of D̃_{B_κ,h}(N, a, m).
Uses 2 · Used by 4
Statement uses\(B_\kappa\)-free polynomials · The \(h\)-fold divisor function
Used byAsymptotic for B-free divisor sums in progressions when h is at most 2 · The progression sum modulo 1 is the full sum · Asymptotic count of B-free polynomials in an arithmetic progression · Asymptotic for the B-free divisor function in an arithmetic progression

TheoremThe progression sum modulo 1 is the full sum#✓fully proved

Let \(F\) be a field, let \(\kappa : F[T] \to \mathbb{N}\), and let \(h\) and \(N\) be natural numbers. Write \(\tilde D_{\kappa,h}(N)\) for the sum of \(d_h(f)\) over the monic \(B_\kappa\)-free \(f \in F[T]\) of degree at most \(N\), and for \(a, m \in F[T]\) write \(\tilde D_{\kappa,h}(N, a, m)\) for the same sum restricted to the \(f\) with \(f \equiv a \pmod m\). Here \(d_h(f)\) is the number of \(h\)-tuples of monic polynomials with product \(f\), \(f\) is \(B_\kappa\)-free when no \(P^{\kappa(P)}\) with \(P\) monic irreducible divides it, and a sum with infinitely many nonzero terms is taken to be \(0\). Then for every \(a \in F[T]\), \(\tilde D_{\kappa,h}(N, a, 1) = \tilde D_{\kappa,h}(N)\).

public theorem bFreeDivisorSumMod_one {F : Type*} [Field F] (κ : F[X] → ℕ) (h N : ℕ)
    (a : F[X]) : bFreeDivisorSumMod κ h N a 1 = bFreeDivisorSum κ h N
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Section 1, definition of D̃_{B_κ,h}(N, a, m).
Uses 4
Statement usesThe \(B_\kappa\)-free divisor sum · B-free divisor sum in an arithmetic progression
Proof uses\(B_\kappa\)-free polynomials · The \(h\)-fold divisor function

TheoremAsymptotic count of B-free polynomials#●ready to prove

Let \(F\) be a finite field with \(q\) elements, write \(|f| = q^{\deg f}\) for nonzero \(f \in F[T]\), and let \(\kappa\) assign a natural number to each polynomial in \(F[T]\), with \(\kappa(P) \ge 2\) for every monic irreducible \(P\); let \(\kappa_{\min}\) be the minimum of \(\kappa(P)\) over the monic irreducible \(P\). Let \(\tilde D_{\kappa,1}(N)\) be the sum of \(d_1(f)\) (which is \(1\) for monic \(f\)) over the monic \(B_\kappa\)-free \(f\) of degree at most \(N\), where \(f\) is \(B_\kappa\)-free when no \(P^{\kappa(P)}\) with \(P\) monic irreducible divides it. Then for every \(\varepsilon > 0\),

\[ \tilde D_{\kappa,1}(N) - \frac{q^N}{1 - 1/q} \prod_P \bigl(1 - |P|^{-\kappa(P)}\bigr) = O\bigl(q^{(1/\kappa_{\min} + \varepsilon) N}\bigr) \]

as \(N \to \infty\), the product running over the monic irreducible \(P\).

public theorem_wanted bFreeDivisorSum_one_isBigO {F : Type*} [Field F] [Fintype F]
    (κ : F[X] → ℕ) (hκ : ∀ P : F[X], P.Monic → Irreducible P → 2 ≤ κ P) {ε : ℝ} (hε : 0 < ε) :
    (fun N : ℕ => (bFreeDivisorSum κ 1 N : ℝ) -
        (Fintype.card F : ℝ) ^ N / (1 - 1 / (Fintype.card F : ℝ)) *
          ∏' P : {P : F[X] // P.Monic ∧ Irreducible P}, (1 - 1 / fqNorm (P : F[X]) ^ κ P))
      =O[atTop] fun N : ℕ => (Fintype.card F : ℝ) ^ ((1 / (kappaMin κ : ℝ) + ε) * N)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Theorem 1, first formula.
Uses 3
Statement usesThe \(B_\kappa\)-free divisor sum · Norm of a polynomial over a finite field · The minimal exponent \(\kappa_{\min}\)

TheoremAsymptotic for the \(B_\kappa\)-free sum of the divisor function#●ready to prove

Let \(F\) be a finite field with \(q\) elements and let \(\kappa\) assign to each polynomial in \(F[T]\) a natural number, with \(\kappa(P) \ge 2\) for every monic irreducible \(P\). A polynomial \(f\) is \(B_\kappa\)-free when \(P^{\kappa(P)}\) does not divide \(f\) for any monic irreducible \(P\); \(d_2(f)\) is the number of ordered pairs of monic polynomials with product \(f\); \(\tilde D_{B_\kappa,2}(N)\) is the sum of \(d_2(f)\) over the \(B_\kappa\)-free monic \(f\) of degree at most \(N\); \(\kappa_{\min}\) is the minimum of \(\kappa(P)\) over the monic irreducible \(P\); and for a monic irreducible \(P\) we write \(\kappa_P = \kappa(P)\) and \(|P| = q^{\deg P}\) for its norm. Then for every \(\varepsilon > 0\), as \(N \to \infty\),

\[ \tilde D_{B_\kappa,2}(N) = \frac{q^N}{1 - 1/q} \prod_P \left( 1 - \frac{\kappa_P + 1}{|P|^{\kappa_P}} + \frac{\kappa_P}{|P|^{\kappa_P + 1}} \right) \left( N + 1 - \frac{1}{q - 1} + \sum_P \frac{\kappa_P (\kappa_P + 1) \deg(P) (|P| - 1)}{|P|^{\kappa_P + 1} - |P| (\kappa_P + 1) + \kappa_P} \right) + O\left( q^{(1/\kappa_{\min} + \varepsilon) N} \right), \]

where the product and the sum run over the monic irreducible polynomials \(P\).

public theorem_wanted bFreeDivisorSum_two_isBigO {F : Type*} [Field F] [Fintype F]
    (κ : F[X] → ℕ) (hκ : ∀ P : F[X], P.Monic → Irreducible P → 2 ≤ κ P) {ε : ℝ} (hε : 0 < ε) :
    (fun N : ℕ => (bFreeDivisorSum κ 2 N : ℝ) -
        (Fintype.card F : ℝ) ^ N / (1 - 1 / (Fintype.card F : ℝ)) *
          (∏' P : {P : F[X] // P.Monic ∧ Irreducible P},
            (1 - (κ P + 1 : ℝ) / fqNorm (P : F[X]) ^ κ P +
              (κ P : ℝ) / fqNorm (P : F[X]) ^ (κ P + 1))) *
          ((N : ℝ) + 1 - 1 / ((Fintype.card F : ℝ) - 1) +
            ∑' P : {P : F[X] // P.Monic ∧ Irreducible P},
              (κ P : ℝ) * (κ P + 1) * (P : F[X]).natDegree * (fqNorm (P : F[X]) - 1) /
                (fqNorm (P : F[X]) ^ (κ P + 1) - fqNorm (P : F[X]) * (κ P + 1) + κ P)))
      =O[atTop] fun N : ℕ => (Fintype.card F : ℝ) ^ ((1 / (kappaMin κ : ℝ) + ε) * N)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Theorem 1, second formula.
Uses 3
Statement usesThe \(B_\kappa\)-free divisor sum · Norm of a polynomial over a finite field · The minimal exponent \(\kappa_{\min}\)

TheoremAsymptotic for B-free divisor sums when h is at most 2#●ready to prove

Let \(F\) be a finite field with \(q\) elements, write \(|f| = q^{\deg f}\) for nonzero \(f \in F[T]\), and let \(\kappa\) assign a natural number to each polynomial in \(F[T]\), with \(\kappa(P) \ge 2\) for every monic irreducible \(P\). Let \(h \in \{1, 2\}\) and let \(\tilde D_{\kappa,h}(N)\) be the sum of \(d_h(f)\) over the monic \(B_\kappa\)-free \(f\) of degree at most \(N\), where \(d_h(f)\) is the number of \(h\)-tuples of monic polynomials with product \(f\), and \(f\) is \(B_\kappa\)-free when no \(P^{\kappa(P)}\) with \(P\) monic irreducible divides it. Put \(C_P = \binom{h + \kappa(P) - 1}{\kappa(P)}\) and

\[ M(N) = \frac{q^N N^{h-1}}{1 - 1/q} \prod_P \Bigl(1 - |P|^{-\kappa(P)} \bigl(C_P + |P|^{-1} (1 - C_P)\bigr)\Bigr), \]

the product running over the monic irreducible \(P\). Then \(\tilde D_{\kappa,h}(N) - M(N) = O(M(N)/N)\) as \(N \to \infty\).

The paper states this for every \(h \ge 1\), but its main term is not correct for \(h \ge 3\).

MetaMathlibExt.bFreeDivisorSum_isBigO_of_le_two · 15 lines 
public theorem_wanted bFreeDivisorSum_isBigO_of_le_two {F : Type*} [Field F] [Fintype F]
    (κ : F[X] → ℕ) (hκ : ∀ P : F[X], P.Monic → Irreducible P → 2 ≤ κ P) {h : ℕ} (hh1 : 1 ≤ h)
    (hh2 : h ≤ 2) :
    (fun N : ℕ => (bFreeDivisorSum κ h N : ℝ) -
        (Fintype.card F : ℝ) ^ N * (N : ℝ) ^ (h - 1) / (1 - 1 / (Fintype.card F : ℝ)) *
          ∏' P : {P : F[X] // P.Monic ∧ Irreducible P},
            (1 - 1 / fqNorm (P : F[X]) ^ κ P *
              ((Nat.choose (h + κ P - 1) (κ P) : ℝ) +
                1 / fqNorm (P : F[X]) * (1 - (Nat.choose (h + κ P - 1) (κ P) : ℝ)))))
      =O[atTop] fun N : ℕ =>
        (Fintype.card F : ℝ) ^ N * (N : ℝ) ^ (h - 1) / (1 - 1 / (Fintype.card F : ℝ)) *
          (∏' P : {P : F[X] // P.Monic ∧ Irreducible P},
            (1 - 1 / fqNorm (P : F[X]) ^ κ P *
              ((Nat.choose (h + κ P - 1) (κ P) : ℝ) +
                1 / fqNorm (P : F[X]) * (1 - (Nat.choose (h + κ P - 1) (κ P) : ℝ))))) / N
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Theorem 2, cases h = 1, 2.
Uses 2
Statement usesThe \(B_\kappa\)-free divisor sum · Norm of a polynomial over a finite field

TheoremAsymptotic count of B-free polynomials in an arithmetic progression#●ready to prove

Let \(F\) be a finite field with \(q\) elements, write \(|f| = q^{\deg f}\) for nonzero \(f \in F[T]\), and let \(\kappa\) assign a natural number to each polynomial in \(F[T]\), with \(\kappa(P) \ge 2\) for every monic irreducible \(P\); let \(\kappa_{\min}\) be the minimum of \(\kappa(P)\) over the monic irreducible \(P\). Let \(m \ne 0\) and \(a\) be polynomials in \(F[T]\) with \(a\) coprime to \(m\), and let \(\tilde D_{\kappa,1}(N, a, m)\) be the sum of \(d_1(f)\) (which is \(1\) for monic \(f\)) over the monic \(B_\kappa\)-free \(f\) of degree at most \(N\) with \(f \equiv a \pmod m\), where \(f\) is \(B_\kappa\)-free when no \(P^{\kappa(P)}\) with \(P\) monic irreducible divides it. Then for every \(\varepsilon > 0\),

\[ \tilde D_{\kappa,1}(N, a, m) - \frac{q^N}{(1 - 1/q) \, |m|} \prod_{P \nmid m} \bigl(1 - |P|^{-\kappa(P)}\bigr) = O\bigl(q^{(1/\kappa_{\min} + \varepsilon) N}\bigr) \]

as \(N \to \infty\), the product running over the monic irreducible \(P\) not dividing \(m\).

The paper's statement does not list the hypothesis \(m \ne 0\); it is implicit, since \(m\) is the modulus of a progression.

public theorem_wanted bFreeDivisorSumMod_one_isBigO {F : Type*} [Field F] [Fintype F]
    (κ : F[X] → ℕ) (hκ : ∀ P : F[X], P.Monic → Irreducible P → 2 ≤ κ P) {a m : F[X]}
    (hm : m ≠ 0) (ham : IsCoprime a m) {ε : ℝ} (hε : 0 < ε) :
    (fun N : ℕ => (bFreeDivisorSumMod κ 1 N a m : ℝ) -
        (Fintype.card F : ℝ) ^ N / ((1 - 1 / (Fintype.card F : ℝ)) * fqNorm m) *
          ∏' P : {P : F[X] // P.Monic ∧ Irreducible P ∧ ¬ P ∣ m},
            (1 - 1 / fqNorm (P : F[X]) ^ κ P))
      =O[atTop] fun N : ℕ => (Fintype.card F : ℝ) ^ ((1 / (kappaMin κ : ℝ) + ε) * N)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Theorem 3, first formula.
Uses 3
Statement usesB-free divisor sum in an arithmetic progression · Norm of a polynomial over a finite field · The minimal exponent \(\kappa_{\min}\)

TheoremAsymptotic for the B-free divisor function in an arithmetic progression#●ready to prove

Let \(F\) be a finite field with \(q\) elements, write \(|f| = q^{\deg f}\) for nonzero \(f \in F[T]\), and let \(\kappa\) assign a natural number to each polynomial in \(F[T]\), with \(\kappa(P) \ge 2\) for every monic irreducible \(P\); let \(\kappa_{\min}\) be the minimum of \(\kappa(P)\) over the monic irreducible \(P\). Let \(m \ne 0\) and \(a\) be polynomials in \(F[T]\) with \(a\) coprime to \(m\), and let \(\tilde D_{\kappa,2}(N, a, m)\) be the sum of \(d_2(f)\) over the monic \(B_\kappa\)-free \(f\) of degree at most \(N\) with \(f \equiv a \pmod m\), where \(d_2(f)\) is the number of pairs of monic polynomials with product \(f\), and \(f\) is \(B_\kappa\)-free when no \(P^{\kappa(P)}\) with \(P\) monic irreducible divides it. Writing \(\kappa\) for \(\kappa(P)\) inside sums and products over \(P\), put

\[ M(N) = \frac{q^N}{(1 - 1/q) \, |m|} \prod_{P \mid m} \Bigl(1 - \frac{1}{|P|}\Bigr) \prod_{P \nmid m} \Bigl(1 - \frac{\kappa + 1}{|P|^{\kappa}} + \frac{\kappa}{|P|^{\kappa + 1}}\Bigr) \times \Bigl(N + 1 - \frac{1}{q - 1} + 2 \sum_{P \mid m} \frac{\deg P}{|P| - 1} + \sum_{P \nmid m} \frac{\kappa (\kappa + 1) \deg P \, (|P| - 1)}{|P|^{\kappa + 1} - |P| (\kappa + 1) + \kappa}\Bigr), \]

where \(P\) runs over the monic irreducible polynomials dividing, respectively not dividing, \(m\). Then for every \(\varepsilon > 0\), \(\tilde D_{\kappa,2}(N, a, m) - M(N) = O\bigl(q^{(1/\kappa_{\min} + \varepsilon) N}\bigr)\) as \(N \to \infty\).

MetaMathlibExt.bFreeDivisorSumMod_two_isBigO · 17 lines 
public theorem_wanted bFreeDivisorSumMod_two_isBigO {F : Type*} [Field F] [Fintype F]
    (κ : F[X] → ℕ) (hκ : ∀ P : F[X], P.Monic → Irreducible P → 2 ≤ κ P) {a m : F[X]}
    (hm : m ≠ 0) (ham : IsCoprime a m) {ε : ℝ} (hε : 0 < ε) :
    (fun N : ℕ => (bFreeDivisorSumMod κ 2 N a m : ℝ) -
        (Fintype.card F : ℝ) ^ N *
            (∏ᶠ P ∈ {P : F[X] | P.Monic ∧ Irreducible P ∧ P ∣ m}, (1 - 1 / fqNorm P)) /
            ((1 - 1 / (Fintype.card F : ℝ)) * fqNorm m) *
          (∏' P : {P : F[X] // P.Monic ∧ Irreducible P ∧ ¬ P ∣ m},
            (1 - (κ P + 1 : ℝ) / fqNorm (P : F[X]) ^ κ P +
              (κ P : ℝ) / fqNorm (P : F[X]) ^ (κ P + 1))) *
          ((N : ℝ) + 1 - 1 / ((Fintype.card F : ℝ) - 1) +
            2 * (∑ᶠ P ∈ {P : F[X] | P.Monic ∧ Irreducible P ∧ P ∣ m},
              (P.natDegree : ℝ) / (fqNorm P - 1)) +
            ∑' P : {P : F[X] // P.Monic ∧ Irreducible P ∧ ¬ P ∣ m},
              (κ P : ℝ) * (κ P + 1) * (P : F[X]).natDegree * (fqNorm (P : F[X]) - 1) /
                (fqNorm (P : F[X]) ^ (κ P + 1) - fqNorm (P : F[X]) * (κ P + 1) + κ P)))
      =O[atTop] fun N : ℕ => (Fintype.card F : ℝ) ^ ((1 / (kappaMin κ : ℝ) + ε) * N)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Theorem 3, second formula; Φ as defined after Theorem 3.
Uses 3
Statement usesB-free divisor sum in an arithmetic progression · Norm of a polynomial over a finite field · The minimal exponent \(\kappa_{\min}\)

TheoremAsymptotic for B-free divisor sums in progressions when h is at most 2#●ready to prove

Let \(F\) be a finite field with \(q\) elements, write \(|f| = q^{\deg f}\) for nonzero \(f \in F[T]\), and let \(\kappa\) assign a natural number to each polynomial in \(F[T]\), with \(\kappa(P) \ge 2\) for every monic irreducible \(P\). Let \(m \ne 0\) and \(a\) be polynomials in \(F[T]\) with \(a\) coprime to \(m\), let \(h \in \{1, 2\}\), and let \(\tilde D_{\kappa,h}(N, a, m)\) be the sum of \(d_h(f)\) over the monic \(B_\kappa\)-free \(f\) of degree at most \(N\) with \(f \equiv a \pmod m\), where \(d_h(f)\) is the number of \(h\)-tuples of monic polynomials with product \(f\), and \(f\) is \(B_\kappa\)-free when no \(P^{\kappa(P)}\) with \(P\) monic irreducible divides it. Put \(C_P = \binom{h + \kappa(P) - 1}{\kappa(P)}\) and

\[ M(N) = \frac{q^N N^{h-1}}{(h-1)!} \cdot \frac{\bigl(\prod_{P \mid m} (1 - 1/|P|)\bigr)^{h-1}}{|m| \, (1 - 1/q)} \prod_{P \nmid m} \Bigl(1 - |P|^{-\kappa(P)} \bigl(C_P + |P|^{-1} (1 - C_P)\bigr)\Bigr), \]

the products running over the monic irreducible \(P\) dividing, respectively not dividing, \(m\). Then \(\tilde D_{\kappa,h}(N, a, m) - M(N) = O(M(N)/N)\) as \(N \to \infty\).

The paper states this for every \(h \ge 1\), but its main term is not correct for \(h \ge 3\).

MetaMathlibExt.bFreeDivisorSumMod_isBigO_of_le_two · 19 lines 
public theorem_wanted bFreeDivisorSumMod_isBigO_of_le_two {F : Type*} [Field F] [Fintype F]
    (κ : F[X] → ℕ) (hκ : ∀ P : F[X], P.Monic → Irreducible P → 2 ≤ κ P) {a m : F[X]}
    (hm : m ≠ 0) (ham : IsCoprime a m) {h : ℕ} (hh1 : 1 ≤ h) (hh2 : h ≤ 2) :
    (fun N : ℕ => (bFreeDivisorSumMod κ h N a m : ℝ) -
        (Fintype.card F : ℝ) ^ N * (N : ℝ) ^ (h - 1) / (h - 1).factorial *
          (∏ᶠ P ∈ {P : F[X] | P.Monic ∧ Irreducible P ∧ P ∣ m}, (1 - 1 / fqNorm P)) ^ (h - 1) /
          fqNorm m / (1 - 1 / (Fintype.card F : ℝ)) *
          ∏' P : {P : F[X] // P.Monic ∧ Irreducible P ∧ ¬ P ∣ m},
            (1 - 1 / fqNorm (P : F[X]) ^ κ P *
              ((Nat.choose (h + κ P - 1) (κ P) : ℝ) +
                1 / fqNorm (P : F[X]) * (1 - (Nat.choose (h + κ P - 1) (κ P) : ℝ)))))
      =O[atTop] fun N : ℕ =>
        (Fintype.card F : ℝ) ^ N * (N : ℝ) ^ (h - 1) / (h - 1).factorial *
          (∏ᶠ P ∈ {P : F[X] | P.Monic ∧ Irreducible P ∧ P ∣ m}, (1 - 1 / fqNorm P)) ^ (h - 1) /
          fqNorm m / (1 - 1 / (Fintype.card F : ℝ)) *
          (∏' P : {P : F[X] // P.Monic ∧ Irreducible P ∧ ¬ P ∣ m},
            (1 - 1 / fqNorm (P : F[X]) ^ κ P *
              ((Nat.choose (h + κ P - 1) (κ P) : ℝ) +
                1 / fqNorm (P : F[X]) * (1 - (Nat.choose (h + κ P - 1) (κ P) : ℝ))))) / N
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Theorem 4, cases h = 1, 2; Φ as defined after Theorem 3.
Uses 2
Statement usesB-free divisor sum in an arithmetic progression · Norm of a polynomial over a finite field

TheoremDivisor sums over \(B_\kappa\)-free polynomials in short intervals#●ready to prove

Let \(F\) be a finite field with \(q\) elements and let \(\kappa\) assign to each polynomial in \(F[T]\) a natural number, with \(\kappa(P) \ge 2\) for every monic irreducible \(P\). Suppose that \(\kappa\) is symmetric: \(\kappa(P^*) = \kappa(P)\) for every monic irreducible \(P\) with \(P(0) \ne 0\), where \(P^*\) is the monic scalar multiple of \(T^{\deg P} P(1/T)\). Let \(h \ge 1\) be an integer, let \(c\) be a real number with \(c > (h + 2/\kappa_{\min})/(h + 2)\), and let \(\varepsilon > 0\). Then there is a constant \(C\) such that for every sufficiently large \(N\), every monic \(A \in F[T]\) of degree \(N\) and every integer \(\Delta\) with \(cN \le \Delta \le N - 2\),

\[ \left| \tilde N_{B_\kappa,h}(A, \Delta) - q^{-(N - \Delta - 1)} \left( \tilde D_{B_\kappa,h}(N) - \tilde D_{B_\kappa,h}(N - 1) \right) \right| \le C q^{h (N - \Delta)/2 + (1/\kappa_{\min} + \varepsilon) N}. \]

Here \(\tilde N_{B_\kappa,h}(A, \Delta)\) is the sum of \(d_h(f)\) over the \(B_\kappa\)-free \(f \in F[T]\) with \(\deg(f - A) \le \Delta\) (where \(\deg 0 = -\infty\)), \(d_h(f)\) is the number of \(h\)-tuples of monic polynomials with product \(f\), \(\tilde D_{B_\kappa,h}(N)\) is the sum of \(d_h(f)\) over the \(B_\kappa\)-free monic \(f\) of degree at most \(N\), and \(\kappa_{\min}\) is the minimum of \(\kappa(P)\) over the monic irreducible \(P\).

The paper's \(\kappa(P^*)\) leaves \(P^*\) unnormalized and undefined for \(P = T\).

public theorem_wanted bFreeDivisorSum_shortInterval {F : Type*} [Field F] [Fintype F]
    [DecidableEq F] (κ : F[X] → ℕ) (hκ : ∀ P : F[X], P.Monic → Irreducible P → 2 ≤ κ P)
    (hsymm : ∀ P : F[X], P.Monic → Irreducible P → P.coeff 0 ≠ 0 →
      κ (normalize P.reverse) = κ P)
    {h : ℕ} (hh : 1 ≤ h) {c : ℝ} (hc : (h + 2 / (kappaMin κ : ℝ)) / (h + 2) < c) {ε : ℝ}
    (hε : 0 < ε) :
    ∃ C : ℝ, ∀ᶠ N in atTop, ∀ A : F[X], A.Monic → A.natDegree = N → ∀ Δ : ℕ,
      c * N ≤ Δ → Δ + 2 ≤ N →
        |(∑ᶠ f ∈ {f : F[X] | (f - A).degree ≤ Δ ∧ IsBFree κ f}, (monicDivisorCount h f : ℝ)) -
            ((bFreeDivisorSum κ h N : ℝ) - bFreeDivisorSum κ h (N - 1)) /
              (Fintype.card F : ℝ) ^ (N - Δ - 1)| ≤
          C * (Fintype.card F : ℝ) ^ (h * ((N : ℝ) - Δ) / 2 + (1 / (kappaMin κ : ℝ) + ε) * N)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Theorem 5, general formula.
Uses 4
Statement uses\(B_\kappa\)-free polynomials · The \(B_\kappa\)-free divisor sum · The minimal exponent \(\kappa_{\min}\) · The \(h\)-fold divisor function

TheoremB-free polynomials in short intervals#●ready to prove

Let \(F\) be a finite field with \(q\) elements, write \(|f| = q^{\deg f}\) for nonzero \(f \in F[T]\), and let \(\kappa\) assign a natural number to each polynomial in \(F[T]\), with \(\kappa(P) \ge 2\) for every monic irreducible \(P\); let \(\kappa_{\min}\) be the minimum of \(\kappa(P)\) over the monic irreducible \(P\). Assume \(\kappa\) is symmetric: \(\kappa(P^*) = \kappa(P)\) for every monic irreducible \(P\) with \(P(0) \ne 0\), where \(P^*\) is the monic scalar multiple of the reversed polynomial \(T^{\deg P} P(1/T)\). Let \(c > (1 + 2/\kappa_{\min})/3\) and \(\varepsilon > 0\). Then there is a constant \(C\) such that for all sufficiently large \(N\), every monic \(A \in F[T]\) of degree \(N\) and every natural number \(\Delta\) with \(cN \le \Delta \le N - 2\),

\[ \Bigl|\sum_f d_1(f) - q^{\Delta + 1} \prod_P \bigl(1 - |P|^{-\kappa(P)}\bigr)\Bigr| \le C q^{(N - \Delta)/2 + (1/\kappa_{\min} + \varepsilon) N}, \]

where \(f\) runs over the \(B_\kappa\)-free \(f \in F[T]\) with \(f = A\) or \(\deg(f - A) \le \Delta\), \(d_1(f)\) is \(1\) if \(f\) is monic and \(0\) otherwise, \(f\) is \(B_\kappa\)-free when no \(P^{\kappa(P)}\) with \(P\) monic irreducible divides it, and \(P\) runs over the monic irreducible polynomials.

public theorem_wanted bFreeDivisorSum_shortInterval_one {F : Type*} [Field F] [Fintype F]
    [DecidableEq F] (κ : F[X] → ℕ) (hκ : ∀ P : F[X], P.Monic → Irreducible P → 2 ≤ κ P)
    (hsymm : ∀ P : F[X], P.Monic → Irreducible P → P.coeff 0 ≠ 0 →
      κ (normalize P.reverse) = κ P)
    {c : ℝ} (hc : (1 + 2 / (kappaMin κ : ℝ)) / 3 < c) {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, ∀ᶠ N in atTop, ∀ A : F[X], A.Monic → A.natDegree = N → ∀ Δ : ℕ,
      c * N ≤ Δ → Δ + 2 ≤ N →
        |(∑ᶠ f ∈ {f : F[X] | (f - A).degree ≤ Δ ∧ IsBFree κ f}, (monicDivisorCount 1 f : ℝ)) -
            (Fintype.card F : ℝ) ^ (Δ + 1) *
              ∏' P : {P : F[X] // P.Monic ∧ Irreducible P}, (1 - 1 / fqNorm (P : F[X]) ^ κ P)| ≤
          C * (Fintype.card F : ℝ) ^ (((N : ℝ) - Δ) / 2 + (1 / (kappaMin κ : ℝ) + ε) * N)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Theorem 5, case h = 1.
Uses 4
Statement uses\(B_\kappa\)-free polynomials · Norm of a polynomial over a finite field · The minimal exponent \(\kappa_{\min}\) · The \(h\)-fold divisor function

TheoremThe B-free divisor function in short intervals#●ready to prove

Let \(F\) be a finite field with \(q\) elements, write \(|f| = q^{\deg f}\) for nonzero \(f \in F[T]\), and let \(\kappa\) assign a natural number to each polynomial in \(F[T]\), with \(\kappa(P) \ge 2\) for every monic irreducible \(P\); let \(\kappa_{\min}\) be the minimum of \(\kappa(P)\) over the monic irreducible \(P\). Assume \(\kappa\) is symmetric: \(\kappa(P^*) = \kappa(P)\) for every monic irreducible \(P\) with \(P(0) \ne 0\), where \(P^*\) is the monic scalar multiple of the reversed polynomial \(T^{\deg P} P(1/T)\). Let \(c > (2 + 2/\kappa_{\min})/4\) and \(\varepsilon > 0\). Then there is a constant \(C\) such that for all sufficiently large \(N\), every monic \(A \in F[T]\) of degree \(N\) and every natural number \(\Delta\) with \(cN \le \Delta \le N - 2\),

\[ \Bigl|\sum_f d_2(f) - q^{\Delta + 1} \prod_P \Bigl(1 - \frac{\kappa + 1}{|P|^{\kappa}} + \frac{\kappa}{|P|^{\kappa + 1}}\Bigr) \Bigl(N + 1 + \sum_P \frac{\kappa \deg P \, (\kappa + 1) (|P| - 1)}{|P|^{\kappa + 1} - |P| (\kappa + 1) + \kappa}\Bigr) \Bigr| \le C q^{N - \Delta + (1/\kappa_{\min} + \varepsilon) N}, \]

where \(f\) runs over the \(B_\kappa\)-free \(f \in F[T]\) with \(f = A\) or \(\deg(f - A) \le \Delta\), \(d_2(f)\) is the number of pairs of monic polynomials with product \(f\), \(f\) is \(B_\kappa\)-free when no \(P^{\kappa(P)}\) with \(P\) monic irreducible divides it, \(P\) runs over the monic irreducible polynomials, and \(\kappa\) stands for \(\kappa(P)\).

MetaMathlibExt.bFreeDivisorSum_shortInterval_two · 16 lines 
public theorem_wanted bFreeDivisorSum_shortInterval_two {F : Type*} [Field F] [Fintype F]
    [DecidableEq F] (κ : F[X] → ℕ) (hκ : ∀ P : F[X], P.Monic → Irreducible P → 2 ≤ κ P)
    (hsymm : ∀ P : F[X], P.Monic → Irreducible P → P.coeff 0 ≠ 0 →
      κ (normalize P.reverse) = κ P)
    {c : ℝ} (hc : (2 + 2 / (kappaMin κ : ℝ)) / 4 < c) {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, ∀ᶠ N in atTop, ∀ A : F[X], A.Monic → A.natDegree = N → ∀ Δ : ℕ,
      c * N ≤ Δ → Δ + 2 ≤ N →
        |(∑ᶠ f ∈ {f : F[X] | (f - A).degree ≤ Δ ∧ IsBFree κ f}, (monicDivisorCount 2 f : ℝ)) -
            (Fintype.card F : ℝ) ^ (Δ + 1) *
              (∏' P : {P : F[X] // P.Monic ∧ Irreducible P},
                (1 - (κ P + 1 : ℝ) / fqNorm (P : F[X]) ^ κ P +
                  (κ P : ℝ) / fqNorm (P : F[X]) ^ (κ P + 1))) *
              ((N : ℝ) + 1 + ∑' P : {P : F[X] // P.Monic ∧ Irreducible P},
                (κ P : ℝ) * (P : F[X]).natDegree * (κ P + 1) * (fqNorm (P : F[X]) - 1) /
                  (fqNorm (P : F[X]) ^ (κ P + 1) - fqNorm (P : F[X]) * (κ P + 1) + κ P))| ≤
          C * (Fintype.card F : ℝ) ^ ((N : ℝ) - Δ + (1 / (kappaMin κ : ℝ) + ε) * N)
Sources
  • Habib Jaber and Matilde Lalín, Dirichlet Convolutions and Divisor Problems over B-Free Polynomials over Function Fields, INTEGERS 26 (2026), Article A80, Theorem 5, case h = 2.
Uses 4
Statement uses\(B_\kappa\)-free polynomials · Norm of a polynomial over a finite field · The minimal exponent \(\kappa_{\min}\) · The \(h\)-fold divisor function
28 fully proved25 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.