Squarefree numbers

DefinitionLocal factor#✓fully proved

Given \(a : \mathbb{N} \to \mathbb{C}\) and natural numbers \(p\) and \(e\), the local factor of \(a\) at \(p\) with exponent \(e\) is \(1\) if \(e = 0\), \(a(p)\) if \(e = 1\), and \(0\) if \(e \ge 2\).

def chapter5Entry30LocalCoeff (a : ℕ → ℂ) (p e : ℕ) : ℂ :=
  match e with
  | 0 => 1
  | 1 => a p
  | _ + 2 => 0

Used by 8

Used byCoefficients for Entry 30 · Entry 30 coefficients vanish at nonzero non-squarefree natural numbers · Entry 30 coefficients at squarefree integers · The Entry 30 coefficient at one · The Entry 30 coefficient at zero · Entry 30 local factors vanish at exponents at least two · Local factor at exponent one · Local factor at exponent zero

DefinitionCoefficients for Entry 30#✓fully proved

For a function \(a : \mathbb{N} \to \mathbb{C}\) and \(n \in \mathbb{N}\), the Entry 30 coefficient \(c_a(n) \in \mathbb{C}\) is \(0\) when \(n = 0\). When \(n \ne 0\) it is the product, over the prime factors \(p\) of \(n\), of the local factor of \(a\) at \(p\) with exponent the multiplicity of \(p\) in \(n\). The local factor at \(p\) with exponent \(e\) is \(1\) for \(e = 0\), \(a(p)\) for \(e = 1\), and \(0\) for \(e \ge 2\).

def chapter5Entry30Coeff (a : ℕ → ℂ) (n : ℕ) : ℂ :=
  if n = 0 then 0
  else ∏ p ∈ n.primeFactors, chapter5Entry30LocalCoeff a p (n.factorization p)

Uses 1 · Used by 13

Statement usesLocal factor

DefinitionTerms of the Dirichlet series over non-squarefree integers#✓fully proved

For \(s \in \mathbb{C}\) and a natural number \(j\), put \(n = j + 1\); the \(j\)-th term is \(0\) if \(n\) is squarefree and \(n^{-s}\) otherwise. As \(j\) ranges over the natural numbers, these are the terms of \(\sum n^{-s}\) over non-squarefree \(n \ge 1\).

def chapter5Entry30NonSquarefreeTerm (s : ℂ) (j : ℕ) : ℂ :=
  let n := j + 1
  if Squarefree n then 0 else (n : ℂ) ^ (-s)

Used by 4

Used byNon-squarefree term, explicit form · Ramanujan's squarefree Dirichlet series (Entry 30) · Summability of the non-squarefree terms · Sum of \(n^{-s}\) over non-squarefree \(n\)

DefinitionTerms over squarefree integers with an odd number of prime factors#✓fully proved

For \(s \in \mathbb{C}\) and a natural number \(j\), put \(n = j + 1\); the \(j\)-th term is \(n^{-s}\) if \(n\) is squarefree and has an odd number of distinct prime factors, and \(0\) otherwise. As \(j\) ranges over the natural numbers, these are the terms of \(\sum n^{-s}\) over squarefree \(n \ge 1\) with an odd number of prime factors.

def chapter5Entry30OddTerm (s : ℂ) (j : ℕ) : ℂ :=
  let n := j + 1
  if Squarefree n ∧ Odd n.primeFactors.card then (n : ℂ) ^ (-s) else 0

Used by 4

Used byOdd-count squarefree term, explicit form · Ramanujan's squarefree Dirichlet series (Entry 30) · Summability of the odd squarefree terms · Sum of \(n^{-s}\) over squarefree \(n\) with an odd number of prime factors

DefinitionSigned multiplicative coefficient#✓fully proved

For \(s \in \mathbb{C}\) and a natural number \(n\), let \(a(p) = -p^{-s}\) for natural numbers \(p\). The signed coefficient of \(n\) is \(0\) if \(n = 0\) and, for \(n \ne 0\), the product over the prime factors \(p\) of \(n\) of the local factor of \(a\) at \(p\) with exponent the multiplicity of \(p\) in \(n\), where the local factor of \(a\) at \(p\) with exponent \(e\) is \(1\) for \(e = 0\), \(a(p)\) for \(e = 1\), and \(0\) for \(e \ge 2\).

def chapter5Entry30SignedCoeff (s : ℂ) (n : ℕ) : ℂ :=
  chapter5Entry30Coeff (fun p => -((p : ℂ) ^ (-s))) n

def chapter5Entry30Coeff (a : ℕ → ℂ) (n : ℕ) : ℂ :=
  if n = 0 then 0
  else ∏ p ∈ n.primeFactors, chapter5Entry30LocalCoeff a p (n.factorization p)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:44

Uses 1 · Used by 2

Statement usesCoefficients for Entry 30

