Documentation

LeanPool.Zeta3Irrational.D

LeanPool.Zeta3Irrational.D #

def LeanPool.Zeta3Irrational.d (s : Finset ℕ) :

The least common multiple of a finite set of natural numbers.

Equations

LeanPool.Zeta3Irrational.d s = s.lcm id

Instances For

theorem LeanPool.Zeta3Irrational.d_insert (s : Finset ℕ) (n : ℕ) :

d (insert n s) = n.lcm (d s)

theorem LeanPool.Zeta3Irrational.d_empty :

theorem LeanPool.Zeta3Irrational.dvd_d_of_mem (s : Finset ℕ) (n : ℕ) (h : n ∈ s) :

n ∣ d s

theorem LeanPool.Zeta3Irrational.d_dvd_d_of_le (s t : Finset ℕ) (h : s ≤ t) :

d s ∣ d t

theorem LeanPool.Zeta3Irrational.d_ne_zero (s : Finset ℕ) (hs : 0 ∉ s) :

d s ≠ 0

theorem LeanPool.Zeta3Irrational.d_eq_zero (s : Finset ℕ) (hs : 0 ∈ s) :

d s = 0

theorem LeanPool.Zeta3Irrational.Nat_Prime_dvd_lcm {p : ℕ} (hp : Nat.Prime p) (a b : ℕ) (h : p ∣ a.lcm b) :

p ∣ a ∨ p ∣ b

theorem LeanPool.Zeta3Irrational.Nat_primeFactors_lcm {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :

(a.lcm b).primeFactors = a.primeFactors ∪ b.primeFactors

theorem LeanPool.Zeta3Irrational.Nat_lcm_pow_two (a b : ℕ) :

a.lcm b ^ 2 = (a ^ 2).lcm (b ^ 2)

theorem LeanPool.Zeta3Irrational.Nat_lcm_pow_three (a b : ℕ) :

a.lcm b ^ 3 = (a ^ 3).lcm (b ^ 3)

theorem LeanPool.Zeta3Irrational.d_sq (s : Finset ℕ) :

d s ^ 2 = d (Finset.image (fun (x : ℕ) => x ^ 2) s)

theorem LeanPool.Zeta3Irrational.d_cube (s : Finset ℕ) :

d s ^ 3 = d (Finset.image (fun (x : ℕ) => x ^ 3) s)

theorem LeanPool.Zeta3Irrational.d_sq' (n : ℕ) :

d (Finset.Icc 1 n) ^ 2 = d (Finset.image (fun (x : ℕ) => x ^ 2) (Finset.Icc 1 n))

theorem LeanPool.Zeta3Irrational.d_cube' (n : ℕ) :

d (Finset.Icc 1 n) ^ 3 = d (Finset.image (fun (x : ℕ) => x ^ 3) (Finset.Icc 1 n))

theorem LeanPool.Zeta3Irrational.fin_d_neq_zero (n : ℕ) :

d (Finset.Icc 1 n) > 0

theorem LeanPool.Zeta3Irrational.lcm_factorization (m n p : ℕ) (hm : m ≠ 0) (hn : n ≠ 0) :

(m.lcm n).factorization p = max (m.factorization p) (n.factorization p)

theorem LeanPool.Zeta3Irrational.d_factorization (s : Finset ℕ) (hs : s.Nonempty) (p : ℕ) (hs₁ : 0 ∉ s) :

(d s).factorization p = (Finset.image (fun (i : ℕ) => i.factorization p) s).max' ⋯

theorem LeanPool.Zeta3Irrational.d_factorization' (s : Finset ℕ) (hs : s.Nonempty) (p : ℕ) (hs₁ : 0 ∉ s) :

↑((d s).factorization p) = (Finset.image (fun (i : ℕ) => ↑(i.factorization p)) s).max' ⋯

theorem LeanPool.Zeta3Irrational.d_primeFactors (s : Finset ℕ) (hs : 0 ∉ s) :

(d s).primeFactors = s.sup fun (i : ℕ) => i.primeFactors

theorem LeanPool.Zeta3Irrational.d_factorization_eq_div_log'' (p : ℕ) :

(d (Finset.Icc 1 0)).factorization p = ⌊Real.log 0 / Real.log ↑p⌋₊

theorem LeanPool.Zeta3Irrational.d_factorization_eq_div_log' (n p : ℕ) (hp : Nat.Prime p) :

(d (Finset.Icc 1 (n + 1))).factorization p = ⌊Real.log (↑n + 1) / Real.log ↑p⌋₊

theorem LeanPool.Zeta3Irrational.d_factorization_eq_div_log (n p : ℕ) (hp : Nat.Prime p) :

(d (Finset.Icc 1 n)).factorization p = ⌊Real.log ↑n / Real.log ↑p⌋₊

theorem LeanPool.Zeta3Irrational.d_eq_prod_pow' (n : ℕ) :

d (Finset.Icc 1 (n + 1)) = ∏ p ∈ (n + 1 + 1).primesBelow, p ^ (Finset.image (fun (i : ℕ) => i.factorization p) (Finset.Icc 1 (n + 1))).max' ⋯

theorem LeanPool.Zeta3Irrational.d_eq_prod_pow'' (n : ℕ) :

d (Finset.Icc 1 (n + 1)) = ∏ p ∈ (n + 1 + 1).primesBelow, p ^ ⌊Real.log (↑n + 1) / Real.log ↑p⌋₊

theorem LeanPool.Zeta3Irrational.d_eq_prod_pow (n : ℕ) :

d (Finset.Icc 1 n) = ∏ p ∈ (n + 1).primesBelow, p ^ ⌊Real.log ↑n / Real.log ↑p⌋₊

theorem LeanPool.Zeta3Irrational.d_le_pow_counting (n : ℕ) :

d (Finset.Icc 1 n) ≤ n ^ n.primeCounting