Separating squarefree and repeated prime factors

A powerful integer has no prime occurring to exponent one. Every positive integer splits into coprime squarefree and powerful factors. Every powerful integer has a canonical representation a²b³, useful for summability.

def NairTenenbaum.Powerful (n : ℕ) : Prop

An integer is powerful when every prime divisor occurs with exponent at least two.

Equations

• NairTenenbaum.Powerful n = (n ≠ 0 ∧ ∀ (p : ℕ), n.factorization p ≠ 1)

noncomputable def NairTenenbaum.singlePrimePart (n : ℕ+) : ℕ+

The part formed by primes occurring to the first power.

Equations

• NairTenenbaum.singlePrimePart n = NairTenenbaum.primeSelect (fun (x : Fin 1) => n) ({p ∈ (↑n).primeFactors | (↑n).factorization p = 1}) 0

noncomputable def NairTenenbaum.repeatedPrimePart (n : ℕ+) : ℕ+

The part formed by primes occurring with multiplicity at least two.

Equations

• NairTenenbaum.repeatedPrimePart n = NairTenenbaum.primeReject (fun (x : Fin 1) => n) ({p ∈ (↑n).primeFactors | (↑n).factorization p = 1}) 0

theorem NairTenenbaum.singlePrimePart_mul_repeatedPrimePart (n : ℕ+) : singlePrimePart n * repeatedPrimePart n = n

theorem NairTenenbaum.singlePrimePart_coprime_repeatedPrimePart (n : ℕ+) : (↑(singlePrimePart n)).Coprime ↑(repeatedPrimePart n)

theorem NairTenenbaum.squarefree_singlePrimePart (n : ℕ+) : Squarefree ↑(singlePrimePart n)

theorem NairTenenbaum.powerful_repeatedPrimePart (n : ℕ+) : Powerful ↑(repeatedPrimePart n)

noncomputable def NairTenenbaum.powerfulSquareBase (n : ℕ) : ℕ

The square base in the square-times-cube decomposition of a powerful integer.

Equations

• NairTenenbaum.powerfulSquareBase n = ∏ p ∈ n.primeFactors, p ^ (n.factorization p / 2 - n.factorization p % 2)

noncomputable def NairTenenbaum.powerfulCubeBase (n : ℕ) : ℕ

The cube base in the square-times-cube decomposition of a powerful integer.

Equations

• NairTenenbaum.powerfulCubeBase n = ∏ p ∈ n.primeFactors, p ^ (n.factorization p % 2)

theorem NairTenenbaum.powerful_eq_square_mul_cube {n : ℕ} (hn : Powerful n) : powerfulSquareBase n ^ 2 * powerfulCubeBase n ^ 3 = n

theorem NairTenenbaum.powerful_bases_injective : Function.Injective fun (n : { n : ℕ // Powerful n }) => (powerfulSquareBase ↑n, powerfulCubeBase ↑n)