Additive representation functions

DefinitionSum convolution#✓fully proved

Let \(R\) be a semiring. The sum convolution, or Cauchy product, of two functions \(f, g \colon \mathbb{N} \to R\) is the function \(\mathbb{N} \to R\) whose value at \(n \in \mathbb{N}\) is

\[\sum_{a + b = n} f(a)\, g(b),\]

where the sum runs over all pairs \((a, b)\) of natural numbers with \(a + b = n\).

def sumConv (f g : ℕ → R) (n : ℕ) : R := ∑ p ∈ antidiagonal n, f p.1 * g p.2

DefinitionOrdered representation count#✓fully proved

For a set \(A\) of natural numbers and a natural number \(n\), the ordered representation count of \(n\) by \(A\) is the number of ordered pairs \((a, b) \in A \times A\) with \(a + b = n\). Pairs are not identified under swapping: when \(a \ne b\), the pairs \((a, b)\) and \((b, a)\) are counted separately.

public noncomputable def orderedRepresentationCount (A : Set ℕ) (n : ℕ) : ℕ := by
  classical
  exact ((Finset.antidiagonal n).filter
    (fun ab => ab.1 ∈ A ∧ ab.2 ∈ A)).card

Used by 1

Used byPositivity of the ordered representation count

TheoremPositivity of the ordered representation count#✓fully proved

For a set \(A\) of natural numbers and a natural number \(n\), the number of ordered pairs \((a, b) \in A \times A\) with \(a + b = n\) is positive if and only if \(n = a + b\) for some \(a \in A\) and \(b \in A\).

public theorem orderedRepresentationCount_pos_iff {A : Set ℕ} {n : ℕ} :
    0 < orderedRepresentationCount A n ↔
      ∃ a ∈ A, ∃ b ∈ A, a + b = n

Uses 1

Statement usesOrdered representation count

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.