Convolution in the compact normalisation

This file defines several versions of the discrete convolution of functions with the compact normalisation.

Main declarations

• nconv: Discrete convolution of two functions in the compact normalisation
• ndconv: Discrete difference convolution of two functions in the compact normalisation
• iterNConv: Iterated convolution of a function in the compact normalisation

Notation

• f ∗ₙ g: Convolution
• f ○ₙ g: Difference convolution
• f ∗^ₙ n: Iterated convolution

Notes

Some lemmas could technically be generalised to a non-commutative semiring domain. Doesn't seem very useful given that the codomain in applications is either ℝ, ℝ≥0 or ℂ.

Similarly we could drop the commutativity asexpectption on the domain, but this is unneeded at this point in time.

TODO

Multiplicativise? Probably ugly and not very useful.

Convolution of functions

In this section, we define the convolution f ∗ₙ g and difference convolution f ○ₙ g of functions f g : α → β, and show how they interact.

def nconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) : α → β

Convolution

Equations

• (f ∗ₙ g) a = Finset.expect (Finset.filter (fun (x : α × α) => x.1 + x.2 = a) Finset.univ) fun (x : α × α) => f x.1 * g x.2

def ndconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) : α → β

Difference convolution

Equations

• (f ○ₙ g) a = Finset.expect (Finset.filter (fun (x : α × α) => x.1 - x.2 = a) Finset.univ) fun (x : α × α) => f x.1 * (starRingEnd (α → β)) g x.2

def trivNChar {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] : α → β

The trivial character.

Equations

• trivNChar a = if a = 0 then ↑(Fintype.card α) else 0

def «term_∗ₙ_» : Lean.TrailingParserDescr

Equations

• «term_∗ₙ_» = Lean.ParserDescr.trailingNode `term_∗ₙ_ 71 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∗ₙ ") (Lean.ParserDescr.cat `term 72))

def «term_○ₙ_» : Lean.TrailingParserDescr

Equations

• «term_○ₙ_» = Lean.ParserDescr.trailingNode `term_○ₙ_ 71 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ○ₙ ") (Lean.ParserDescr.cat `term 72))

theorem nconv_apply {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) (a : α) : (f ∗ₙ g) a = Finset.expect (Finset.filter (fun (x : α × α) => x.1 + x.2 = a) Finset.univ) fun (x : α × α) => f x.1 * g x.2

theorem ndconv_apply {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) (a : α) : (f ○ₙ g) a = Finset.expect (Finset.filter (fun (x : α × α) => x.1 - x.2 = a) Finset.univ) fun (x : α × α) => f x.1 * (starRingEnd (α → β)) g x.2

theorem nconv_apply_eq_smul_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) (a : α) : (f ∗ₙ g) a = (↑(Fintype.card α))⁻¹ • (f ∗ g) a

theorem ndconv_apply_eq_smul_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) (a : α) : (f ○ₙ g) a = (↑(Fintype.card α))⁻¹ • (f ○ g) a

theorem nconv_eq_smul_conv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) : f ∗ₙ g = (↑(Fintype.card α))⁻¹ • (f ∗ g)

theorem ndconv_eq_smul_dconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) : f ○ₙ g = (↑(Fintype.card α))⁻¹ • (f ○ g)

@[simp]

theorem trivNChar_apply {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] (a : α) : trivNChar a = if a = 0 then ↑(Fintype.card α) else 0

@[simp]

theorem nconv_conjneg {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) : f ∗ₙ conjneg g = f ○ₙ g

@[simp]

theorem ndconv_conjneg {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) : f ○ₙ conjneg g = f ∗ₙ g

@[simp]

theorem translate_nconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (a : α) (f : α → β) (g : α → β) : τ a f ∗ₙ g = τ a (f ∗ₙ g)

@[simp]

theorem translate_ndconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (a : α) (f : α → β) (g : α → β) : τ a f ○ₙ g = τ a (f ○ₙ g)

@[simp]

