Documentation

LeanPool.Erdos367.RFullLowerBound

Erdős #367: r-full part and the odd-r extension #

For a positive integer m with prime factorization m = ∏ p^{a_p}, and r ≥ 1, the r-full part is B_r(m) = ∏_{p : a_p ≥ r} p^{a_p}.

Main theorem: for odd r ≥ 1 and q ≥ 2, with n = (q^r - 1)^r, (i) B_r(n) = n, (ii) q^r ∣ n + 1, (iii) B_r(n) · B_r(n+1) ≥ n · q^r, (iv) (B_r(n) · B_r(n+1))^r > n^{r+1}.

Definition of the r-full part #

source
noncomputable def RFullOdd.rFullPart (r m : ℕ) :
ℕ

The r-full part of m: the product of prime-power components p^{a_p} of m for which the exponent a_p ≥ r.

Equations
Instances For

    Factorization of rFullPart #

    source
    theorem RFullOdd.rFullPart_factorization (r m : ℕ) (_hm : m ≠ 0) :
    (rFullPart r m).factorization = Finsupp.filter (fun (p : ℕ) => r ≤ m.factorization p) m.factorization
    source
    theorem RFullOdd.rFullPart_pos (r m : ℕ) (_hm : m ≠ 0) :
    0 < rFullPart r m

    Key properties of rFullPart #

    source
    theorem RFullOdd.rFullPart_dvd (r m : ℕ) (hm : m ≠ 0) :
    rFullPart r m ∣ m
    source
    theorem RFullOdd.rFullPart_pow (r m : ℕ) (hm : m ≠ 0) (hr : r ≠ 0) :
    rFullPart r (m ^ r) = m ^ r
    source
    theorem RFullOdd.pow_dvd_rFullPart (r m d : ℕ) (hm : m ≠ 0) (hdvd : d ^ r ∣ m) :
    d ^ r ∣ rFullPart r m
    source
    theorem RFullOdd.pow_le_rFullPart (r m d : ℕ) (hm : m ≠ 0) (hdvd : d ^ r ∣ m) :
    d ^ r ≤ rFullPart r m

    If d^r ∣ m and m ≠ 0, then d^r ≤ B_r(m).

    L2: Odd-power divisibility #

    source
    theorem RFullOdd.odd_pow_add_one_dvd (r a : ℕ) (hr : Odd r) :
    a + 1 ∣ a ^ r + 1

    Main theorem: the odd-r case #

    source
    theorem RFullOdd.erdos367_i {r q : ℕ} (hr : 0 < r) (hq : 2 ≤ q) :
    rFullPart r ((q ^ r - 1) ^ r) = (q ^ r - 1) ^ r

    (i) B_r(n) = n where n = (q^r - 1)^r.

    source
    theorem RFullOdd.erdos367_ii {r q : ℕ} (hr : Odd r) (hq : 2 ≤ q) :
    q ^ r ∣ (q ^ r - 1) ^ r + 1
    source
    theorem RFullOdd.erdos367_Br_succ_ge {r q : ℕ} (hr_odd : Odd r) (_hr : 0 < r) (hq : 2 ≤ q) :
    q ^ r ≤ rFullPart r ((q ^ r - 1) ^ r + 1)

    B_r(n+1) ≥ q^r.

    source
    theorem RFullOdd.erdos367_iii {r q : ℕ} (hr_odd : Odd r) (hr : 0 < r) (hq : 2 ≤ q) :
    (q ^ r - 1) ^ r * q ^ r ≤ rFullPart r ((q ^ r - 1) ^ r) * rFullPart r ((q ^ r - 1) ^ r + 1)

    (iii) B_r(n) · B_r(n+1) ≥ n · q^r.

    source
    theorem RFullOdd.erdos367_iv {r q : ℕ} (hr_odd : Odd r) (hr : 0 < r) (hq : 2 ≤ q) :
    ((q ^ r - 1) ^ r) ^ (r + 1) < (rFullPart r ((q ^ r - 1) ^ r) * rFullPart r ((q ^ r - 1) ^ r + 1)) ^ r

    Axiom verification #