APAP.Prereqs.Convolution.Order

source

theorem ddconv_nonneg {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] [PartialOrder R] [IsOrderedRing R] {f g : G → R} (hf : 0 ≤ f) (hg : 0 ≤ g) :

0 ≤ f ∗ᵈ g

source

theorem ddconv_apply_nonneg {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] [PartialOrder R] [IsOrderedRing R] {f g : G → R} (hf : 0 ≤ f) (hg : 0 ≤ g) (a : G) :

0 ≤ (f ∗ᵈ g) a

source

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

0 ≤ f ○ᵈ g

source

theorem dddconv_apply_nonneg {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] [PartialOrder R] [IsOrderedRing R] {f g : G → R} [StarRing R] [StarOrderedRing R] (hf : 0 ≤ f) (hg : 0 ≤ g) (a : G) :

0 ≤ (f ○ᵈ g) a

source

@[simp]

theorem support_ddconv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {f g : G → R} (hf : 0 ≤ f) (hg : 0 ≤ g) :

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

source

theorem ddconv_pos {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {f g : G → R} (hf : 0 < f) (hg : 0 < g) :

0 < f ∗ᵈ g

source

@[simp]

theorem support_dddconv {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {f 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 dddconv_pos {G : Type u_1} {R : Type u_2} [Fintype G] [DecidableEq G] [AddCommGroup G] [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] {f 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] [CommSemiring R] [PartialOrder R] [IsOrderedRing 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] [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] [StarRing R] [StarOrderedRing R] {f : G → R} (hf : 0 < f) {n : ℕ} :

0 < f ∗ᵈ^ n

source

def Mathlib.Meta.Positivity.evalConv :

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 :

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 :

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