theorem nconv_translate {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (a : α) (f : α → β) (g : α → β) : f ∗ₙ τ a g = τ a (f ∗ₙ g)

@[simp]

theorem ndconv_translate {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (a : α) (f : α → β) (g : α → β) : f ○ₙ τ a g = τ (-a) (f ○ₙ g)

theorem nconv_comm {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) : f ∗ₙ g = g ∗ₙ f

@[simp]

theorem conj_nconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) : (starRingEnd (α → β)) (f ∗ₙ g) = (starRingEnd (α → β)) f ∗ₙ (starRingEnd (α → β)) g

@[simp]

theorem conj_ndconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) : (starRingEnd (α → β)) (f ○ₙ g) = (starRingEnd (α → β)) f ○ₙ (starRingEnd (α → β)) g

@[simp]

theorem conj_trivNChar {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [StarRing β] : (starRingEnd (α → β)) trivNChar = trivNChar

theorem IsSelfAdjoint.nconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] {f : α → β} {g : α → β} (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfAdjoint (f ∗ₙ g)

theorem IsSelfAdjoint.ndconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] {f : α → β} {g : α → β} (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfAdjoint (f ○ₙ g)

@[simp]

theorem isSelfAdjoint_trivNChar {α : Type u_1} {β : Type u_2} [DecidableEq α] [AddCommGroup α] [Semifield β] [StarRing β] : IsSelfAdjoint trivChar

@[simp]

theorem conjneg_nconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) : conjneg (f ∗ₙ g) = conjneg f ∗ₙ conjneg g

@[simp]

theorem conjneg_ndconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) : conjneg (f ○ₙ g) = g ○ₙ f

@[simp]

theorem conjneg_trivNChar {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [StarRing β] : conjneg trivNChar = trivNChar

@[simp]

theorem nconv_zero {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) : f ∗ₙ 0 = 0

@[simp]

theorem zero_nconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) : 0 ∗ₙ f = 0

@[simp]

theorem ndconv_zero {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) : f ○ₙ 0 = 0

@[simp]

theorem zero_ndconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) : 0 ○ₙ f = 0

theorem nconv_add {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) (h : α → β) : f ∗ₙ (g + h) = f ∗ₙ g + f ∗ₙ h

theorem add_nconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) (h : α → β) : (f + g) ∗ₙ h = f ∗ₙ h + g ∗ₙ h

theorem ndconv_add {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) (h : α → β) : f ○ₙ (g + h) = f ○ₙ g + f ○ₙ h

theorem add_ndconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) (h : α → β) : (f + g) ○ₙ h = f ○ₙ h + g ○ₙ h

theorem smul_nconv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [DistribSMul γ β] [IsScalarTower γ β β] [SMulCommClass γ β β] (c : γ) (f : α → β) (g : α → β) : c • f ∗ₙ g = c • (f ∗ₙ g)

theorem smul_ndconv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] [DistribSMul γ β] [IsScalarTower γ β β] [SMulCommClass γ β β] (c : γ) (f : α → β) (g : α → β) : c • f ○ₙ g = c • (f ○ₙ g)

theorem nconv_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [DistribSMul γ β] [IsScalarTower γ β β] [SMulCommClass γ β β] (c : γ) (f : α → β) (g : α → β) : f ∗ₙ c • g = c • (f ∗ₙ g)

theorem ndconv_smul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] [Star γ] [DistribSMul γ β] [IsScalarTower γ β β] [SMulCommClass γ β β] [StarModule γ β] (c : γ) (f : α → β) (g : α → β) : f ○ₙ c • g = star c • (f ○ₙ g)

theorem smul_nconv_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [DistribSMul γ β] [IsScalarTower γ β β] [SMulCommClass γ β β] (c : γ) (f : α → β) (g : α → β) : c • f ∗ₙ g = c • (f ∗ₙ g)

Alias of smul_nconv.

theorem smul_ndconv_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] [DistribSMul γ β] [IsScalarTower γ β β] [SMulCommClass γ β β] (c : γ) (f : α → β) (g : α → β) : c • f ○ₙ g = c • (f ○ₙ g)

Alias of smul_ndconv.

theorem smul_nconv_left_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [DistribSMul γ β] [IsScalarTower γ β β] [SMulCommClass γ β β] (c : γ) (f : α → β) (g : α → β) : f ∗ₙ c • g = c • (f ∗ₙ g)

Alias of nconv_smul.