Used byExplicit form of the signed coefficient · Ramanujan's squarefree Dirichlet series (Entry 30)

DefinitionTerms of the Dirichlet series over squarefree integers#✓fully proved

For a complex number \(s\) and a natural number \(j\), let \(n = j + 1\); the \(j\)-th squarefree term is \(n^{-s}\) if \(n\) is squarefree and \(0\) otherwise, so the series of these terms over \(j \ge 0\) is \(\sum n^{-s}\) over the squarefree \(n \ge 1\).

def chapter5Entry30SquarefreeTerm (s : ℂ) (j : ℕ) : ℂ :=
  let n := j + 1
  if Squarefree n then (n : ℂ) ^ (-s) else 0

Used by 8

Used bySquarefree term, explicit form · Ramanujan's squarefree Dirichlet series (Entry 30) · Summability of the non-squarefree terms · Summability of the odd squarefree terms · Summability of the squarefree terms · Sum of \(n^{-s}\) over non-squarefree \(n\) · Sum of \(n^{-s}\) over squarefree \(n\) with an odd number of prime factors · Sum of \(n^{-s}\) over squarefree \(n\)

LemmaLocal factor at exponent zero#✓fully proved

For every \(a : \mathbb{N} \to \mathbb{C}\) and every natural number \(p\), the local factor of \(a\) at \(p\) with exponent \(0\) is \(1\).

@[simp]
lemma chapter5Entry30LocalCoeff_zero (a : ℕ → ℂ) (p : ℕ) :
    chapter5Entry30LocalCoeff a p 0 = 1

Uses 1

Statement usesLocal factor

LemmaLocal factor at exponent one#✓fully proved

For every \(a : \mathbb{N} \to \mathbb{C}\) and every natural number \(p\), the local factor of \(a\) at \(p\) with exponent \(1\) is \(a(p)\).

@[simp]
lemma chapter5Entry30LocalCoeff_one (a : ℕ → ℂ) (p : ℕ) :
    chapter5Entry30LocalCoeff a p 1 = a p

Uses 1

Statement usesLocal factor

LemmaEntry 30 local factors vanish at exponents at least two#✓fully proved

For every function \(a : \mathbb{N} \to \mathbb{C}\), every \(p \in \mathbb{N}\) and every \(e \ge 2\), the Entry 30 local factor of \(a\) at \(p\) with exponent \(e\) is \(0\).

lemma chapter5Entry30LocalCoeff_of_two_le (a : ℕ → ℂ) (p e : ℕ) (he : 2 ≤ e) :
    chapter5Entry30LocalCoeff a p e = 0

Uses 1 · Used by 1

Statement usesLocal factor

Used byEntry 30 coefficients vanish at nonzero non-squarefree natural numbers

LemmaEntry 30 coefficients at squarefree integers#✓fully proved

For every function \(a : \mathbb{N} \to \mathbb{C}\) and every squarefree \(n \in \mathbb{N}\) with \(n \ne 0\), the Entry 30 coefficient \(c_a(n)\) is the product of \(a(p)\) over the prime factors \(p\) of \(n\).

lemma chapter5Entry30Coeff_of_squarefree (a : ℕ → ℂ) (n : ℕ) (hn : n ≠ 0) (hsq : Squarefree n) :
    chapter5Entry30Coeff a n = ∏ p ∈ n.primeFactors, a p

def chapter5Entry30Coeff (a : ℕ → ℂ) (n : ℕ) : ℂ :=
  if n = 0 then 0
  else ∏ p ∈ n.primeFactors, chapter5Entry30LocalCoeff a p (n.factorization p)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:44

Uses 2 · Used by 5

Statement usesCoefficients for Entry 30

Proof usesLocal factor

Used byEntry 30 coefficients are multiplicative · Closed form of the Entry 30 coefficients · Entry 30 coefficients at primes · Euler product for the Entry 30 coefficients · Summability of the Entry 30 coefficients

LemmaEntry 30 coefficients vanish at nonzero non-squarefree natural numbers#✓fully proved

For every function \(a : \mathbb{N} \to \mathbb{C}\) and every natural number \(n \ne 0\) that is not squarefree, the Entry 30 coefficient \(c_a(n)\) is \(0\).

lemma chapter5Entry30Coeff_of_not_squarefree (a : ℕ → ℂ) (n : ℕ) (hn : n ≠ 0)
    (hsq : ¬Squarefree n) : chapter5Entry30Coeff a n = 0

def chapter5Entry30Coeff (a : ℕ → ℂ) (n : ℕ) : ℂ :=
  if n = 0 then 0
  else ∏ p ∈ n.primeFactors, chapter5Entry30LocalCoeff a p (n.factorization p)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:44

Uses 3 · Used by 5

Statement usesCoefficients for Entry 30

Proof usesLocal factor · Entry 30 local factors vanish at exponents at least two

