Convolution in the compact normalisation

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

Main declarations

• conv: Discrete convolution of two functions in the compact normalisation
• dconv: Discrete difference convolution of two functions in the compact normalisation
• iterConv: 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 division ring. Doesn't seem very useful given that the codomain in applications is either ℝ, ℝ≥0 or ℂ.

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

def conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) : G → K

Compact convolution on a finite group.

The value of f ∗ g at a is the average of the value of f b * g c over b + c = a.

Equations

• (f ∗ g) a = {x : G × G | x.1 + x.2 = a}.expect fun (x : G × G) => f x.1 * g x.2

def «term_∗_» : Lean.TrailingParserDescr

Compact convolution on a finite group.

The value of f ∗ g at a is the average of the value of f b * g c over b + c = a.

Equations

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

theorem conv_apply {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) (a : G) : (f ∗ g) a = {x : G × G | x.1 + x.2 = a}.expect fun (x : G × G) => f x.1 * g x.2

theorem conv_eq_smul_sum {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) (a : G) : (f ∗ g) a = (↑(Fintype.card G))⁻¹ • ∑ x : G × G with x.1 + x.2 = a, f x.1 * g x.2

@[simp]

theorem conv_zero {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f : G → K) : f ∗ 0 = 0

@[simp]

theorem zero_conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f : G → K) : 0 ∗ f = 0

theorem conv_add {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g h : G → K) : f ∗ (g + h) = f ∗ g + f ∗ h

theorem add_conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g h : G → K) : (f + g) ∗ h = f ∗ h + g ∗ h

theorem smul_conv {G : Type u_1} {H : Type u_2} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [DistribSMul H K] [IsScalarTower H K K] [SMulCommClass H K K] (c : H) (f g : G → K) : c • f ∗ g = c • (f ∗ g)

theorem conv_smul {G : Type u_1} {H : Type u_2} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [DistribSMul H K] [SMulCommClass H K K] (c : H) (f g : G → K) : f ∗ c • g = c • (f ∗ g)

theorem smul_conv_assoc {G : Type u_1} {H : Type u_2} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [DistribSMul H K] [IsScalarTower H K K] [SMulCommClass H K K] (c : H) (f g : G → K) : c • f ∗ g = c • (f ∗ g)

Alias of smul_conv.

theorem smul_conv_left_comm {G : Type u_1} {H : Type u_2} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [DistribSMul H K] [SMulCommClass H K K] (c : H) (f g : G → K) : f ∗ c • g = c • (f ∗ g)

Alias of conv_smul.

@[simp]

theorem translate_conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (a : G) (f g : G → K) : translate a f ∗ g = translate a (f ∗ g)

@[simp]