theorem smul_ndconv_left_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] [Star γ] [DistribSMul γ β] [IsScalarTower γ β β] [SMulCommClass γ β β] [StarModule γ β] (c : γ) (f : α → β) (g : α → β) : f ○ₙ c • g = star c • (f ○ₙ g)

Alias of ndconv_smul.

theorem mul_smul_nconv_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [Monoid γ] [DistribMulAction γ β] [IsScalarTower γ β β] [SMulCommClass γ β β] (c : γ) (d : γ) (f : α → β) (g : α → β) : (c * d) • (f ∗ₙ g) = c • f ∗ₙ d • g

theorem nconv_assoc {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) (h : α → β) : f ∗ₙ g ∗ₙ h = f ∗ₙ (g ∗ₙ h)

theorem nconv_right_comm {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) (h : α → β) : f ∗ₙ g ∗ₙ h = f ∗ₙ h ∗ₙ g

theorem nconv_left_comm {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) (h : α → β) : f ∗ₙ (g ∗ₙ h) = g ∗ₙ (f ∗ₙ h)

theorem nconv_nconv_nconv_comm {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) (h : α → β) (i : α → β) : f ∗ₙ g ∗ₙ (h ∗ₙ i) = f ∗ₙ h ∗ₙ (g ∗ₙ i)

theorem nconv_ndconv_nconv_comm {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) (h : α → β) (i : α → β) : f ∗ₙ g ○ₙ (h ∗ₙ i) = f ○ₙ h ∗ₙ (g ○ₙ i)

theorem ndconv_nconv_ndconv_comm {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) (h : α → β) (i : α → β) : f ○ₙ g ∗ₙ (h ○ₙ i) = f ∗ₙ h ○ₙ (g ∗ₙ i)

theorem ndconv_ndconv_ndconv_comm {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) (h : α → β) (i : α → β) : f ○ₙ g ○ₙ (h ○ₙ i) = f ○ₙ h ○ₙ (g ○ₙ i)

theorem map_nconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] {γ : Type u_4} [Semifield γ] [CharZero γ] [StarRing γ] (m : β →+* γ) (f : α → β) (g : α → β) (a : α) : m ((f ∗ₙ g) a) = (⇑m ∘ f ∗ₙ ⇑m ∘ g) a

theorem comp_nconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] {γ : Type u_4} [Semifield γ] [CharZero γ] [StarRing γ] (m : β →+* γ) (f : α → β) (g : α → β) : ⇑m ∘ (f ∗ₙ g) = ⇑m ∘ f ∗ₙ ⇑m ∘ g

theorem nconv_eq_expect_sub {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) (a : α) : (f ∗ₙ g) a = Finset.expect Finset.univ fun (t : α) => f (a - t) * g t

theorem nconv_eq_expect_add {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) (a : α) : (f ∗ₙ g) a = Finset.expect Finset.univ fun (t : α) => f (a + t) * g (-t)

theorem ndconv_eq_expect_add {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) (a : α) : (f ○ₙ g) a = Finset.expect Finset.univ fun (t : α) => f (a + t) * (starRingEnd β) (g t)

theorem nconv_eq_expect_sub' {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) (a : α) : (f ∗ₙ g) a = Finset.expect Finset.univ fun (t : α) => f t * g (a - t)

theorem ndconv_eq_expect_sub {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) (a : α) : (f ○ₙ g) a = Finset.expect Finset.univ fun (t : α) => f t * (starRingEnd β) (g (t - a))

theorem nconv_eq_expect_add' {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) (a : α) : (f ∗ₙ g) a = Finset.expect Finset.univ fun (t : α) => f (-t) * g (a + t)

theorem nconv_apply_add {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) (a : α) (b : α) : (f ∗ₙ g) (a + b) = Finset.expect Finset.univ fun (t : α) => f (a + t) * g (b - t)

theorem ndconv_apply_neg {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) (a : α) : (f ○ₙ g) (-a) = (starRingEnd β) ((g ○ₙ f) a)

theorem ndconv_apply_sub {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) (a : α) (b : α) : (f ○ₙ g) (a - b) = Finset.expect Finset.univ fun (t : α) => f (a + t) * (starRingEnd β) (g (b + t))