Used byEntry 30 coefficients are multiplicative · Closed form of the Entry 30 coefficients · Entry 30 coefficients vanish at higher prime powers · Euler product for the Entry 30 coefficients · Summability of the Entry 30 coefficients

LemmaClosed form of the Entry 30 coefficients#✓fully proved

For every function \(a : \mathbb{N} \to \mathbb{C}\) and every \(n \in \mathbb{N}\) with \(n \ne 0\), the Entry 30 coefficient \(c_a(n)\) equals the product of \(a(p)\) over the prime factors \(p\) of \(n\) when \(n\) is squarefree, and \(c_a(n) = 0\) otherwise.

lemma chapter5Entry30Coeff_of_ne_zero (a : ℕ → ℂ) (n : ℕ) (hn : n ≠ 0) :
    chapter5Entry30Coeff a n =
      if Squarefree n then ∏ p ∈ n.primeFactors, a p else 0

def chapter5Entry30Coeff (a : ℕ → ℂ) (n : ℕ) : ℂ :=
  if n = 0 then 0
  else ∏ p ∈ n.primeFactors, chapter5Entry30LocalCoeff a p (n.factorization p)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:44

Uses 3 · Used by 2

Statement usesCoefficients for Entry 30

Proof usesEntry 30 coefficients vanish at nonzero non-squarefree natural numbers · Entry 30 coefficients at squarefree integers

Used byExplicit form of the signed coefficient · Ramanujan's squarefree Dirichlet series (Entry 30)

LemmaSummability of the Entry 30 coefficients#✓fully proved

Let \(a : \mathbb{N} \to \mathbb{C}\) and let \(c > 1\) be real with \(|a(p)| \le p^{-c}\) for every prime \(p\). Then the Entry 30 coefficients \(f_a(n)\) of \(a\) (equal to \(0\) at \(n = 0\); for \(n \ge 1\), the product of \(a(p)\) over the primes \(p \mid n\) if \(n\) is squarefree, and \(0\) otherwise) form a summable family over \(n \ge 2\).

lemma summable_chapter5Entry30Coeff_add_two (a : ℕ → ℂ) (c : ℝ) (hc : 1 < c)
    (ha : ∀ p : ℕ, p.Prime → ‖a p‖ ≤ Real.rpow (p : ℝ) (-c)) :
    Summable (fun j : ℕ => chapter5Entry30Coeff a (j + 2))

def chapter5Entry30Coeff (a : ℕ → ℂ) (n : ℕ) : ℂ :=
  if n = 0 then 0
  else ∏ p ∈ n.primeFactors, chapter5Entry30LocalCoeff a p (n.factorization p)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:44

Uses 3 · Used by 1

Statement usesCoefficients for Entry 30

Proof usesEntry 30 coefficients vanish at nonzero non-squarefree natural numbers · Entry 30 coefficients at squarefree integers

Used byRamanujan's squarefree Dirichlet series (Entry 30)

LemmaThe Entry 30 coefficient at zero#✓fully proved

For every function \(a : \mathbb{N} \to \mathbb{C}\), the Entry 30 coefficient \(c_a(0)\) is \(0\).

@[simp]
lemma chapter5Entry30Coeff_zero (a : ℕ → ℂ) : chapter5Entry30Coeff a 0 = 0

def chapter5Entry30Coeff (a : ℕ → ℂ) (n : ℕ) : ℂ :=
  if n = 0 then 0
  else ∏ p ∈ n.primeFactors, chapter5Entry30LocalCoeff a p (n.factorization p)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:44

Uses 2 · Used by 2

Statement usesCoefficients for Entry 30

Proof usesLocal factor

Used byEntry 30 coefficients are multiplicative · Euler product for the Entry 30 coefficients

LemmaThe Entry 30 coefficient at one#✓fully proved

For every function \(a : \mathbb{N} \to \mathbb{C}\), the Entry 30 coefficient \(c_a(1)\) is \(1\).

@[simp]
lemma chapter5Entry30Coeff_one (a : ℕ → ℂ) : chapter5Entry30Coeff a 1 = 1

def chapter5Entry30Coeff (a : ℕ → ℂ) (n : ℕ) : ℂ :=
  if n = 0 then 0
  else ∏ p ∈ n.primeFactors, chapter5Entry30LocalCoeff a p (n.factorization p)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:44

Uses 2 · Used by 2

Statement usesCoefficients for Entry 30

Proof usesLocal factor

Used byEntry 30 coefficients are multiplicative · Euler product for the Entry 30 coefficients

LemmaEntry 30 coefficients at primes#✓fully proved

For every function \(a : \mathbb{N} \to \mathbb{C}\) and every prime \(p\), the Entry 30 coefficient \(c_a(p)\) equals \(a(p)\).