theorem conv_translate {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (a : G) (f g : G → K) : f ∗ translate a g = translate a (f ∗ g)

theorem conv_comm {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) : f ∗ g = g ∗ f

theorem mul_smul_conv_comm {G : Type u_1} {H : Type u_2} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [Monoid H] [DistribMulAction H K] [IsScalarTower H K K] [SMulCommClass H K K] (c d : H) (f g : G → K) : (c * d) • (f ∗ g) = c • f ∗ d • g

theorem conv_assoc {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g h : G → K) : f ∗ g ∗ h = f ∗ (g ∗ h)

theorem conv_right_comm {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g h : G → K) : f ∗ g ∗ h = f ∗ h ∗ g

theorem conv_left_comm {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g h : G → K) : f ∗ (g ∗ h) = g ∗ (f ∗ h)

theorem conv_conv_conv_comm {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g h i : G → K) : f ∗ g ∗ (h ∗ i) = f ∗ h ∗ (g ∗ i)

theorem map_conv {G : Type u_1} {K : Type u_3} {L : Type u_4} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [Semifield L] [CharZero L] (m : K →+* L) (f g : G → K) (a : G) : m ((f ∗ g) a) = (⇑m ∘ f ∗ ⇑m ∘ g) a

theorem comp_conv {G : Type u_1} {K : Type u_3} {L : Type u_4} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [Semifield L] [CharZero L] (m : K →+* L) (f g : G → K) : ⇑m ∘ (f ∗ g) = ⇑m ∘ f ∗ ⇑m ∘ g

theorem conv_eq_expect_sub {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) (a : G) : (f ∗ g) a = Finset.univ.expect fun (t : G) => f (a - t) * g t

theorem conv_eq_expect_add {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) (a : G) : (f ∗ g) a = Finset.univ.expect fun (t : G) => f (a + t) * g (-t)

theorem conv_eq_expect_sub' {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) (a : G) : (f ∗ g) a = Finset.univ.expect fun (t : G) => f t * g (a - t)

theorem conv_eq_expect_add' {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) (a : G) : (f ∗ g) a = Finset.univ.expect fun (t : G) => f (-t) * g (a + t)

theorem conv_apply_add {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) (a b : G) : (f ∗ g) (a + b) = Finset.univ.expect fun (t : G) => f (a + t) * g (b - t)

theorem expect_conv_mul {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g h : G → K) : (Finset.univ.expect fun (a : G) => (f ∗ g) a * h a) = Finset.univ.expect fun (a : G) => Finset.univ.expect fun (b : G) => f a * g b * h (a + b)

theorem expect_conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) : (Finset.univ.expect fun (a : G) => (f ∗ g) a) = (Finset.univ.expect fun (a : G) => f a) * Finset.univ.expect fun (a : G) => g a

@[simp]

theorem conv_const {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f : G → K) (b : K) : f ∗ Function.const G b = Function.const G ((Finset.univ.expect fun (x : G) => f x) * b)

@[simp]

theorem const_conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (b : K) (f : G → K) : Function.const G b ∗ f = Function.const G (b * Finset.univ.expect fun (x : G) => f x)

theorem support_conv_subset {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f g : G → K) : Function.support (f ∗ g) ⊆ Function.support f + Function.support g

theorem indicator_one_conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (s : Finset G) (f : G → K) : ((↑s).indicator fun (x : G) => 1) ∗ f = (↑(Fintype.card G))⁻¹ • ∑ a ∈ s, translate a f

theorem conv_indicator_one {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (f : G → K) (s : Finset G) : (f ∗ (↑s).indicator fun (x : G) => 1) = (↑(Fintype.card G))⁻¹ • ∑ a ∈ s, translate a f

theorem indicator_one_conv_indicator_one_eq_dens {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] (s t : Finset G) (a : G) : (((↑s).indicator fun (x : G) => 1) ∗ (↑t).indicator fun (x : G) => 1) a = ↑(s ∩ (a +ᵥ -t)).dens

def dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) : G → K

Compact difference convolution on a finite group.

The value of f ∗ g at a is the average of the value of f b * g c over b - c = a.

Equations

• (f ○ g) a = {x : G × G | x.1 - x.2 = a}.expect fun (x : G × G) => f x.1 * (starRingEnd (G → K)) g x.2

def «term_○_» : Lean.TrailingParserDescr

Compact difference convolution on a finite group.

The value of f ∗ g at a is the average of the value of f b * g c over b - c = a.

Equations

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

theorem dconv_apply {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) (a : G) : (f ○ g) a = {x : G × G | x.1 - x.2 = a}.expect fun (x : G × G) => f x.1 * (starRingEnd (G → K)) g x.2

theorem dconv_eq_smul_sum {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) (a : G) : (f ○ g) a = (↑(Fintype.card G))⁻¹ • ∑ x : G × G with x.1 - x.2 = a, f x.1 * (starRingEnd (G → K)) g x.2

@[simp]

theorem conv_conjneg {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) : f ∗ conjneg g = f ○ g

@[simp]

theorem dconv_conjneg {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) : f ○ conjneg g = f ∗ g

@[simp]

theorem translate_dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (a : G) (f g : G → K) : translate a f ○ g = translate a (f ○ g)

@[simp]

theorem dconv_translate {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (a : G) (f g : G → K) : f ○ translate a g = translate (-a) (f ○ g)

@[simp]

theorem conj_conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) : (starRingEnd (G → K)) (f ∗ g) = (starRingEnd (G → K)) f ∗ (starRingEnd (G → K)) g