theorem expect_nconv_mul {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) (h : α → β) : (Finset.expect Finset.univ fun (a : α) => (f ∗ₙ g) a * h a) = Finset.expect Finset.univ fun (a : α) => Finset.expect Finset.univ fun (b : α) => f a * g b * h (a + b)

theorem expect_ndconv_mul {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) (h : α → β) : (Finset.expect Finset.univ fun (a : α) => (f ○ₙ g) a * h a) = Finset.expect Finset.univ fun (a : α) => Finset.expect Finset.univ fun (b : α) => f a * (starRingEnd β) (g b) * h (a - b)

theorem expect_nconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) : (Finset.expect Finset.univ fun (a : α) => (f ∗ₙ g) a) = (Finset.expect Finset.univ fun (a : α) => f a) * Finset.expect Finset.univ fun (a : α) => g a

theorem expect_ndconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) : (Finset.expect Finset.univ fun (a : α) => (f ○ₙ g) a) = (Finset.expect Finset.univ fun (a : α) => f a) * Finset.expect Finset.univ fun (a : α) => (starRingEnd β) (g a)

@[simp]

theorem nconv_const {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (b : β) : f ∗ₙ Function.const α b = Function.const α ((Finset.expect Finset.univ fun (x : α) => f x) * b)

@[simp]

theorem const_nconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (b : β) (f : α → β) : Function.const α b ∗ₙ f = Function.const α (b * Finset.expect Finset.univ fun (x : α) => f x)

@[simp]

theorem ndconv_const {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (b : β) : f ○ₙ Function.const α b = Function.const α ((Finset.expect Finset.univ fun (x : α) => f x) * (starRingEnd β) b)

@[simp]

theorem const_ndconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (b : β) (f : α → β) : Function.const α b ○ₙ f = Function.const α (b * Finset.expect Finset.univ fun (x : α) => (starRingEnd β) (f x))

@[simp]

theorem nconv_trivNChar {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) : f ∗ₙ trivNChar = f

@[simp]

theorem trivNChar_nconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) : trivNChar ∗ₙ f = f

@[simp]

theorem ndconv_trivNChar {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [StarRing β] [CharZero β] (f : α → β) : f ○ₙ trivNChar = f

@[simp]

theorem trivNChar_ndconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [StarRing β] [CharZero β] (f : α → β) : trivNChar ○ₙ f = conjneg f

theorem support_nconv_subset {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) : Function.support (f ∗ₙ g) ⊆ Function.support f + Function.support g

theorem support_ndconv_subset {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) : Function.support (f ○ₙ g) ⊆ Function.support f - Function.support g

@[simp]

theorem nconv_neg {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Field β] [CharZero β] (f : α → β) (g : α → β) : f ∗ₙ -g = -(f ∗ₙ g)

@[simp]

theorem neg_nconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Field β] [CharZero β] (f : α → β) (g : α → β) : -f ∗ₙ g = -(f ∗ₙ g)

@[simp]

theorem ndconv_neg {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Field β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) : f ○ₙ -g = -(f ○ₙ g)

@[simp]

theorem neg_ndconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Field β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) : -f ○ₙ g = -(f ○ₙ g)

theorem nconv_sub {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Field β] [CharZero β] (f : α → β) (g : α → β) (h : α → β) : f ∗ₙ (g - h) = f ∗ₙ g - f ∗ₙ h

theorem sub_nconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Field β] [CharZero β] (f : α → β) (g : α → β) (h : α → β) : (f - g) ∗ₙ h = f ∗ₙ h - g ∗ₙ h

theorem ndconv_sub {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Field β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) (h : α → β) : f ○ₙ (g - h) = f ○ₙ g - f ○ₙ h

theorem sub_ndconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Field β] [CharZero β] [StarRing β] (f : α → β) (g : α → β) (h : α → β) : (f - g) ○ₙ h = f ○ₙ h - g ○ₙ h

@[simp]

theorem indicate_univ_nconv_indicate_univ {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] : 𝟭 Finset.univ ∗ₙ 𝟭 Finset.univ = 𝟭 Finset.univ

@[simp]

