Lambert series

DefinitionLambert series summand#✓fully proved

For a complex number \(q\) with \(|q| < 1\) and a natural number \(k\), the \(k\)-th summand of the basic Lambert series is \(q^{k+1} / (1 - q^{k+1})\), that is, the term \(q^n / (1 - q^n)\) with \(n = k + 1\).

public noncomputable def lambertSeriesSummand (q : {q : ℂ // ‖q‖ < 1}) (k : ℕ) : ℂ :=
  (q : ℂ) ^ (k + 1) / (1 - (q : ℂ) ^ (k + 1))

Used by 1

Used byLambert series

DefinitionLambert series#✓fully proved

For a complex number \(q\) with \(|q| < 1\), the basic Lambert series is \(L(q) = \sum_{n \ge 1} q^n / (1 - q^n)\).

public noncomputable def lambertSeries (q : {q : ℂ // ‖q‖ < 1}) : ℂ :=
  ∑' k, lambertSeriesSummand q k

Uses 1

Statement usesLambert series summand

DefinitionTerms of the weighted Lambert series \(f\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\) and a natural number \(k\), the term of index \(k\) is \(n q^n / (1 - q^n)\) with \(n = k + 1\). These are the terms of the weighted Lambert series \(f(q) = \sum_{n \ge 1} n q^n / (1 - q^n)\).

public noncomputable def lambertFSummand (q : {q : ℂ // ‖q‖ < 1}) (k : ℕ) : ℂ :=
  (k + 1 : ℂ) * (q : ℂ) ^ (k + 1) / (1 - (q : ℂ) ^ (k + 1))

Used by 1

Used byThe weighted Lambert series \(f\)

DefinitionThe weighted Lambert series \(f\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\), the weighted Lambert series is \(f(q) = \sum_{n \ge 1} n q^n / (1 - q^n)\).

public noncomputable def lambertF (q : {q : ℂ // ‖q‖ < 1}) : ℂ :=
  ∑' k, lambertFSummand q k

Uses 1 · Used by 1

Statement usesTerms of the weighted Lambert series \(f\)

Used by\(2\)-adic expansion of the weighted Lambert series \(f\)

DefinitionTerms of the weighted Lambert series \(g\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\) and a natural number \(k\), the term of index \(k\) is \(n q^n / (1 + q^n)\) with \(n = k + 1\). These are the terms of the weighted Lambert series \(g(q) = \sum_{n \ge 1} n q^n / (1 + q^n)\).

public noncomputable def lambertGSummand (q : {q : ℂ // ‖q‖ < 1}) (k : ℕ) : ℂ :=
  (k + 1 : ℂ) * (q : ℂ) ^ (k + 1) / (1 + (q : ℂ) ^ (k + 1))

Used by 1

Used byThe weighted Lambert series \(g\)

DefinitionThe weighted Lambert series \(g\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\), the weighted Lambert series is \(g(q) = \sum_{n \ge 1} n q^n / (1 + q^n)\).

public noncomputable def lambertG (q : {q : ℂ // ‖q‖ < 1}) : ℂ :=
  ∑' k, lambertGSummand q k

Uses 1 · Used by 1

Statement usesTerms of the weighted Lambert series \(g\)

Used by\(2\)-adic expansion of the weighted Lambert series \(f\)

DefinitionTerms of the power-weighted Lambert series \(f_\mu\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\), an integer \(\mu \ge 1\) and a natural number \(k\), the term of index \(k\) is \(n^\mu q^n / (1 - q^n)\) with \(n = k + 1\). These are the terms of the power-weighted Lambert series \(f_\mu(q) = \sum_{n \ge 1} n^\mu q^n / (1 - q^n)\).

public noncomputable def lambertFMuSummand (q : {q : ℂ // ‖q‖ < 1})
    (μ : {μ : ℕ // 1 ≤ μ}) (k : ℕ) : ℂ :=
  (k + 1 : ℂ) ^ (μ : ℕ) * (q : ℂ) ^ (k + 1) / (1 - (q : ℂ) ^ (k + 1))

Used by 1

Used byThe power-weighted Lambert series \(f_\mu\)

DefinitionThe power-weighted Lambert series \(f_\mu\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\) and an integer \(\mu \ge 1\), the power-weighted Lambert series is \(f_\mu(q) = \sum_{n \ge 1} n^\mu q^n / (1 - q^n)\).

public noncomputable def lambertFMu (q : {q : ℂ // ‖q‖ < 1})
    (μ : {μ : ℕ // 1 ≤ μ}) : ℂ :=
  ∑' k, lambertFMuSummand q μ k

Uses 1 · Used by 1

Statement usesTerms of the power-weighted Lambert series \(f_\mu\)

Used byTwo-adic multisection of the power-weighted Lambert series

DefinitionTerms of the power-weighted Lambert series \(g_\mu\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\), an integer \(\mu \ge 1\) and a natural number \(k\), the term of index \(k\) is \(n^\mu q^n / (1 + q^n)\) with \(n = k + 1\). These are the terms of the power-weighted Lambert series \(g_\mu(q) = \sum_{n \ge 1} n^\mu q^n / (1 + q^n)\).

public noncomputable def lambertGMuSummand (q : {q : ℂ // ‖q‖ < 1})
    (μ : {μ : ℕ // 1 ≤ μ}) (k : ℕ) : ℂ :=
  (k + 1 : ℂ) ^ (μ : ℕ) * (q : ℂ) ^ (k + 1) / (1 + (q : ℂ) ^ (k + 1))

Used by 1

Used byThe power-weighted Lambert series \(g_\mu\)

DefinitionThe power-weighted Lambert series \(g_\mu\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\) and an integer \(\mu \ge 1\), the power-weighted Lambert series is \(g_\mu(q) = \sum_{n \ge 1} n^\mu q^n / (1 + q^n)\).

public noncomputable def lambertGMu (q : {q : ℂ // ‖q‖ < 1})
    (μ : {μ : ℕ // 1 ≤ μ}) : ℂ :=
  ∑' k, lambertGMuSummand q μ k

Uses 1 · Used by 1

Statement usesTerms of the power-weighted Lambert series \(g_\mu\)

Used byTwo-adic multisection of the power-weighted Lambert series

DefinitionTerms of the Lambert family \(L_m\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\), an integer \(m \ge 1\) and a natural number \(k\), the term of index \(k\) is \(q^{mn} / (1 - q^{2n})^m\) with \(n = k + 1\). These are the terms of \(L_m(q) = \sum_{n \ge 1} q^{mn} / (1 - q^{2n})^m\).

public noncomputable def lambertLmSummand (q : {q : ℂ // ‖q‖ < 1})
    (m : {m : ℕ // 1 ≤ m}) (k : ℕ) : ℂ :=
  (q : ℂ) ^ ((m : ℕ) * (k + 1)) /
    (1 - (q : ℂ) ^ (2 * (k + 1))) ^ (m : ℕ)

Used by 1

Used byThe Lambert family \(L_m\)

DefinitionThe Lambert family \(L_m\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\) and an integer \(m \ge 1\), the Lambert family is \(L_m(q) = \sum_{n \ge 1} q^{mn} / (1 - q^{2n})^m\).

public noncomputable def lambertLm (q : {q : ℂ // ‖q‖ < 1})
    (m : {m : ℕ // 1 ≤ m}) : ℂ :=
  ∑' k, lambertLmSummand q m k

Uses 1

Statement usesTerms of the Lambert family \(L_m\)

DefinitionTerms of the Lambert-type series \(\tilde L_m\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\), an integer \(m \ge 1\) and a natural number \(k\), the term of index \(k\) is \(q^{(2k+1)m} / (1 + q^{2k+1})^{2m}\), that is, \(q^{(2n-1)m} / (1 + q^{2n-1})^{2m}\) with \(n = k + 1\).

noncomputable def tildeLMSummand (q : { q : ℂ // ‖q‖ < 1 }) (m : { m : ℕ // 1 ≤ m }) (k : ℕ) : ℂ :=
  (q.val ^ ((2 * k + 1) * m.val)) / ((1 + q.val ^ (2 * k + 1)) ^ (2 * m.val))

Sources

• Gerhold.

Used by 2

Used byThe Lambert-type series \(\tilde L_m\) · Summability of the Lambert-type series \(\tilde L_m\)

DefinitionSummability of the Lambert-type series \(\tilde L_m\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\) and an integer \(m \ge 1\), this predicate holds when the series \(\sum_{n \ge 1} q^{(2n-1)m} / (1 + q^{2n-1})^{2m}\) is summable in \(\mathbb{C}\).

noncomputable def tildeLMSummable (q : { q : ℂ // ‖q‖ < 1 }) (m : { m : ℕ // 1 ≤ m }) : Prop :=
  Summable (tildeLMSummand q m)

Sources

• Gerhold.

Uses 1

Statement usesTerms of the Lambert-type series \(\tilde L_m\)

DefinitionThe Lambert-type series \(\tilde L_m\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\) and an integer \(m \ge 1\), \(\tilde L_m(q) = \sum_{n \ge 1} q^{(2n-1)m} / (1 + q^{2n-1})^{2m}\), where the sum is taken to be \(0\) if the series is not summable.

noncomputable def tildeLM (q : { q : ℂ // ‖q‖ < 1 }) (m : { m : ℕ // 1 ≤ m }) : ℂ :=
  tsum (tildeLMSummand q m)

Sources

• Gerhold.

Uses 1

Statement usesTerms of the Lambert-type series \(\tilde L_m\)

DefinitionTerms of the Lambert-type series \(\hat L_m\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\), an integer \(m \ge 1\) and a natural number \(k\), the term of index \(k\) is \(q^{m(k+1)} / (1 + q^{2(k+1)})^m\), that is, \(q^{mn} / (1 + q^{2n})^m\) with \(n = k + 1\).

noncomputable def hatLMSummand (q : { q : ℂ // ‖q‖ < 1 }) (m : { m : ℕ // 1 ≤ m }) (k : ℕ) : ℂ :=
  (q.val ^ (m.val * (k + 1))) / ((1 + q.val ^ (2 * (k + 1))) ^ m.val)

Sources

• Gerhold.

Used by 2

Used byThe Lambert-type series \(\hat L_m\) · Summability of the Lambert-type series \(\hat L_m\)

DefinitionSummability of the Lambert-type series \(\hat L_m\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\) and an integer \(m \ge 1\), this predicate holds when the series \(\sum_{n \ge 1} q^{mn} / (1 + q^{2n})^m\) is summable in \(\mathbb{C}\).

noncomputable def hatLMSummable (q : { q : ℂ // ‖q‖ < 1 }) (m : { m : ℕ // 1 ≤ m }) : Prop :=
  Summable (hatLMSummand q m)

Sources

• Gerhold.

Uses 1

Statement usesTerms of the Lambert-type series \(\hat L_m\)

DefinitionThe Lambert-type series \(\hat L_m\)#✓fully proved

For a complex number \(q\) with \(|q| < 1\) and an integer \(m \ge 1\), \(\hat L_m(q) = \sum_{n \ge 1} q^{mn} / (1 + q^{2n})^m\), where the sum is taken to be \(0\) if the series is not summable.

noncomputable def hatLM (q : { q : ℂ // ‖q‖ < 1 }) (m : { m : ℕ // 1 ≤ m }) : ℂ :=
  tsum (hatLMSummand q m)

Sources

• Gerhold.

Uses 1

Statement usesTerms of the Lambert-type series \(\hat L_m\)

DefinitionTerms of the Lambert-type series \(L_m^*\)#✓fully proved

Terms of the Lambert-type series \(L_m^*\). For a complex number \(q\) with \(|q| < 1\), an integer \(m \ge 1\) and a natural number \(k\), the term of index \(k\) is \(q^{(2k+1)m} / (1 - q^{2k+1})^{2m}\), that is, \(q^{(2n-1)m} / (1 - q^{2n-1})^{2m}\) with \(n = k + 1\).

noncomputable def starLMSummand (q : { q : ℂ // ‖q‖ < 1 }) (m : { m : ℕ // 1 ≤ m }) (k : ℕ) : ℂ :=
  (q.val ^ ((2 * k + 1) * m.val)) / ((1 - q.val ^ (2 * k + 1)) ^ (2 * m.val))

Sources

• Gerhold.

Used by 2

Used byThe Lambert-type series \(L_m^*\) · Summability of the Lambert-type series \(L_m^*\)

DefinitionSummability of the Lambert-type series \(L_m^*\)#✓fully proved

Summability of the Lambert-type series \(L_m^*\). For a complex number \(q\) with \(|q| < 1\) and an integer \(m \ge 1\), this predicate holds when the series \(\sum_{n \ge 1} q^{(2n-1)m} / (1 - q^{2n-1})^{2m}\) is summable in \(\mathbb{C}\).

noncomputable def starLMSummable (q : { q : ℂ // ‖q‖ < 1 }) (m : { m : ℕ // 1 ≤ m }) : Prop :=
  Summable (starLMSummand q m)

Sources

• Gerhold.

Uses 1

Statement usesTerms of the Lambert-type series \(L_m^*\)

DefinitionThe Lambert-type series \(L_m^*\)#✓fully proved

The Lambert-type series \(L_m^*\). For a complex number \(q\) with \(|q| < 1\) and an integer \(m \ge 1\), \(L_m^*(q) = \sum_{n \ge 1} q^{(2n-1)m} / (1 - q^{2n-1})^{2m}\), where the sum is taken to be \(0\) if the series is not summable.

noncomputable def starLM (q : { q : ℂ // ‖q‖ < 1 }) (m : { m : ℕ // 1 ≤ m }) : ℂ :=
  tsum (starLMSummand q m)

Sources

• Gerhold.

Uses 1

Statement usesTerms of the Lambert-type series \(L_m^*\)

21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.