@[simp]

theorem conj_dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) : (starRingEnd (G → K)) (f ○ g) = (starRingEnd (G → K)) f ○ (starRingEnd (G → K)) g

theorem IsSelfAdjoint.conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] {f g : G → K} [StarRing K] (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfAdjoint (f ∗ g)

theorem IsSelfAdjoint.dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] {f g : G → K} [StarRing K] (hf : IsSelfAdjoint f) (hg : IsSelfAdjoint g) : IsSelfAdjoint (f ○ g)

@[simp]

theorem conjneg_conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) : conjneg (f ∗ g) = conjneg f ∗ conjneg g

@[simp]

theorem conjneg_dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) : conjneg (f ○ g) = g ○ f

@[simp]

theorem dconv_zero {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f : G → K) : f ○ 0 = 0

@[simp]

theorem zero_dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f : G → K) : 0 ○ f = 0

theorem dconv_add {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g h : G → K) : f ○ (g + h) = f ○ g + f ○ h

theorem add_dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g h : G → K) : (f + g) ○ h = f ○ h + g ○ h

theorem smul_dconv {G : Type u_1} {H : Type u_2} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] [DistribSMul H K] [IsScalarTower H K K] [SMulCommClass H K K] (c : H) (f g : G → K) : c • f ○ g = c • (f ○ g)

theorem dconv_smul {G : Type u_1} {H : Type u_2} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] [Star H] [DistribSMul H K] [SMulCommClass H K K] [StarModule H K] (c : H) (f g : G → K) : f ○ c • g = star c • (f ○ g)

theorem smul_dconv_assoc {G : Type u_1} {H : Type u_2} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] [DistribSMul H K] [IsScalarTower H K K] [SMulCommClass H K K] (c : H) (f g : G → K) : c • f ○ g = c • (f ○ g)

Alias of smul_dconv.

theorem smul_dconv_left_comm {G : Type u_1} {H : Type u_2} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] [Star H] [DistribSMul H K] [SMulCommClass H K K] [StarModule H K] (c : H) (f g : G → K) : f ○ c • g = star c • (f ○ g)

Alias of dconv_smul.

theorem conv_dconv_conv_comm {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g h i : G → K) : f ∗ g ○ (h ∗ i) = f ○ h ∗ (g ○ i)

theorem dconv_conv_dconv_comm {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g h i : G → K) : f ○ g ∗ (h ○ i) = f ∗ h ○ (g ∗ i)

theorem dconv_dconv_dconv_comm {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g h i : G → K) : f ○ g ○ (h ○ i) = f ○ h ○ (g ○ i)

theorem dconv_eq_expect_add {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) (a : G) : (f ○ g) a = Finset.univ.expect fun (t : G) => f (a + t) * (starRingEnd K) (g t)

theorem dconv_eq_expect_sub {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) (a : G) : (f ○ g) a = Finset.univ.expect fun (t : G) => f t * (starRingEnd K) (g (t - a))

theorem dconv_apply_neg {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) (a : G) : (f ○ g) (-a) = (starRingEnd K) ((g ○ f) a)

theorem dconv_apply_sub {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) (a b : G) : (f ○ g) (a - b) = Finset.univ.expect fun (t : G) => f (a + t) * (starRingEnd K) (g (b + t))

theorem expect_dconv_mul {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g h : G → K) : (Finset.univ.expect fun (a : G) => (f ○ g) a * h a) = Finset.univ.expect fun (a : G) => Finset.univ.expect fun (b : G) => f a * (starRingEnd K) (g b) * h (a - b)

theorem expect_dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) : (Finset.univ.expect fun (a : G) => (f ○ g) a) = (Finset.univ.expect fun (a : G) => f a) * Finset.univ.expect fun (a : G) => (starRingEnd K) (g a)

@[simp]

theorem dconv_const {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f : G → K) (b : K) : f ○ Function.const G b = Function.const G ((Finset.univ.expect fun (x : G) => f x) * (starRingEnd K) b)