theorem indicate_univ_ndconv_mu_univ {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [StarRing β] [CharZero β] : 𝟭 Finset.univ ○ₙ 𝟭 Finset.univ = 𝟭 Finset.univ

@[simp]

theorem balance_nconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Field β] [CharZero β] (f : α → β) (g : α → β) : Finset.balance (f ∗ₙ g) = Finset.balance f ∗ₙ Finset.balance g

@[simp]

theorem balance_ndconv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Field β] [StarRing β] [CharZero β] (f : α → β) (g : α → β) : Finset.balance (f ○ₙ g) = Finset.balance f ○ₙ Finset.balance g

@[simp]

theorem RCLike.coe_nconv {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] {𝕜 : Type} [RCLike 𝕜] (f : α → ℝ) (g : α → ℝ) (a : α) : ↑((f ∗ₙ g) a) = (RCLike.ofReal ∘ f ∗ₙ RCLike.ofReal ∘ g) a

@[simp]

theorem RCLike.coe_ndconv {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] {𝕜 : Type} [RCLike 𝕜] (f : α → ℝ) (g : α → ℝ) (a : α) : ↑((f ○ₙ g) a) = (RCLike.ofReal ∘ f ○ₙ RCLike.ofReal ∘ g) a

@[simp]

theorem RCLike.coe_comp_nconv {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] {𝕜 : Type} [RCLike 𝕜] (f : α → ℝ) (g : α → ℝ) : RCLike.ofReal ∘ (f ∗ₙ g) = RCLike.ofReal ∘ f ∗ₙ RCLike.ofReal ∘ g

@[simp]

theorem RCLike.coe_comp_ndconv {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] {𝕜 : Type} [RCLike 𝕜] (f : α → ℝ) (g : α → ℝ) : RCLike.ofReal ∘ (f ○ₙ g) = RCLike.ofReal ∘ f ○ₙ RCLike.ofReal ∘ g

@[simp]

theorem Complex.coe_nconv {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] (f : α → ℝ) (g : α → ℝ) (a : α) : ↑((f ∗ₙ g) a) = (Complex.ofReal' ∘ f ∗ₙ Complex.ofReal' ∘ g) a

@[simp]

theorem Complex.coe_ndconv {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] (f : α → ℝ) (g : α → ℝ) (a : α) : ↑((f ○ₙ g) a) = (Complex.ofReal' ∘ f ○ₙ Complex.ofReal' ∘ g) a

@[simp]

theorem Complex.coe_comp_nconv {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] (f : α → ℝ) (g : α → ℝ) : Complex.ofReal' ∘ (f ∗ₙ g) = Complex.ofReal' ∘ f ∗ₙ Complex.ofReal' ∘ g

@[simp]

theorem Complex.coe_comp_ndconv {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] (f : α → ℝ) (g : α → ℝ) : Complex.ofReal' ∘ (f ○ₙ g) = Complex.ofReal' ∘ f ○ₙ Complex.ofReal' ∘ g

@[simp]

theorem NNReal.coe_nconv {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] (f : α → NNReal) (g : α → NNReal) (a : α) : ↑((f ∗ₙ g) a) = (NNReal.toReal ∘ f ∗ₙ NNReal.toReal ∘ g) a

@[simp]

theorem NNReal.coe_ndconv {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] (f : α → NNReal) (g : α → NNReal) (a : α) : ↑((f ○ₙ g) a) = (NNReal.toReal ∘ f ○ₙ NNReal.toReal ∘ g) a

@[simp]

theorem NNReal.coe_comp_nconv {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] (f : α → NNReal) (g : α → NNReal) : NNReal.toReal ∘ (f ∗ₙ g) = NNReal.toReal ∘ f ∗ₙ NNReal.toReal ∘ g

@[simp]

theorem NNReal.coe_comp_ndconv {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] (f : α → NNReal) (g : α → NNReal) : NNReal.toReal ∘ (f ○ₙ g) = NNReal.toReal ∘ f ○ₙ NNReal.toReal ∘ g

Iterated convolution

def iterNConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) : ℕ → α → β

Iterated convolution.

Equations

• f ∗^ₙ 0 = trivNChar
• f ∗^ₙ Nat.succ n = f ∗^ₙ n ∗ₙ f

def «term_∗^ₙ_» : Lean.TrailingParserDescr

Equations

