Convolution of Functions on ℕ

This file defines the sum (∗) convolution of functions ℕ → R.

Main Definitions

• AdditiveCombinatorics.sumConv: The sum convolution f ∗ g.

Notation

• f ∗ g for sumConv f g.

TODO

• f ∘ g for diffConv f g.

def AdditiveCombinatorics.sumConv {R : Type u_1} [Semiring R] (f g : ℕ → R) (n : ℕ) : R

The sum convolution of two functions f, g : ℕ → R, also known as the Cauchy product. (f ∗ g) n = ∑_{a+b=n} f(a)g(b).

Equations

• (f ∗ g) n = ∑ p ∈ Finset.antidiagonal n, f p.1 * g p.2

def AdditiveCombinatorics.«term_∗_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AdditiveCombinatorics.sumRep (A : Set ℕ) : ℕ → ℕ

The number of sum representations is the sum convolution of A's indicator function with itself.

Equations

• AdditiveCombinatorics.sumRep A = A.indicatorOne ∗ A.indicatorOne

@[simp]

theorem AdditiveCombinatorics.sumRep_def (A : Set ℕ) (n : ℕ) : sumRep A n = (Finset.filter (fun (p : ℕ × ℕ) => p.1 ∈ A ∧ p.2 ∈ A) (Finset.antidiagonal n)).card

theorem AdditiveCombinatorics.sumRep_eq_powerSeries_coeff (A : Set ℕ) (n : ℕ) : sumRep A n = (PowerSeries.coeff ℕ n) (PowerSeries.mk A.indicatorOne * PowerSeries.mk A.indicatorOne)