theorem
conv_nonneg
{G : Type u_1}
{R : Type u_2}
[Fintype G]
[DecidableEq G]
[AddCommGroup G]
[OrderedCommSemiring R]
{f g : G → R}
(hf : 0 ≤ f)
(hg : 0 ≤ g)
:
theorem
dconv_nonneg
{G : Type u_1}
{R : Type u_2}
[Fintype G]
[DecidableEq G]
[AddCommGroup G]
[OrderedCommSemiring R]
{f g : G → R}
[StarRing R]
[StarOrderedRing R]
(hf : 0 ≤ f)
(hg : 0 ≤ g)
:
@[simp]
theorem
support_conv
{G : Type u_1}
{R : Type u_2}
[Fintype G]
[DecidableEq G]
[AddCommGroup G]
[StrictOrderedCommSemiring R]
{f g : G → R}
(hf : 0 ≤ f)
(hg : 0 ≤ g)
:
Function.support (f ∗ g) = Function.support f + Function.support g
theorem
conv_pos
{G : Type u_1}
{R : Type u_2}
[Fintype G]
[DecidableEq G]
[AddCommGroup G]
[StrictOrderedCommSemiring R]
{f g : G → R}
(hf : 0 < f)
(hg : 0 < g)
:
@[simp]
theorem
support_dconv
{G : Type u_1}
{R : Type u_2}
[Fintype G]
[DecidableEq G]
[AddCommGroup G]
[StrictOrderedCommSemiring 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
theorem
dconv_pos
{G : Type u_1}
{R : Type u_2}
[Fintype G]
[DecidableEq G]
[AddCommGroup G]
[StrictOrderedCommSemiring R]
{f g : G → R}
[StarRing R]
[StarOrderedRing R]
(hf : 0 < f)
(hg : 0 < g)
:
@[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 : ℕ}
:
@[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 : ℕ}
:
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
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
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.