• «term_∗^ₙ_» = Lean.ParserDescr.trailingNode `term_∗^ₙ_ 78 78 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∗^ₙ ") (Lean.ParserDescr.cat `term 79))

@[simp]

theorem iterNConv_zero {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) : f ∗^ₙ 0 = trivNChar

@[simp]

theorem iterNConv_one {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) : f ∗^ₙ 1 = f

theorem iterNConv_succ {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (n : ℕ) : f ∗^ₙ (n + 1) = f ∗^ₙ n ∗ₙ f

theorem iterNConv_succ' {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (n : ℕ) : f ∗^ₙ (n + 1) = f ∗ₙ f ∗^ₙ n

theorem iterNConv_add {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (m : ℕ) (n : ℕ) : f ∗^ₙ (m + n) = f ∗^ₙ m ∗ₙ f ∗^ₙ n

theorem iterNConv_mul {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (m : ℕ) (n : ℕ) : f ∗^ₙ (m * n) = f ∗^ₙ m ∗^ₙ n

theorem iterNConv_mul' {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (m : ℕ) (n : ℕ) : f ∗^ₙ (m * n) = f ∗^ₙ n ∗^ₙ m

@[simp]

theorem conj_iterNConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [StarRing β] [CharZero β] (f : α → β) (n : ℕ) : (starRingEnd (α → β)) (f ∗^ₙ n) = (starRingEnd (α → β)) f ∗^ₙ n

@[simp]

theorem conjneg_iterNConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [StarRing β] [CharZero β] (f : α → β) (n : ℕ) : conjneg (f ∗^ₙ n) = conjneg f ∗^ₙ n

theorem iterNConv_nconv_distrib {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (g : α → β) (n : ℕ) : (f ∗ₙ g) ∗^ₙ n = f ∗^ₙ n ∗ₙ g ∗^ₙ n

theorem iterNConv_ndconv_distrib {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [StarRing β] [CharZero β] (f : α → β) (g : α → β) (n : ℕ) : (f ○ₙ g) ∗^ₙ n = f ∗^ₙ n ○ₙ g ∗^ₙ n

@[simp]

theorem zero_iterNConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] {n : ℕ} : n ≠ 0 → 0 ∗^ₙ n = 0

@[simp]

theorem smul_iterNConv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] [Monoid γ] [DistribMulAction γ β] [IsScalarTower γ β β] [SMulCommClass γ β β] (c : γ) (f : α → β) (n : ℕ) : (c • f) ∗^ₙ n = c ^ n • f ∗^ₙ n

theorem comp_iterNConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] {γ : Type u_4} [Semifield γ] [CharZero γ] [StarRing γ] (m : β →+* γ) (f : α → β) (n : ℕ) : ⇑m ∘ (f ∗^ₙ n) = ⇑m ∘ f ∗^ₙ n

theorem map_iterNConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] {γ : Type u_4} [Semifield γ] [CharZero γ] [StarRing γ] (m : β →+* γ) (f : α → β) (a : α) (n : ℕ) : m ((f ∗^ₙ n) a) = (⇑m ∘ f ∗^ₙ n) a

theorem expect_iterNConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (n : ℕ) : (Finset.expect Finset.univ fun (a : α) => (f ∗^ₙ n) a) = (Finset.expect Finset.univ fun (a : α) => f a) ^ n

@[simp]

theorem iterNConv_trivNChar {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (n : ℕ) : trivNChar ∗^ₙ n = trivNChar

theorem support_iterNConv_subset {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Semifield β] [CharZero β] (f : α → β) (n : ℕ) : Function.support (f ∗^ₙ n) ⊆ n • Function.support f

@[simp]

theorem balance_iterNConv {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [AddCommGroup α] [Field β] [CharZero β] (f : α → β) {n : ℕ} : n ≠ 0 → Finset.balance (f ∗^ₙ n) = Finset.balance f ∗^ₙ n

@[simp]

theorem NNReal.coe_iterNConv {α : Type u_1} [Fintype α] [DecidableEq α] [AddCommGroup α] (f : α → NNReal) (n : ℕ) (a : α) : ↑((f ∗^ₙ n) a) = (NNReal.toReal ∘ f ∗^ₙ n) a