@[simp]

theorem const_dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (b : K) (f : G → K) : Function.const G b ○ f = Function.const G (b * Finset.univ.expect fun (x : G) => (starRingEnd K) (f x))

theorem support_dconv_subset {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f g : G → K) : Function.support (f ○ g) ⊆ Function.support f - Function.support g

theorem indicator_one_dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (s : Finset G) (f : G → K) : ((↑s).indicator fun (x : G) => 1) ○ f = (↑(Fintype.card G))⁻¹ • ∑ a ∈ s, translate a (conjneg f)

theorem dconv_indicator_one {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (f : G → K) (s : Finset G) : (f ○ (↑s).indicator fun (x : G) => 1) = (↑(Fintype.card G))⁻¹ • ∑ a ∈ s, translate (-a) f

theorem indicator_one_dconv_indicator_one_eq_dens {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (s t : Finset G) (a : G) : (((↑s).indicator fun (x : G) => 1) ○ (↑t).indicator fun (x : G) => 1) a = ↑(s ∩ (a +ᵥ t)).dens

theorem indicator_one_dconv_indicator_one_eq_addConvolution_div {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (s t : Finset G) (a : G) : (((↑s).indicator fun (x : G) => 1) ○ (↑t).indicator fun (x : G) => 1) a = ↑(s.addConvolution (-t) a) / ↑(Fintype.card G)

theorem expect_indicator_one_dconv_indicator_one {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (s t : Finset G) : (Finset.univ.expect fun (a : G) => (((↑s).indicator fun (x : G) => 1) ○ (↑t).indicator fun (x : G) => 1) a) = ↑s.dens * ↑t.dens

theorem expect_indicator_one_dconv_indicator_sq {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [StarRing K] (s t : Finset G) : (Finset.univ.expect fun (x : G) => (((↑s).indicator fun (x : G) => 1) ○ (↑t).indicator fun (x : G) => 1) x ^ 2) = ↑(s.addEnergy' t)

@[simp]

theorem conv_neg {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field K] [CharZero K] (f g : G → K) : f ∗ -g = -(f ∗ g)

@[simp]

theorem neg_conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field K] [CharZero K] (f g : G → K) : -f ∗ g = -(f ∗ g)

theorem conv_sub {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field K] [CharZero K] (f g h : G → K) : f ∗ (g - h) = f ∗ g - f ∗ h

theorem sub_conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field K] [CharZero K] (f g h : G → K) : (f - g) ∗ h = f ∗ h - g ∗ h

@[simp]

theorem balance_conv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field K] [CharZero K] (f g : G → K) : Fintype.balance (f ∗ g) = Fintype.balance f ∗ Fintype.balance g

@[simp]

theorem dconv_neg {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field K] [CharZero K] [StarRing K] (f g : G → K) : f ○ -g = -(f ○ g)

@[simp]

theorem neg_dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field K] [CharZero K] [StarRing K] (f g : G → K) : -f ○ g = -(f ○ g)

theorem dconv_sub {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field K] [CharZero K] [StarRing K] (f g h : G → K) : f ○ (g - h) = f ○ g - f ○ h

theorem sub_dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field K] [CharZero K] [StarRing K] (f g h : G → K) : (f - g) ○ h = f ○ h - g ○ h

@[simp]

theorem balance_dconv {G : Type u_1} {K : Type u_3} [Fintype G] [DecidableEq G] [AddCommGroup G] [Field K] [CharZero K] [StarRing K] (f g : G → K) : Fintype.balance (f ○ g) = Fintype.balance f ○ Fintype.balance g

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Complex.ofReal_comp_conv {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] (f g : G → ℝ) : ofReal ∘ (f ∗ g) = ofReal ∘ f ∗ ofReal ∘ g

@[simp]

theorem Complex.ofReal_comp_dconv {G : Type u_1} [Fintype G] [DecidableEq G] [AddCommGroup G] (f g : G → ℝ) : ofReal ∘ (f ○ g) = ofReal ∘ f ○ ofReal ∘ g

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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