/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import FormalConjecturesForMathlib.Algebra.Group.Indicator
public import Mathlib.RingTheory.PowerSeries.Basic@[expose] public sectionConvolution 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.
namespace AdditiveCombinatoricsopen Finset Setvariable {R : Type*} [Semiring 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).
def sumConv (f g : ℕ → R) (n : ℕ) : R := ∑ p ∈ antidiagonal n, f p.1 * g p.2infixl:70 " ∗ " => sumConv
The number of sum representations is the sum convolution of A's indicator
function with itself: $1_A\ast 1_A(n)$.
noncomputable def sumRep (A : Set ℕ) : ℕ → ℕ := (𝟙_A ∗ 𝟙_A)open scoped Classical in
@[simp]
lemma sumRep_def (A : Set ℕ) (n : ℕ) :
sumRep A n = ((antidiagonal n).filter (fun (p : ℕ × ℕ) ↦ p.1 ∈ A ∧ p.2 ∈ A)).card := A:Set ℕn:ℕ⊢ sumRep A n = #({p ∈ antidiagonal n | p.1 ∈ A ∧ p.2 ∈ A})
A:Set ℕn:ℕ⊢ (∑ x ∈ antidiagonal n, if x.2 ∈ A then if x.1 ∈ A then 1 else 0 else 0) = #({p ∈ antidiagonal n | p.1 ∈ A ∧ p.2 ∈ A})
A:Set ℕn:ℕ⊢ (∑ x ∈ antidiagonal n, if x.1 ∈ A ∧ x.2 ∈ A then 1 else 0) = ∑ i ∈ antidiagonal n, if i.1 ∈ A ∧ i.2 ∈ A then 1 else 0
All goals completed! 🐙open PowerSeriestheorem sumRep_eq_powerSeries_coeff (A : Set ℕ) (n : ℕ) : (sumRep A n : ℕ) =
((PowerSeries.mk (𝟙_A)) * (PowerSeries.mk (𝟙_A)) : PowerSeries ℕ).coeff n := A:Set ℕn:ℕ⊢ sumRep A n = (coeff n) (PowerSeries.mk (𝟙_A) * PowerSeries.mk (𝟙_A))
All goals completed! 🐙end AdditiveCombinatorics