LeanAPAP.Prereqs.Convolution.Order

source

theorem conv_nonneg {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [OrderedCommSemiring R] {f : G → R} {g : G → R} (hf : 0 ≤ f) (hg : 0 ≤ g) :

0 ≤ f ∗ g

source

theorem dconv_nonneg {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [OrderedCommSemiring R] {f : G → R} {g : G → R} [StarRing R] [StarOrderedRing R] (hf : 0 ≤ f) (hg : 0 ≤ g) :

0 ≤ f ○ g

source

@[simp]

theorem support_conv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [StrictOrderedCommSemiring R] {f : G → R} {g : G → R} (hf : 0 ≤ f) (hg : 0 ≤ g) :

Function.support (f ∗ g) = Function.support f + Function.support g

source

theorem conv_pos {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [StrictOrderedCommSemiring R] {f : G → R} {g : G → R} (hf : 0 < f) (hg : 0 < g) :

0 < f ∗ g

source

@[simp]

theorem support_dconv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [StrictOrderedCommSemiring R] {f : G → R} {g : G → R} [StarRing R] [StarOrderedRing R] (hf : 0 ≤ f) (hg : 0 ≤ g) :

Function.support (f ○ g) = Function.support f - Function.support g

source

theorem dconv_pos {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [StrictOrderedCommSemiring R] {f : G → R} {g : G → R} [StarRing R] [StarOrderedRing R] (hf : 0 < f) (hg : 0 < g) :

0 < f ○ g

source

@[simp]

theorem iterConv_nonneg {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [OrderedCommSemiring R] {f : G → R} (hf : 0 ≤ f) {n : ℕ} :

0 ≤ f ∗^ n

source

@[simp]

theorem iterConv_pos {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [StrictOrderedCommSemiring R] [StarRing R] [StarOrderedRing R] {f : G → R} (hf : 0 < f) {n : ℕ} :

0 < f ∗^ n

source

def Mathlib.Meta.Positivity.evalConv :

Mathlib.Meta.Positivity.PositivityExt

The positivity extension which identifies expressions of the form f ∗ g, such that positivity successfully recognises both f and g.

Equations

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

Instances For

source

def Mathlib.Meta.Positivity.evalDConv :

Mathlib.Meta.Positivity.PositivityExt

The positivity extension which identifies expressions of the form f ○ g, such that positivity successfully recognises both f and g.

Equations

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

Instances For

source

def Mathlib.Meta.Positivity.evalIterConv :

Mathlib.Meta.Positivity.PositivityExt

The positivity extension which identifies expressions of the form f ○ g, such that positivity successfully recognises both f and g.

Equations

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

Instances For