theorem conv_nonneg {G : Type u_1} {K : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] {f g : G → K} (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ f ∗ g

theorem conv_apply_nonneg {G : Type u_1} {K : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] {f g : G → K} (hf : 0 ≤ f) (hg : 0 ≤ g) (a : G) : 0 ≤ (f ∗ g) a

@[simp]

theorem support_conv {G : Type u_1} {K : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] {f g : G → K} (hf : 0 ≤ f) (hg : 0 ≤ g) : Function.support (f ∗ g) = Function.support f + Function.support g

theorem conv_pos {G : Type u_1} {K : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] {f g : G → K} (hf : 0 < f) (hg : 0 < g) : 0 < f ∗ g

theorem dconv_nonneg {G : Type u_1} {K : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [LinearOrder K] {f g : G → K} [StarRing K] [StarOrderedRing K] (hf : 0 ≤ f) (hg : 0 ≤ g) : 0 ≤ f ○ g

theorem dconv_apply_nonneg {G : Type u_1} {K : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [LinearOrder K] {f g : G → K} [StarRing K] [StarOrderedRing K] (hf : 0 ≤ f) (hg : 0 ≤ g) (a : G) : 0 ≤ (f ○ g) a

@[simp]

theorem support_dconv {G : Type u_1} {K : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] {f g : G → K} [StarRing K] [StarOrderedRing K] (hf : 0 ≤ f) (hg : 0 ≤ g) : Function.support (f ○ g) = Function.support f - Function.support g

theorem dconv_pos {G : Type u_1} {K : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [Semifield K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] {f g : G → K} [StarRing K] [StarOrderedRing K] (hf : 0 < f) (hg : 0 < g) : 0 < f ○ g