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