lemma chapter5Entry30Coeff_prime (a : ℕ → ℂ) (p : ℕ) (hp : p.Prime) :
    chapter5Entry30Coeff a p = a p

def chapter5Entry30Coeff (a : ℕ → ℂ) (n : ℕ) : ℂ :=
  if n = 0 then 0
  else ∏ p ∈ n.primeFactors, chapter5Entry30LocalCoeff a p (n.factorization p)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:44

Uses 2 · Used by 1

Statement usesCoefficients for Entry 30

Proof usesEntry 30 coefficients at squarefree integers

Used byEuler product for the Entry 30 coefficients

LemmaEntry 30 coefficients vanish at higher prime powers#✓fully proved

For every function \(a : \mathbb{N} \to \mathbb{C}\), every prime \(p\) and every \(e \ge 2\), the Entry 30 coefficient satisfies \(c_a(p^e) = 0\).

lemma chapter5Entry30Coeff_prime_pow_of_two_le (a : ℕ → ℂ) (p e : ℕ) (hp : p.Prime) (he : 2 ≤ e) :
    chapter5Entry30Coeff a (p ^ e) = 0

def chapter5Entry30Coeff (a : ℕ → ℂ) (n : ℕ) : ℂ :=
  if n = 0 then 0
  else ∏ p ∈ n.primeFactors, chapter5Entry30LocalCoeff a p (n.factorization p)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:44

Uses 2 · Used by 1

Statement usesCoefficients for Entry 30

Proof usesEntry 30 coefficients vanish at nonzero non-squarefree natural numbers

Used byEuler product for the Entry 30 coefficients

LemmaEntry 30 coefficients are multiplicative#✓fully proved

For every function \(a : \mathbb{N} \to \mathbb{C}\) and all coprime \(m, n \in \mathbb{N}\), the Entry 30 coefficients \(c_a\) satisfy \(c_a(mn) = c_a(m)\,c_a(n)\).

lemma chapter5Entry30Coeff_mul_of_coprime (a : ℕ → ℂ) (m n : ℕ) (hcop : Nat.Coprime m n) :
    chapter5Entry30Coeff a (m * n) = chapter5Entry30Coeff a m * chapter5Entry30Coeff a n

def chapter5Entry30Coeff (a : ℕ → ℂ) (n : ℕ) : ℂ :=
  if n = 0 then 0
  else ∏ p ∈ n.primeFactors, chapter5Entry30LocalCoeff a p (n.factorization p)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:44

Uses 5 · Used by 1

Statement usesCoefficients for Entry 30

Proof usesEntry 30 coefficients vanish at nonzero non-squarefree natural numbers · Entry 30 coefficients at squarefree integers · The Entry 30 coefficient at one · The Entry 30 coefficient at zero

Used byEuler product for the Entry 30 coefficients

LemmaEuler product for the Entry 30 coefficients#✓fully proved

Let \(a : \mathbb{N} \to \mathbb{C}\) and let \(c > 1\) be real with \(|a(p)| \le p^{-c}\) for every prime \(p\). Write \(f_a(n)\) for the Entry 30 coefficient of \(a\) at \(n\) (it is \(0\) at \(n = 0\); for \(n \ge 1\) it is the product of \(a(p)\) over the primes \(p \mid n\) if \(n\) is squarefree, and \(0\) otherwise). Then the product of \(1 + a(p)\) over all primes \(p\) converges unconditionally to \(1 + \sum_{n \ge 2} f_a(n)\).

