Powerful and k-full numbers

Definition\(k\)-full numbers#✓fully proved

Let \(k\) be a natural number. A natural number \(n\) is \(k\)-full if \(n \ne 0\) and \(p^k\) divides \(n\) for every prime \(p\) dividing \(n\).

The definition makes sense for every \(k\); the source considers only \(k \ge 2\).

public def IsKFull (k n : ℕ) : Prop :=
  n ≠ 0 ∧ ∀ p : ℕ, p.Prime → p ∣ n → p ^ k ∣ n

Used by 17

Used byFine zeta factorization of the squareful \(2^{\omega(n)}\) Dirichlet series · Coarse zeta factorization of the squareful \(2^{\omega(n)}\) Dirichlet series · Asymptotic for the sum of \(2^{\omega(n)}\) over squareful \(n\) · Odd-to-even ratio of \(k\)-full numbers · Odd-to-even ratio of \(k\)-full, \(l\)-free numbers · Odd-to-even ratio of \(l\)-free numbers · Factorization criterion for \(k\)-full numbers · The \(1\)-full numbers · The \(0\)-full numbers · Monotonicity of \(k\)-fullness in \(k\) · For \(k \ge 2\), \(k\)-full numbers are \(2\)-full · One is \(k\)-full · The \(2\)-full numbers · Zero is not \(k\)-full · Arithmetic progressions of 2-full numbers of every length · Arbitrarily long arithmetic progressions of powerful numbers · Four-term progressions of pairwise coprime powerful numbers

DefinitionPowerful part of a natural number#✓fully proved

For a natural number \(n \ge 1\) and a prime \(p\), let \(v_p(n)\) be the exponent of \(p\) in \(n\). The powerful (or \(2\)-full) part of \(n\) is the product of the prime powers \(p^{v_p(n)}\) over the primes \(p\) dividing \(n\) with \(v_p(n) \ge 2\) (and \(1\) if there are none). The powerful part of \(0\) is defined to be \(1\).

public def powerfulPart (n : ℕ) : ℕ :=
  Finset.prod (n.primeFactors.filter (fun p => 2 ≤ n.factorization p))
    (fun p ↦ p ^ n.factorization p)

Used by 2

Used byThe powerful part of \(n\) divides \(n\) · Prime exponents of the powerful part

TheoremPrime exponents of the powerful part#✓fully proved

For natural numbers \(n\) and \(p\), write \(v_p(n)\) for the exponent of \(p\) in the prime factorization of \(n\) (it is \(0\) when \(p\) is not a prime factor of \(n\)). Then the exponent of \(p\) in the powerful part of \(n\) equals \(v_p(n)\) if \(v_p(n) \ge 2\), and \(0\) otherwise.

public theorem powerfulPart_factorization (n p : ℕ) :
    (powerfulPart n).factorization p =
      if 2 ≤ n.factorization p then n.factorization p else 0

Uses 1 · Used by 1

Statement usesPowerful part of a natural number

Used byThe powerful part of \(n\) divides \(n\)

TheoremThe powerful part of \(n\) divides \(n\)#✓fully proved

For every natural number \(n\), the powerful part of \(n\) divides \(n\).

public theorem powerfulPart_dvd (n : ℕ) : powerfulPart n ∣ n

Uses 2

Statement usesPowerful part of a natural number

Proof usesPrime exponents of the powerful part

TheoremFactorization criterion for \(k\)-full numbers#✓fully proved

Let \(k\) and \(n\) be natural numbers with \(n \ne 0\), and write \(v_p(n)\) for the exponent of a prime \(p\) in the prime factorization of \(n\). Then \(n\) is \(k\)-full if and only if \(k \le v_p(n)\) for every prime \(p\) dividing \(n\).

public theorem isKFull_iff_factorization {k n : ℕ} (hn : n ≠ 0) :
    IsKFull k n ↔ ∀ p : ℕ, p.Prime → p ∣ n → k ≤ n.factorization p

Uses 1

Statement uses\(k\)-full numbers

TheoremZero is not \(k\)-full#✓fully proved

For every natural number \(k\), the number \(0\) is not \(k\)-full.

The source works with positive integers.

public theorem not_isKFull_zero (k : ℕ) : ¬ IsKFull k 0

Uses 1

Statement uses\(k\)-full numbers

TheoremOne is \(k\)-full#✓fully proved

For every natural number \(k\), the number \(1\) is \(k\)-full: it is nonzero and has no prime divisors.

public theorem isKFull_one (k : ℕ) : IsKFull k 1

Uses 1

Statement uses\(k\)-full numbers

TheoremThe \(0\)-full numbers#✓fully proved

A natural number \(n\) is \(0\)-full if and only if \(n \ne 0\), since \(p^0 = 1\) divides \(n\) for every prime \(p\).

The source considers only \(k\)-full numbers with \(k \ge 2\).

public theorem isKFull_k_eq_zero {n : ℕ} : IsKFull 0 n ↔ n ≠ 0

Uses 1

Statement uses\(k\)-full numbers

TheoremThe \(1\)-full numbers#✓fully proved

A natural number \(n\) is \(1\)-full if and only if \(n \ne 0\), since \(p^1 = p\) divides \(n\) for every prime \(p\) dividing \(n\).

The source considers only \(k\)-full numbers with \(k \ge 2\).

public theorem isKFull_k_eq_one {n : ℕ} : IsKFull 1 n ↔ n ≠ 0

Uses 1

Statement uses\(k\)-full numbers

TheoremMonotonicity of \(k\)-fullness in \(k\)#✓fully proved

Let \(j \le k\) be natural numbers. Every \(k\)-full natural number is \(j\)-full.

public theorem isKFull_mono {j k n : ℕ} (hjk : j ≤ k) (h : IsKFull k n) :
    IsKFull j n

Uses 1 · Used by 1

Statement uses\(k\)-full numbers

Used byFor \(k \ge 2\), \(k\)-full numbers are \(2\)-full

TheoremFor \(k \ge 2\), \(k\)-full numbers are \(2\)-full#✓fully proved

Let \(k \ge 2\) be a natural number. Every \(k\)-full natural number is \(2\)-full.

public theorem isKFull_of_two_le {k n : ℕ} (hk : 2 ≤ k) (h : IsKFull k n) :
    IsKFull 2 n

Uses 2

Statement uses\(k\)-full numbers

Proof usesMonotonicity of \(k\)-fullness in \(k\)

TheoremThe \(2\)-full numbers#✓fully proved

A natural number \(n\) is \(2\)-full if and only if \(n \ne 0\) and \(p^2\) divides \(n\) for every prime \(p\) dividing \(n\). These are the squarefull (also called powerful) numbers.

public theorem isKFull_two {n : ℕ} :
    IsKFull 2 n ↔ n ≠ 0 ∧ ∀ p : ℕ, p.Prime → p ∣ n → p ^ 2 ∣ n

Uses 1

Statement uses\(k\)-full numbers

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.