Integers with restricted factorization

Squarefree, k-free, k-full and powerful, smooth and rough numbers, highly composite numbers, integers with prescribed prime factors.

• Benelux pairs
• Consecutive smooth numbers
• Density of integers by their k-th smallest prime factor
• Distribution of cyclic numbers
• Highly composite numbers
• Integers with all prime factors 3 mod 4
• Power-free integers
• Powerful and k-full numbers
• Mean value of 2^ω(n) over squareful numbers
• Odd and even k-full and l-free numbers
• Powerful numbers in arithmetic progressions
• Rough numbers
• Squarefree numbers
• Weakly prime-additive numbers

TheoremAverage number of prime factors of h-free integers#✓fully proved

Let \(h \ge 2\) be an integer. Call a positive integer \(n\) \(h\)-free if every prime occurs in the factorization of \(n\) with exponent less than \(h\), and write \(\Omega(n)\) for the number of prime factors of \(n\) counted with multiplicity and \(\zeta\) for the Riemann zeta function. Then, as the real number \(x\) tends to infinity,

\[ \sum_{\substack{1 \le n \le x \\ n \ h\text{-free}}} \Omega(n) = \frac{x \log\log x}{\zeta(h)} + O(x). \]

theorem average_cardFactors_over_h_free
    (h : ℕ) (hh : 2 ≤ h) :
    Asymptotics.IsBigO Filter.atTop
      (fun x : ℝ =>
        (∑ n ∈ (Finset.Icc 1 ⌊x⌋₊).filter
            (fun n => ∀ p ∈ n.primeFactors, n.factorization p < h),
            (ArithmeticFunction.cardFactors n : ℝ)) -
          (1 / (riemannZeta (h : ℂ)).re) * x * Real.log (Real.log x))
      (fun x : ℝ => x)

Sources

• Rafael Jakimczuk and Matilde Lalín, "The Number of Prime Factors on Average in Certain Integer Sequences," Journal of Integer Sequences 25 (2022), Article 22.2.3, Theorem, lines 110–117, https://cs.uwaterloo.ca/journals/JIS/VOL25/Lalin/lalin2.tex

DefinitionConsecutive polynomial family#✓fully proved

Let \(k\) be a natural number. A family \(L_0, \dots, L_{k-1}\) of polynomials in \(\mathbb{Z}[X]\) is consecutive when \(L_{i+1} - L_i = 1\) for every \(i\) with \(i + 1 < k\).

def IsConsecutivePolynomialFamily (k : ℕ) (L : Fin k → Polynomial ℤ) : Prop :=
  ∀ i : Fin k, ∀ h : i.val + 1 < k, L ⟨i.val + 1, h⟩ - L i = 1

DefinitionNatural numbers with the same prime divisors#✓fully proved

Natural numbers \(a\) and \(b\) have the same prime support when every prime \(p\) divides \(a\) if and only if it divides \(b\).

def SamePrimeSupport (a b : ℕ) : Prop := ∀ p : ℕ, p.Prime → (p ∣ a ↔ p ∣ b)

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.