lemma hasProd_one_add_chapter5Entry30Coeff (a : ℕ → ℂ) (c : ℝ) (hc : 1 < c)
    (ha : ∀ p : ℕ, p.Prime → ‖a p‖ ≤ Real.rpow (p : ℝ) (-c)) :
    HasProd (fun p : Nat.Primes => 1 + a p)
      (1 + ∑' j : ℕ, chapter5Entry30Coeff a (j + 2))

def chapter5Entry30Coeff (a : ℕ → ℂ) (n : ℕ) : ℂ :=
  if n = 0 then 0
  else ∏ p ∈ n.primeFactors, chapter5Entry30LocalCoeff a p (n.factorization p)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:44

Uses 8 · Used by 1

Statement usesCoefficients for Entry 30

Proof usesEntry 30 coefficients are multiplicative · Entry 30 coefficients vanish at nonzero non-squarefree natural numbers · Entry 30 coefficients at squarefree integers · The Entry 30 coefficient at one · Entry 30 coefficients at primes · Entry 30 coefficients vanish at higher prime powers · The Entry 30 coefficient at zero

Used byRamanujan's squarefree Dirichlet series (Entry 30)

LemmaSquarefree term, explicit form#✓fully proved

For \(s \in \mathbb{C}\) and a natural number \(j\), the \(j\)-th term of the Dirichlet series over squarefree integers equals \((j + 1)^{-s}\) if \(j + 1\) is squarefree and \(0\) otherwise.

lemma chapter5Entry30SquarefreeTerm_def (s : ℂ) (j : ℕ) :
    chapter5Entry30SquarefreeTerm s j
      = (if Squarefree (j + 1) then (((j + 1 : ℕ)) : ℂ) ^ (-s) else 0)

def chapter5Entry30SquarefreeTerm (s : ℂ) (j : ℕ) : ℂ :=
  let n := j + 1
  if Squarefree n then (n : ℂ) ^ (-s) else 0

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:64

Uses 1 · Used by 6

Statement usesTerms of the Dirichlet series over squarefree integers

Used bySummability of the non-squarefree terms · Summability of the odd squarefree terms · Summability of the squarefree terms · Sum of \(n^{-s}\) over non-squarefree \(n\) · Sum of \(n^{-s}\) over squarefree \(n\) with an odd number of prime factors · Sum of \(n^{-s}\) over squarefree \(n\)

LemmaSummability of the squarefree terms#✓fully proved

For every complex number \(s\) with \(\operatorname{Re} s > 1\), the series of \(n^{-s}\) over the squarefree \(n \ge 1\) is summable.

lemma summable_chapter5Entry30SquarefreeTerm (s : ℂ) (hs : 1 < s.re) :
    Summable (chapter5Entry30SquarefreeTerm s)

def chapter5Entry30SquarefreeTerm (s : ℂ) (j : ℕ) : ℂ :=
  let n := j + 1
  if Squarefree n then (n : ℂ) ^ (-s) else 0

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:64

Uses 2 · Used by 5

Statement usesTerms of the Dirichlet series over squarefree integers

Proof usesSquarefree term, explicit form

Used byRamanujan's squarefree Dirichlet series (Entry 30) · Summability of the non-squarefree terms · Summability of the odd squarefree terms · Sum of \(n^{-s}\) over non-squarefree \(n\) · Sum of \(n^{-s}\) over squarefree \(n\) with an odd number of prime factors

LemmaSum of \(n^{-s}\) over squarefree \(n\)#✓fully proved

For every complex number \(s\) with \(\operatorname{Re} s > 1\), the sum of \(n^{-s}\) over the squarefree \(n \ge 1\) equals \(\zeta(s)/\zeta(2s)\).

lemma tsum_chapter5Entry30SquarefreeTerm (s : ℂ) (hs : 1 < s.re) :
    (∑' j : ℕ, chapter5Entry30SquarefreeTerm s j)
      = riemannZeta s / riemannZeta (2 * s)

def chapter5Entry30SquarefreeTerm (s : ℂ) (j : ℕ) : ℂ :=
  let n := j + 1
  if Squarefree n then (n : ℂ) ^ (-s) else 0

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:64

Uses 2 · Used by 3

Statement usesTerms of the Dirichlet series over squarefree integers

Proof usesSquarefree term, explicit form

Used byRamanujan's squarefree Dirichlet series (Entry 30) · Sum of \(n^{-s}\) over non-squarefree \(n\) · Sum of \(n^{-s}\) over squarefree \(n\) with an odd number of prime factors

LemmaOdd-count squarefree term, explicit form#✓fully proved

For \(s \in \mathbb{C}\) and a natural number \(j\), the \(j\)-th term of the Dirichlet series over squarefree integers with an odd number of prime factors equals \((j + 1)^{-s}\) if \(j + 1\) is squarefree and has an odd number of distinct prime factors, and \(0\) otherwise.

lemma chapter5Entry30OddTerm_def (s : ℂ) (j : ℕ) :
    chapter5Entry30OddTerm s j
      = (if Squarefree (j + 1) ∧ Odd (j + 1).primeFactors.card
        then (((j + 1 : ℕ)) : ℂ) ^ (-s) else 0)

def chapter5Entry30OddTerm (s : ℂ) (j : ℕ) : ℂ :=
  let n := j + 1
  if Squarefree n ∧ Odd n.primeFactors.card then (n : ℂ) ^ (-s) else 0

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:55

Uses 1 · Used by 2

Statement usesTerms over squarefree integers with an odd number of prime factors

Used bySummability of the odd squarefree terms · Sum of \(n^{-s}\) over squarefree \(n\) with an odd number of prime factors

LemmaSummability of the odd squarefree terms#✓fully proved

For every complex number \(s\) with \(\operatorname{Re} s > 1\), the series of \(n^{-s}\) over the squarefree \(n \ge 1\) with an odd number of distinct prime factors is summable.

lemma summable_chapter5Entry30OddTerm (s : ℂ) (hs : 1 < s.re) :
    Summable (chapter5Entry30OddTerm s)

def chapter5Entry30OddTerm (s : ℂ) (j : ℕ) : ℂ :=
  let n := j + 1
  if Squarefree n ∧ Odd n.primeFactors.card then (n : ℂ) ^ (-s) else 0

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:55

Uses 5 · Used by 1

Statement usesTerms over squarefree integers with an odd number of prime factors

Proof usesOdd-count squarefree term, explicit form · Terms of the Dirichlet series over squarefree integers · Squarefree term, explicit form · Summability of the squarefree terms

Used byRamanujan's squarefree Dirichlet series (Entry 30)

LemmaSum of \(n^{-s}\) over squarefree \(n\) with an odd number of prime factors#✓fully proved

For every complex number \(s\) with \(\operatorname{Re} s > 1\), the sum of \(n^{-s}\) over the squarefree \(n \ge 1\) with an odd number of distinct prime factors equals \((\zeta(s)^2 - \zeta(2s))/(2\zeta(s)\zeta(2s))\).

lemma tsum_chapter5Entry30OddTerm (s : ℂ) (hs : 1 < s.re) :
    (∑' j : ℕ, chapter5Entry30OddTerm s j)
      = (riemannZeta s ^ 2 - riemannZeta (2 * s)) /
        (2 * riemannZeta s * riemannZeta (2 * s))

def chapter5Entry30OddTerm (s : ℂ) (j : ℕ) : ℂ :=
  let n := j + 1
  if Squarefree n ∧ Odd n.primeFactors.card then (n : ℂ) ^ (-s) else 0

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:55

Uses 6 · Used by 1

Statement usesTerms over squarefree integers with an odd number of prime factors

Proof usesOdd-count squarefree term, explicit form · Terms of the Dirichlet series over squarefree integers · Squarefree term, explicit form · Summability of the squarefree terms · Sum of \(n^{-s}\) over squarefree \(n\)

Used byRamanujan's squarefree Dirichlet series (Entry 30)

LemmaNon-squarefree term, explicit form#✓fully proved

For \(s \in \mathbb{C}\) and a natural number \(j\), the \(j\)-th term of the Dirichlet series over non-squarefree integers equals \(0\) if \(j + 1\) is squarefree and \((j + 1)^{-s}\) otherwise.

lemma chapter5Entry30NonSquarefreeTerm_def (s : ℂ) (j : ℕ) :
    chapter5Entry30NonSquarefreeTerm s j
      = (if Squarefree (j + 1) then 0 else ((((j + 1 : ℕ))) : ℂ) ^ (-s))

def chapter5Entry30NonSquarefreeTerm (s : ℂ) (j : ℕ) : ℂ :=
  let n := j + 1
  if Squarefree n then 0 else (n : ℂ) ^ (-s)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:49

Uses 1 · Used by 2

Statement usesTerms of the Dirichlet series over non-squarefree integers

Used bySummability of the non-squarefree terms · Sum of \(n^{-s}\) over non-squarefree \(n\)

LemmaSummability of the non-squarefree terms#✓fully proved

For every complex number \(s\) with \(\operatorname{Re} s > 1\), the series of \(n^{-s}\) over the non-squarefree \(n \ge 1\) is summable.

lemma summable_chapter5Entry30NonSquarefreeTerm (s : ℂ) (hs : 1 < s.re) :
    Summable (chapter5Entry30NonSquarefreeTerm s)

def chapter5Entry30NonSquarefreeTerm (s : ℂ) (j : ℕ) : ℂ :=
  let n := j + 1
  if Squarefree n then 0 else (n : ℂ) ^ (-s)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:49

Uses 5 · Used by 1

Statement usesTerms of the Dirichlet series over non-squarefree integers

Proof usesNon-squarefree term, explicit form · Terms of the Dirichlet series over squarefree integers · Squarefree term, explicit form · Summability of the squarefree terms

Used byRamanujan's squarefree Dirichlet series (Entry 30)

LemmaSum of \(n^{-s}\) over non-squarefree \(n\)#✓fully proved

For every complex number \(s\) with \(\operatorname{Re} s > 1\), the sum of \(n^{-s}\) over the non-squarefree \(n \ge 1\) equals \(\zeta(s)(\zeta(2s) - 1)/\zeta(2s)\).

lemma tsum_chapter5Entry30NonSquarefreeTerm (s : ℂ) (hs : 1 < s.re) :
    (∑' j : ℕ, chapter5Entry30NonSquarefreeTerm s j)
      = riemannZeta s * (riemannZeta (2 * s) - 1) / riemannZeta (2 * s)

def chapter5Entry30NonSquarefreeTerm (s : ℂ) (j : ℕ) : ℂ :=
  let n := j + 1
  if Squarefree n then 0 else (n : ℂ) ^ (-s)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:49

Uses 6 · Used by 1

Statement usesTerms of the Dirichlet series over non-squarefree integers

Proof usesNon-squarefree term, explicit form · Terms of the Dirichlet series over squarefree integers · Squarefree term, explicit form · Summability of the squarefree terms · Sum of \(n^{-s}\) over squarefree \(n\)

Used byRamanujan's squarefree Dirichlet series (Entry 30)

LemmaExplicit form of the signed coefficient#✓fully proved

For \(s \in \mathbb{C}\) and a natural number \(n \ne 0\), the signed coefficient of \(n\) equals \(-n^{-s}\) if \(n\) is squarefree with an odd number of distinct prime factors, \(n^{-s}\) if \(n\) is squarefree with an even number of distinct prime factors, and \(0\) if \(n\) is not squarefree.

lemma chapter5Entry30SignedCoeff_of_ne_zero (s : ℂ) (n : ℕ) (hn : n ≠ 0) :
    chapter5Entry30SignedCoeff s n =
      if Squarefree n then
        if Odd n.primeFactors.card then -((((n : ℕ))) : ℂ) ^ (-s)
        else ((((n : ℕ))) : ℂ) ^ (-s)
      else 0

Uses 3 · Used by 1

Statement usesSigned multiplicative coefficient

Proof usesCoefficients for Entry 30 · Closed form of the Entry 30 coefficients

Used byRamanujan's squarefree Dirichlet series (Entry 30)

TheoremRamanujan's squarefree Dirichlet series (Entry 30)#✓fully proved

(i) Let \(a : \mathbb{N} \to \mathbb{C}\) and let \(c > 1\) be real with \(|a(p)| \le p^{-c}\) for every prime \(p\), and write \(f_a(n)\) for the Entry 30 coefficient of \(a\) at \(n\). Then the family \((f_a(n))_{n \ge 2}\) is summable; for every \(n \ge 1\), \(f_a(n)\) is the product of \(a(p)\) over the primes \(p \mid n\) if \(n\) is squarefree and \(0\) otherwise; and the product of \(1 + a(p)\) over all primes \(p\) converges unconditionally to \(1 + \sum_{n \ge 2} f_a(n)\). (ii) Let \(s\) be a complex number with \(\operatorname{Re} s > 1\). Then for every \(n \ge 1\) the Entry 30 coefficient at \(n\) of \(p \mapsto -p^{-s}\) is \(-n^{-s}\) if \(n\) is squarefree with an odd number of distinct prime factors, \(n^{-s}\) if \(n\) is squarefree with an even number of distinct prime factors, and \(0\) if \(n\) is not squarefree; \(\zeta(s) \ne 0\) and \(\zeta(2s) \ne 0\); the series of \(n^{-s}\) over the squarefree \(n \ge 1\) is summable with sum \(\zeta(s)/\zeta(2s)\); the series of \(n^{-s}\) over the squarefree \(n \ge 1\) with an odd number of distinct prime factors is summable with sum \((\zeta(s)^2 - \zeta(2s))/(2\zeta(s)\zeta(2s))\); and the series of \(n^{-s}\) over the non-squarefree \(n \ge 1\) is summable with sum \(\zeta(s)(\zeta(2s) - 1)/\zeta(2s)\).

MathlibExt.Analysis.Ramanujan.Part1Ch5.Entry30Secondordereulerian.ramanujan_part1_ch5_entry30_secondordereulerian · 29 lines

theorem ramanujan_part1_ch5_entry30_secondordereulerian :
    (∀ (a : ℕ → ℂ) (c : ℝ), 1 < c →
      (∀ p : ℕ, p.Prime → ‖a p‖ ≤ Real.rpow (p : ℝ) (-c)) →
        Summable (fun j : ℕ => chapter5Entry30Coeff a (j + 2)) ∧
        (∀ n : ℕ, n ≠ 0 →
          chapter5Entry30Coeff a n =
            if Squarefree n then ∏ p ∈ n.primeFactors, a p else 0) ∧
        HasProd (fun p : Nat.Primes => 1 + a p)
          (1 + ∑' j : ℕ, chapter5Entry30Coeff a (j + 2))) ∧
    (∀ s : ℂ, 1 < s.re →
      (∀ n : ℕ, n ≠ 0 →
        chapter5Entry30SignedCoeff s n =
          if Squarefree n then
            if Odd n.primeFactors.card then -((n : ℂ) ^ (-s))
            else (n : ℂ) ^ (-s)
          else 0) ∧
      riemannZeta s ≠ 0 ∧
      riemannZeta (2 * s) ≠ 0 ∧
      Summable (chapter5Entry30SquarefreeTerm s) ∧
      (∑' j : ℕ, chapter5Entry30SquarefreeTerm s j) =
        riemannZeta s / riemannZeta (2 * s) ∧
      Summable (chapter5Entry30OddTerm s) ∧
      (∑' j : ℕ, chapter5Entry30OddTerm s j) =
        (riemannZeta s ^ 2 - riemannZeta (2 * s)) /
          (2 * riemannZeta s * riemannZeta (2 * s)) ∧
      Summable (chapter5Entry30NonSquarefreeTerm s) ∧
      (∑' j : ℕ, chapter5Entry30NonSquarefreeTerm s j) =
        riemannZeta s * (riemannZeta (2 * s) - 1) /
          riemannZeta (2 * s))

def chapter5Entry30Coeff (a : ℕ → ℂ) (n : ℕ) : ℂ :=
  if n = 0 then 0
  else ∏ p ∈ n.primeFactors, chapter5Entry30LocalCoeff a p (n.factorization p)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:44

def chapter5Entry30SignedCoeff (s : ℂ) (n : ℕ) : ℂ :=
  chapter5Entry30Coeff (fun p => -((p : ℂ) ^ (-s))) n

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:60

def chapter5Entry30SquarefreeTerm (s : ℂ) (j : ℕ) : ℂ :=
  let n := j + 1
  if Squarefree n then (n : ℂ) ^ (-s) else 0

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:64

def chapter5Entry30OddTerm (s : ℂ) (j : ℕ) : ℂ :=
  let n := j + 1
  if Squarefree n ∧ Odd n.primeFactors.card then (n : ℂ) ^ (-s) else 0

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:55

def chapter5Entry30NonSquarefreeTerm (s : ℂ) (j : ℕ) : ℂ :=
  let n := j + 1
  if Squarefree n then 0 else (n : ℂ) ^ (-s)

MathlibExt/Analysis/Ramanujan/Part1Ch5Entry30Secondordereulerian.lean:49

Sources

Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 5, Entry 30, pp. 131–132.

Uses 15

Statement usesCoefficients for Entry 30 · Terms of the Dirichlet series over non-squarefree integers · Terms over squarefree integers with an odd number of prime factors · Signed multiplicative coefficient · Terms of the Dirichlet series over squarefree integers

Proof usesClosed form of the Entry 30 coefficients · Explicit form of the signed coefficient · Euler product for the Entry 30 coefficients · Summability of the Entry 30 coefficients · Summability of the non-squarefree terms · Summability of the odd squarefree terms · Summability of the squarefree terms · Sum of \(n^{-s}\) over non-squarefree \(n\) · Sum of \(n^{-s}\) over squarefree \(n\) with an odd number of prime factors · Sum of \(n^{-s}\) over squarefree \(n\)

DefinitionEven or odd non-squarefree numbers up to a bound#✓fully proved

For a natural number \(N\), the set of integers \(n\) with \(1 \le n \le N\) that are even or not squarefree, that is, the even numbers in \(\{1, \dots, N\}\) together with the odd non-squarefree numbers in \(\{1, \dots, N\}\).

def evenOrOddNonSquarefree (N : ℕ) : Finset ℕ :=
  (Finset.Icc 1 N).filter (fun n => 2 ∣ n ∨ ¬ Squarefree n)

Used by 1

Used byErdős Problem 844

DefinitionErdős Problem 844#✓fully proved

For a natural number \(N\), let \(E_N\) be the set of integers \(n\) with \(1 \le n \le N\) that are even or not squarefree. The statement that for every natural number \(N\), the largest size of a set \(A \subseteq \{1, \dots, N\}\) such that \(ab\) is not squarefree for all \(a, b \in A\) (including \(a = b\)) is the size of \(E_N\).

def conjecture : Prop :=
  ∀ N : ℕ,
    IsGreatest {k : ℕ | ∃ A ⊆ Finset.Icc 1 N,
      (∀ a ∈ A, ∀ b ∈ A, ¬ Squarefree (a * b)) ∧ A.card = k}
      (evenOrOddNonSquarefree N).card

Uses 1 · Used by 1

Statement usesEven or odd non-squarefree numbers up to a bound

Used byErdős Problem 844 is true

TheoremErdős Problem 844 is true#●ready to prove

For every natural number \(N\), the largest size of a set \(A \subseteq \{1, \dots, N\}\) such that \(ab\) is not squarefree for all \(a, b \in A\) (including \(a = b\)) is the number of integers \(n\) with \(1 \le n \le N\) that are even or not squarefree.

public theorem_wanted conjecture_holds : conjecture

def conjecture : Prop :=
  ∀ N : ℕ,
    IsGreatest {k : ℕ | ∃ A ⊆ Finset.Icc 1 N,
      (∀ a ∈ A, ∀ b ∈ A, ¬ Squarefree (a * b)) ∧ A.card = k}
      (evenOrOddNonSquarefree N).card

WantedExt/NumberTheory/ErdosProblem844Wanted.lean:44

Sources

B. Alexeev, D. Mixon, and W. Sawin, The independence and clique cover numbers of the squarefree graph, arXiv:2507.01928 (2025), https://arxiv.org/abs/2507.01928; Erdős Problems, Problem 844 (including Desmond Weisenberg's proof), https://www.erdosproblems.com/latex/844.

Uses 1

Statement usesErdős Problem 844

32 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.