Indicator function #
indicator (s : Set α) (f : α → β) (a : α)→ β) (a : α)isf aifa ∈ s∈ sand is0otherwise.mulIndicator (s : Set α) (f : α → β) (a : α)→ β) (a : α)isf aifa ∈ s∈ sand is1otherwise.
Implementation note #
In mathematics, an indicator function or a characteristic function is a function
used to indicate membership of an element in a set s,
having the value 1 for all elements of s and the value 0 otherwise.
But since it is usually used to restrict a function to a certain set s,
we let the indicator function take the value f x for some function f, instead of 1.
If the usual indicator function is needed, just set f to be the constant function λx, 1.
The indicator function is implemented non-computably, to avoid having to pass around Decidable
arguments. This is in contrast with the design of Pi.Single or Set.Piecewise.
Tags #
indicator, characteristic
noncomputable def
Set.indicator
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
(s : Set α)
(f : α → M)
:
α → M
indicator s f a is f a if a ∈ s∈ s, 0 otherwise.
Equations
- Set.indicator s f x = let x := x; if x ∈ s then f x else 0
noncomputable def
Set.mulIndicator
{α : Type u_1}
{M : Type u_2}
[inst : One M]
(s : Set α)
(f : α → M)
:
α → M
mulIndicator s f a is f a if a ∈ s∈ s, 1 otherwise.
Equations
- Set.mulIndicator s f x = let x := x; if x ∈ s then f x else 1
@[simp]
theorem
Set.piecewise_eq_indicator
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{s : Set α}
{f : α → M}
[inst : DecidablePred fun x => x ∈ s]
:
Set.piecewise s f 0 = Set.indicator s f
@[simp]
theorem
Set.piecewise_eq_mulIndicator
{α : Type u_1}
{M : Type u_2}
[inst : One M]
{s : Set α}
{f : α → M}
[inst : DecidablePred fun x => x ∈ s]
:
Set.piecewise s f 1 = Set.mulIndicator s f
@[simp]
theorem
Set.indicator_of_mem
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{s : Set α}
{a : α}
(h : a ∈ s)
(f : α → M)
:
Set.indicator s f a = f a
@[simp]
theorem
Set.mulIndicator_of_mem
{α : Type u_1}
{M : Type u_2}
[inst : One M]
{s : Set α}
{a : α}
(h : a ∈ s)
(f : α → M)
:
Set.mulIndicator s f a = f a
theorem
Set.indicator_eq_zero_or_self
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
(s : Set α)
(f : α → M)
(a : α)
:
Set.indicator s f a = 0 ∨ Set.indicator s f a = f a
theorem
Set.mulIndicator_eq_one_or_self
{α : Type u_1}
{M : Type u_2}
[inst : One M]
(s : Set α)
(f : α → M)
(a : α)
:
Set.mulIndicator s f a = 1 ∨ Set.mulIndicator s f a = f a
@[simp]
theorem
Set.indicator_eq_self
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{s : Set α}
{f : α → M}
:
Set.indicator s f = f ↔ Function.support f ⊆ s
@[simp]
theorem
Set.mulIndicator_eq_self
{α : Type u_1}
{M : Type u_2}
[inst : One M]
{s : Set α}
{f : α → M}
:
Set.mulIndicator s f = f ↔ Function.mulSupport f ⊆ s
theorem
Set.indicator_eq_self_of_superset
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{s : Set α}
{t : Set α}
{f : α → M}
(h1 : Set.indicator s f = f)
(h2 : s ⊆ t)
:
Set.indicator t f = f
theorem
Set.mulIndicator_eq_self_of_superset
{α : Type u_1}
{M : Type u_2}
[inst : One M]
{s : Set α}
{t : Set α}
{f : α → M}
(h1 : Set.mulIndicator s f = f)
(h2 : s ⊆ t)
:
Set.mulIndicator t f = f
@[simp]
theorem
Set.indicator_eq_zero
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{s : Set α}
{f : α → M}
:
(Set.indicator s f = fun x => 0) ↔ Disjoint (Function.support f) s
@[simp]
theorem
Set.mulIndicator_eq_one
{α : Type u_1}
{M : Type u_2}
[inst : One M]
{s : Set α}
{f : α → M}
:
(Set.mulIndicator s f = fun x => 1) ↔ Disjoint (Function.mulSupport f) s
@[simp]
theorem
Set.indicator_eq_zero'
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{s : Set α}
{f : α → M}
:
Set.indicator s f = 0 ↔ Disjoint (Function.support f) s
@[simp]
theorem
Set.mulIndicator_eq_one'
{α : Type u_1}
{M : Type u_2}
[inst : One M]
{s : Set α}
{f : α → M}
:
Set.mulIndicator s f = 1 ↔ Disjoint (Function.mulSupport f) s
theorem
Set.indicator_apply_ne_zero
{α : Type u_2}
{M : Type u_1}
[inst : Zero M]
{s : Set α}
{f : α → M}
{a : α}
:
Set.indicator s f a ≠ 0 ↔ a ∈ s ∩ Function.support f
theorem
Set.mulIndicator_apply_ne_one
{α : Type u_2}
{M : Type u_1}
[inst : One M]
{s : Set α}
{f : α → M}
{a : α}
:
Set.mulIndicator s f a ≠ 1 ↔ a ∈ s ∩ Function.mulSupport f
@[simp]
theorem
Set.support_indicator
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{s : Set α}
{f : α → M}
:
Function.support (Set.indicator s f) = s ∩ Function.support f
@[simp]
theorem
Set.mulSupport_mulIndicator
{α : Type u_1}
{M : Type u_2}
[inst : One M]
{s : Set α}
{f : α → M}
:
Function.mulSupport (Set.mulIndicator s f) = s ∩ Function.mulSupport f
theorem
Set.mem_of_indicator_ne_zero
{α : Type u_2}
{M : Type u_1}
[inst : Zero M]
{s : Set α}
{f : α → M}
{a : α}
(h : Set.indicator s f a ≠ 0)
:
a ∈ s
If an additive indicator function is not equal to 0 at a point, then that point is
in the set.
theorem
Set.mem_of_mulIndicator_ne_one
{α : Type u_2}
{M : Type u_1}
[inst : One M]
{s : Set α}
{f : α → M}
{a : α}
(h : Set.mulIndicator s f a ≠ 1)
:
a ∈ s
If a multiplicative indicator function is not equal to 1 at a point, then that point is in the
set.
theorem
Set.eqOn_indicator
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{s : Set α}
{f : α → M}
:
Set.EqOn (Set.indicator s f) f s
theorem
Set.eqOn_mulIndicator
{α : Type u_1}
{M : Type u_2}
[inst : One M]
{s : Set α}
{f : α → M}
:
Set.EqOn (Set.mulIndicator s f) f s
theorem
Set.support_indicator_subset
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{s : Set α}
{f : α → M}
:
Function.support (Set.indicator s f) ⊆ s
theorem
Set.mulSupport_mulIndicator_subset
{α : Type u_1}
{M : Type u_2}
[inst : One M]
{s : Set α}
{f : α → M}
:
Function.mulSupport (Set.mulIndicator s f) ⊆ s
@[simp]
theorem
Set.indicator_support
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{f : α → M}
:
Set.indicator (Function.support f) f = f
@[simp]
theorem
Set.mulIndicator_mulSupport
{α : Type u_1}
{M : Type u_2}
[inst : One M]
{f : α → M}
:
Set.mulIndicator (Function.mulSupport f) f = f
theorem
Set.indicator_congr
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{s : Set α}
{f : α → M}
{g : α → M}
(h : Set.EqOn f g s)
:
Set.indicator s f = Set.indicator s g
theorem
Set.mulIndicator_congr
{α : Type u_1}
{M : Type u_2}
[inst : One M]
{s : Set α}
{f : α → M}
{g : α → M}
(h : Set.EqOn f g s)
:
Set.mulIndicator s f = Set.mulIndicator s g
@[simp]
theorem
Set.indicator_univ
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
(f : α → M)
:
Set.indicator Set.univ f = f
@[simp]
theorem
Set.mulIndicator_univ
{α : Type u_1}
{M : Type u_2}
[inst : One M]
(f : α → M)
:
Set.mulIndicator Set.univ f = f
@[simp]
theorem
Set.indicator_empty
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
(f : α → M)
:
Set.indicator ∅ f = fun x => 0
@[simp]
theorem
Set.mulIndicator_empty
{α : Type u_1}
{M : Type u_2}
[inst : One M]
(f : α → M)
:
Set.mulIndicator ∅ f = fun x => 1
theorem
Set.indicator_empty'
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
(f : α → M)
:
Set.indicator ∅ f = 0
theorem
Set.mulIndicator_empty'
{α : Type u_1}
{M : Type u_2}
[inst : One M]
(f : α → M)
:
Set.mulIndicator ∅ f = 1
@[simp]
theorem
Set.indicator_zero
{α : Type u_1}
(M : Type u_2)
[inst : Zero M]
(s : Set α)
:
(Set.indicator s fun x => 0) = fun x => 0
@[simp]
theorem
Set.mulIndicator_one
{α : Type u_1}
(M : Type u_2)
[inst : One M]
(s : Set α)
:
(Set.mulIndicator s fun x => 1) = fun x => 1
@[simp]
theorem
Set.indicator_zero'
{α : Type u_1}
(M : Type u_2)
[inst : Zero M]
{s : Set α}
:
Set.indicator s 0 = 0
@[simp]
theorem
Set.mulIndicator_one'
{α : Type u_1}
(M : Type u_2)
[inst : One M]
{s : Set α}
:
Set.mulIndicator s 1 = 1
theorem
Set.indicator_indicator
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
(s : Set α)
(t : Set α)
(f : α → M)
:
Set.indicator s (Set.indicator t f) = Set.indicator (s ∩ t) f
theorem
Set.mulIndicator_mulIndicator
{α : Type u_1}
{M : Type u_2}
[inst : One M]
(s : Set α)
(t : Set α)
(f : α → M)
:
Set.mulIndicator s (Set.mulIndicator t f) = Set.mulIndicator (s ∩ t) f
@[simp]
theorem
Set.indicator_inter_support
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
(s : Set α)
(f : α → M)
:
Set.indicator (s ∩ Function.support f) f = Set.indicator s f
@[simp]
theorem
Set.mulIndicator_inter_mulSupport
{α : Type u_1}
{M : Type u_2}
[inst : One M]
(s : Set α)
(f : α → M)
:
Set.mulIndicator (s ∩ Function.mulSupport f) f = Set.mulIndicator s f
theorem
Set.comp_indicator
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[inst : Zero M]
(h : M → β)
(f : α → M)
{s : Set α}
{x : α}
[inst : DecidablePred fun x => x ∈ s]
:
h (Set.indicator s f x) = Set.piecewise s (h ∘ f) (Function.const α (h 0)) x
theorem
Set.comp_mulIndicator
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[inst : One M]
(h : M → β)
(f : α → M)
{s : Set α}
{x : α}
[inst : DecidablePred fun x => x ∈ s]
:
h (Set.mulIndicator s f x) = Set.piecewise s (h ∘ f) (Function.const α (h 1)) x
theorem
Set.indicator_comp_right
{α : Type u_1}
{β : Type u_3}
{M : Type u_2}
[inst : Zero M]
{s : Set α}
(f : β → α)
{g : α → M}
{x : β}
:
Set.indicator (f ⁻¹' s) (g ∘ f) x = Set.indicator s g (f x)
theorem
Set.mulIndicator_comp_right
{α : Type u_1}
{β : Type u_3}
{M : Type u_2}
[inst : One M]
{s : Set α}
(f : β → α)
{g : α → M}
{x : β}
:
Set.mulIndicator (f ⁻¹' s) (g ∘ f) x = Set.mulIndicator s g (f x)
theorem
Set.indicator_image
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[inst : Zero M]
{s : Set α}
{f : β → M}
{g : α → β}
(hg : Function.Injective g)
{x : α}
:
Set.indicator (g '' s) f (g x) = Set.indicator s (f ∘ g) x
theorem
Set.mulIndicator_image
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[inst : One M]
{s : Set α}
{f : β → M}
{g : α → β}
(hg : Function.Injective g)
{x : α}
:
Set.mulIndicator (g '' s) f (g x) = Set.mulIndicator s (f ∘ g) x
theorem
Set.indicator_comp_of_zero
{α : Type u_3}
{M : Type u_2}
{N : Type u_1}
[inst : Zero M]
[inst : Zero N]
{s : Set α}
{f : α → M}
{g : M → N}
(hg : g 0 = 0)
:
Set.indicator s (g ∘ f) = g ∘ Set.indicator s f
theorem
Set.mulIndicator_comp_of_one
{α : Type u_3}
{M : Type u_2}
{N : Type u_1}
[inst : One M]
[inst : One N]
{s : Set α}
{f : α → M}
{g : M → N}
(hg : g 1 = 1)
:
Set.mulIndicator s (g ∘ f) = g ∘ Set.mulIndicator s f
theorem
Set.comp_indicator_const
{α : Type u_3}
{M : Type u_2}
{N : Type u_1}
[inst : Zero M]
[inst : Zero N]
{s : Set α}
(c : M)
(f : M → N)
(hf : f 0 = 0)
:
(fun x => f (Set.indicator s (fun x => c) x)) = Set.indicator s fun x => f c
theorem
Set.comp_mulIndicator_const
{α : Type u_3}
{M : Type u_2}
{N : Type u_1}
[inst : One M]
[inst : One N]
{s : Set α}
(c : M)
(f : M → N)
(hf : f 1 = 1)
:
(fun x => f (Set.mulIndicator s (fun x => c) x)) = Set.mulIndicator s fun x => f c
theorem
Set.indicator_rel_indicator
{α : Type u_2}
{M : Type u_1}
[inst : Zero M]
{s : Set α}
{f : α → M}
{g : α → M}
{a : α}
{r : M → M → Prop}
(h1 : r 0 0)
(ha : a ∈ s → r (f a) (g a))
:
r (Set.indicator s f a) (Set.indicator s g a)
theorem
Set.mulIndicator_rel_mulIndicator
{α : Type u_2}
{M : Type u_1}
[inst : One M]
{s : Set α}
{f : α → M}
{g : α → M}
{a : α}
{r : M → M → Prop}
(h1 : r 1 1)
(ha : a ∈ s → r (f a) (g a))
:
r (Set.mulIndicator s f a) (Set.mulIndicator s g a)
theorem
Set.indicator_union_add_inter_apply
{α : Type u_1}
{M : Type u_2}
[inst : AddZeroClass M]
(f : α → M)
(s : Set α)
(t : Set α)
(a : α)
:
Set.indicator (s ∪ t) f a + Set.indicator (s ∩ t) f a = Set.indicator s f a + Set.indicator t f a
theorem
Set.mulIndicator_union_mul_inter_apply
{α : Type u_1}
{M : Type u_2}
[inst : MulOneClass M]
(f : α → M)
(s : Set α)
(t : Set α)
(a : α)
:
Set.mulIndicator (s ∪ t) f a * Set.mulIndicator (s ∩ t) f a = Set.mulIndicator s f a * Set.mulIndicator t f a
theorem
Set.indicator_union_add_inter
{α : Type u_1}
{M : Type u_2}
[inst : AddZeroClass M]
(f : α → M)
(s : Set α)
(t : Set α)
:
Set.indicator (s ∪ t) f + Set.indicator (s ∩ t) f = Set.indicator s f + Set.indicator t f
theorem
Set.mulIndicator_union_mul_inter
{α : Type u_1}
{M : Type u_2}
[inst : MulOneClass M]
(f : α → M)
(s : Set α)
(t : Set α)
:
Set.mulIndicator (s ∪ t) f * Set.mulIndicator (s ∩ t) f = Set.mulIndicator s f * Set.mulIndicator t f
theorem
Set.indicator_union_of_not_mem_inter
{α : Type u_1}
{M : Type u_2}
[inst : AddZeroClass M]
{s : Set α}
{t : Set α}
{a : α}
(h : ¬a ∈ s ∩ t)
(f : α → M)
:
Set.indicator (s ∪ t) f a = Set.indicator s f a + Set.indicator t f a
theorem
Set.mulIndicator_union_of_not_mem_inter
{α : Type u_1}
{M : Type u_2}
[inst : MulOneClass M]
{s : Set α}
{t : Set α}
{a : α}
(h : ¬a ∈ s ∩ t)
(f : α → M)
:
Set.mulIndicator (s ∪ t) f a = Set.mulIndicator s f a * Set.mulIndicator t f a
theorem
Set.indicator_union_of_disjoint
{α : Type u_1}
{M : Type u_2}
[inst : AddZeroClass M]
{s : Set α}
{t : Set α}
(h : Disjoint s t)
(f : α → M)
:
Set.indicator (s ∪ t) f = fun a => Set.indicator s f a + Set.indicator t f a
theorem
Set.mulIndicator_union_of_disjoint
{α : Type u_1}
{M : Type u_2}
[inst : MulOneClass M]
{s : Set α}
{t : Set α}
(h : Disjoint s t)
(f : α → M)
:
Set.mulIndicator (s ∪ t) f = fun a => Set.mulIndicator s f a * Set.mulIndicator t f a
theorem
Set.indicator_add
{α : Type u_1}
{M : Type u_2}
[inst : AddZeroClass M]
(s : Set α)
(f : α → M)
(g : α → M)
:
(Set.indicator s fun a => f a + g a) = fun a => Set.indicator s f a + Set.indicator s g a
theorem
Set.mulIndicator_mul
{α : Type u_1}
{M : Type u_2}
[inst : MulOneClass M]
(s : Set α)
(f : α → M)
(g : α → M)
:
(Set.mulIndicator s fun a => f a * g a) = fun a => Set.mulIndicator s f a * Set.mulIndicator s g a
theorem
Set.indicator_add'
{α : Type u_1}
{M : Type u_2}
[inst : AddZeroClass M]
(s : Set α)
(f : α → M)
(g : α → M)
:
Set.indicator s (f + g) = Set.indicator s f + Set.indicator s g
theorem
Set.mulIndicator_mul'
{α : Type u_1}
{M : Type u_2}
[inst : MulOneClass M]
(s : Set α)
(f : α → M)
(g : α → M)
:
Set.mulIndicator s (f * g) = Set.mulIndicator s f * Set.mulIndicator s g
@[simp]
theorem
Set.indicator_compl_add_self_apply
{α : Type u_1}
{M : Type u_2}
[inst : AddZeroClass M]
(s : Set α)
(f : α → M)
(a : α)
:
Set.indicator (sᶜ) f a + Set.indicator s f a = f a
@[simp]
theorem
Set.mulIndicator_compl_mul_self_apply
{α : Type u_1}
{M : Type u_2}
[inst : MulOneClass M]
(s : Set α)
(f : α → M)
(a : α)
:
Set.mulIndicator (sᶜ) f a * Set.mulIndicator s f a = f a
@[simp]
theorem
Set.indicator_compl_add_self
{α : Type u_1}
{M : Type u_2}
[inst : AddZeroClass M]
(s : Set α)
(f : α → M)
:
Set.indicator (sᶜ) f + Set.indicator s f = f
@[simp]
theorem
Set.mulIndicator_compl_mul_self
{α : Type u_1}
{M : Type u_2}
[inst : MulOneClass M]
(s : Set α)
(f : α → M)
:
Set.mulIndicator (sᶜ) f * Set.mulIndicator s f = f
@[simp]
theorem
Set.indicator_self_add_compl_apply
{α : Type u_1}
{M : Type u_2}
[inst : AddZeroClass M]
(s : Set α)
(f : α → M)
(a : α)
:
Set.indicator s f a + Set.indicator (sᶜ) f a = f a
@[simp]
theorem
Set.mulIndicator_self_mul_compl_apply
{α : Type u_1}
{M : Type u_2}
[inst : MulOneClass M]
(s : Set α)
(f : α → M)
(a : α)
:
Set.mulIndicator s f a * Set.mulIndicator (sᶜ) f a = f a
@[simp]
theorem
Set.indicator_self_add_compl
{α : Type u_1}
{M : Type u_2}
[inst : AddZeroClass M]
(s : Set α)
(f : α → M)
:
Set.indicator s f + Set.indicator (sᶜ) f = f
@[simp]
theorem
Set.mulIndicator_self_mul_compl
{α : Type u_1}
{M : Type u_2}
[inst : MulOneClass M]
(s : Set α)
(f : α → M)
:
Set.mulIndicator s f * Set.mulIndicator (sᶜ) f = f
theorem
Set.indicator_add_eq_left
{α : Type u_1}
{M : Type u_2}
[inst : AddZeroClass M]
{f : α → M}
{g : α → M}
(h : Disjoint (Function.support f) (Function.support g))
:
Set.indicator (Function.support f) (f + g) = f
theorem
Set.mulIndicator_mul_eq_left
{α : Type u_1}
{M : Type u_2}
[inst : MulOneClass M]
{f : α → M}
{g : α → M}
(h : Disjoint (Function.mulSupport f) (Function.mulSupport g))
:
Set.mulIndicator (Function.mulSupport f) (f * g) = f
theorem
Set.indicator_add_eq_right
{α : Type u_1}
{M : Type u_2}
[inst : AddZeroClass M]
{f : α → M}
{g : α → M}
(h : Disjoint (Function.support f) (Function.support g))
:
Set.indicator (Function.support g) (f + g) = g
theorem
Set.mulIndicator_mul_eq_right
{α : Type u_1}
{M : Type u_2}
[inst : MulOneClass M]
{f : α → M}
{g : α → M}
(h : Disjoint (Function.mulSupport f) (Function.mulSupport g))
:
Set.mulIndicator (Function.mulSupport g) (f * g) = g
theorem
Set.indicator_add_compl_eq_piecewise
{α : Type u_1}
{M : Type u_2}
[inst : AddZeroClass M]
{s : Set α}
[inst : DecidablePred fun x => x ∈ s]
(f : α → M)
(g : α → M)
:
Set.indicator s f + Set.indicator (sᶜ) g = Set.piecewise s f g
theorem
Set.mulIndicator_mul_compl_eq_piecewise
{α : Type u_1}
{M : Type u_2}
[inst : MulOneClass M]
{s : Set α}
[inst : DecidablePred fun x => x ∈ s]
(f : α → M)
(g : α → M)
:
Set.mulIndicator s f * Set.mulIndicator (sᶜ) g = Set.piecewise s f g
def
Set.indicatorHom.proof_1
{α : Type u_1}
(M : Type u_2)
[inst : AddZeroClass M]
(s : Set α)
:
(Set.indicator s fun x => 0) = fun x => 0
Equations
- (_ : (Set.indicator s fun x => 0) = fun x => 0) = (_ : (Set.indicator s fun x => 0) = fun x => 0)
noncomputable def
Set.indicatorHom
{α : Type u_1}
(M : Type u_2)
[inst : AddZeroClass M]
(s : Set α)
:
(α → M) →+ α → M
Set.indicator as an addMonoidHom.
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
Set.mulIndicatorHom
{α : Type u_1}
(M : Type u_2)
[inst : MulOneClass M]
(s : Set α)
:
(α → M) →* α → M
Set.mulIndicator as a monoidHom.
Equations
- One or more equations did not get rendered due to their size.
theorem
Set.indicator_smul_apply
{α : Type u_1}
{M : Type u_3}
{A : Type u_2}
[inst : AddMonoid A]
[inst : Monoid M]
[inst : DistribMulAction M A]
(s : Set α)
(r : α → M)
(f : α → A)
(x : α)
:
Set.indicator s (fun x => r x • f x) x = r x • Set.indicator s f x
theorem
Set.indicator_smul
{α : Type u_1}
{M : Type u_3}
{A : Type u_2}
[inst : AddMonoid A]
[inst : Monoid M]
[inst : DistribMulAction M A]
(s : Set α)
(r : α → M)
(f : α → A)
:
(Set.indicator s fun x => r x • f x) = fun x => r x • Set.indicator s f x
theorem
Set.indicator_const_smul_apply
{α : Type u_1}
{M : Type u_3}
{A : Type u_2}
[inst : AddMonoid A]
[inst : Monoid M]
[inst : DistribMulAction M A]
(s : Set α)
(r : M)
(f : α → A)
(x : α)
:
Set.indicator s (fun x => r • f x) x = r • Set.indicator s f x
theorem
Set.indicator_const_smul
{α : Type u_1}
{M : Type u_3}
{A : Type u_2}
[inst : AddMonoid A]
[inst : Monoid M]
[inst : DistribMulAction M A]
(s : Set α)
(r : M)
(f : α → A)
:
(Set.indicator s fun x => r • f x) = fun x => r • Set.indicator s f x
theorem
Set.indicator_neg'
{α : Type u_1}
{G : Type u_2}
[inst : AddGroup G]
(s : Set α)
(f : α → G)
:
Set.indicator s (-f) = -Set.indicator s f
theorem
Set.mulIndicator_inv'
{α : Type u_1}
{G : Type u_2}
[inst : Group G]
(s : Set α)
(f : α → G)
:
Set.mulIndicator s f⁻¹ = (Set.mulIndicator s f)⁻¹
theorem
Set.indicator_neg
{α : Type u_1}
{G : Type u_2}
[inst : AddGroup G]
(s : Set α)
(f : α → G)
:
(Set.indicator s fun a => -f a) = fun a => -Set.indicator s f a
theorem
Set.mulIndicator_inv
{α : Type u_1}
{G : Type u_2}
[inst : Group G]
(s : Set α)
(f : α → G)
:
(Set.mulIndicator s fun a => (f a)⁻¹) = fun a => (Set.mulIndicator s f a)⁻¹
theorem
Set.indicator_sub
{α : Type u_1}
{G : Type u_2}
[inst : AddGroup G]
(s : Set α)
(f : α → G)
(g : α → G)
:
(Set.indicator s fun a => f a - g a) = fun a => Set.indicator s f a - Set.indicator s g a
theorem
Set.mulIndicator_div
{α : Type u_1}
{G : Type u_2}
[inst : Group G]
(s : Set α)
(f : α → G)
(g : α → G)
:
(Set.mulIndicator s fun a => f a / g a) = fun a => Set.mulIndicator s f a / Set.mulIndicator s g a
theorem
Set.indicator_sub'
{α : Type u_1}
{G : Type u_2}
[inst : AddGroup G]
(s : Set α)
(f : α → G)
(g : α → G)
:
Set.indicator s (f - g) = Set.indicator s f - Set.indicator s g
theorem
Set.mulIndicator_div'
{α : Type u_1}
{G : Type u_2}
[inst : Group G]
(s : Set α)
(f : α → G)
(g : α → G)
:
Set.mulIndicator s (f / g) = Set.mulIndicator s f / Set.mulIndicator s g
theorem
Set.indicator_compl'
{α : Type u_1}
{G : Type u_2}
[inst : AddGroup G]
(s : Set α)
(f : α → G)
:
Set.indicator (sᶜ) f = f + -Set.indicator s f
theorem
Set.mulIndicator_compl
{α : Type u_1}
{G : Type u_2}
[inst : Group G]
(s : Set α)
(f : α → G)
:
Set.mulIndicator (sᶜ) f = f * (Set.mulIndicator s f)⁻¹
theorem
Set.indicator_compl
{α : Type u_2}
{G : Type u_1}
[inst : AddGroup G]
(s : Set α)
(f : α → G)
:
Set.indicator (sᶜ) f = f - Set.indicator s f
theorem
Set.indicator_diff'
{α : Type u_1}
{G : Type u_2}
[inst : AddGroup G]
{s : Set α}
{t : Set α}
(h : s ⊆ t)
(f : α → G)
:
Set.indicator (t \ s) f = Set.indicator t f + -Set.indicator s f
theorem
Set.mulIndicator_diff
{α : Type u_1}
{G : Type u_2}
[inst : Group G]
{s : Set α}
{t : Set α}
(h : s ⊆ t)
(f : α → G)
:
Set.mulIndicator (t \ s) f = Set.mulIndicator t f * (Set.mulIndicator s f)⁻¹
theorem
Set.indicator_diff
{α : Type u_2}
{G : Type u_1}
[inst : AddGroup G]
{s : Set α}
{t : Set α}
(h : s ⊆ t)
(f : α → G)
:
Set.indicator (t \ s) f = Set.indicator t f - Set.indicator s f
theorem
Set.sum_indicator_subset_of_eq_zero
{α : Type u_2}
{M : Type u_3}
{N : Type u_1}
[inst : AddCommMonoid M]
[inst : Zero N]
(f : α → N)
(g : α → N → M)
{s : Finset α}
{t : Finset α}
(h : s ⊆ t)
(hg : ∀ (a : α), g a 0 = 0)
:
(Finset.sum s fun i => g i (f i)) = Finset.sum t fun i => g i (Set.indicator (↑s) f i)
Consider a sum of g i (f i) over a Finset. Suppose g is a
function such as multiplication, which maps a second argument of 0 to
0. (A typical use case would be a weighted sum of f i * h i or f i • h i,
where f gives the weights that are multiplied by some other
function h.) Then if f is replaced by the corresponding indicator
function, the Finset may be replaced by a possibly larger Finset
without changing the value of the sum.
theorem
Set.prod_mulIndicator_subset_of_eq_one
{α : Type u_2}
{M : Type u_3}
{N : Type u_1}
[inst : CommMonoid M]
[inst : One N]
(f : α → N)
(g : α → N → M)
{s : Finset α}
{t : Finset α}
(h : s ⊆ t)
(hg : ∀ (a : α), g a 1 = 1)
:
(Finset.prod s fun i => g i (f i)) = Finset.prod t fun i => g i (Set.mulIndicator (↑s) f i)
Consider a product of g i (f i) over a Finset. Suppose g is a
function such as Pow, which maps a second argument of 1 to
1. Then if f is replaced by the corresponding multiplicative indicator
function, the Finset may be replaced by a possibly larger Finset
without changing the value of the sum.
theorem
Set.sum_indicator_subset
{α : Type u_1}
{M : Type u_2}
[inst : AddCommMonoid M]
(f : α → M)
{s : Finset α}
{t : Finset α}
(h : s ⊆ t)
:
(Finset.sum s fun i => f i) = Finset.sum t fun i => Set.indicator (↑s) f i
Summing an indicator function over a possibly larger Finset is the same as summing
the original function over the original finset.
theorem
Set.prod_mulIndicator_subset
{α : Type u_1}
{M : Type u_2}
[inst : CommMonoid M]
(f : α → M)
{s : Finset α}
{t : Finset α}
(h : s ⊆ t)
:
(Finset.prod s fun i => f i) = Finset.prod t fun i => Set.mulIndicator (↑s) f i
Taking the product of an indicator function over a possibly larger Finset is the same as
taking the original function over the original Finset.
theorem
Finset.sum_indicator_eq_sum_filter
{α : Type u_2}
{ι : Type u_1}
{M : Type u_3}
[inst : AddCommMonoid M]
(s : Finset ι)
(f : ι → α → M)
(t : ι → Set α)
(g : ι → α)
[inst : DecidablePred fun i => g i ∈ t i]
:
(Finset.sum s fun i => Set.indicator (t i) (f i) (g i)) = Finset.sum (Finset.filter (fun i => g i ∈ t i) s) fun i => f i (g i)
theorem
Finset.prod_mulIndicator_eq_prod_filter
{α : Type u_2}
{ι : Type u_1}
{M : Type u_3}
[inst : CommMonoid M]
(s : Finset ι)
(f : ι → α → M)
(t : ι → Set α)
(g : ι → α)
[inst : DecidablePred fun i => g i ∈ t i]
:
(Finset.prod s fun i => Set.mulIndicator (t i) (f i) (g i)) = Finset.prod (Finset.filter (fun i => g i ∈ t i) s) fun i => f i (g i)
theorem
Set.indicator_finset_sum
{α : Type u_2}
{ι : Type u_1}
{M : Type u_3}
[inst : AddCommMonoid M]
(I : Finset ι)
(s : Set α)
(f : ι → α → M)
:
Set.indicator s (Finset.sum I fun i => f i) = Finset.sum I fun i => Set.indicator s (f i)
theorem
Set.mulIndicator_finset_prod
{α : Type u_2}
{ι : Type u_1}
{M : Type u_3}
[inst : CommMonoid M]
(I : Finset ι)
(s : Set α)
(f : ι → α → M)
:
Set.mulIndicator s (Finset.prod I fun i => f i) = Finset.prod I fun i => Set.mulIndicator s (f i)
theorem
Set.indicator_finset_bunionᵢ
{α : Type u_2}
{M : Type u_3}
[inst : AddCommMonoid M]
{ι : Type u_1}
(I : Finset ι)
(s : ι → Set α)
{f : α → M}
:
(∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
Set.indicator (Set.unionᵢ fun i => Set.unionᵢ fun h => s i) f = fun a => Finset.sum I fun i => Set.indicator (s i) f a
theorem
Set.mulIndicator_finset_bunionᵢ
{α : Type u_2}
{M : Type u_3}
[inst : CommMonoid M]
{ι : Type u_1}
(I : Finset ι)
(s : ι → Set α)
{f : α → M}
:
(∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
Set.mulIndicator (Set.unionᵢ fun i => Set.unionᵢ fun h => s i) f = fun a =>
Finset.prod I fun i => Set.mulIndicator (s i) f a
theorem
Set.indicator_finset_bunionᵢ_apply
{α : Type u_2}
{M : Type u_3}
[inst : AddCommMonoid M]
{ι : Type u_1}
(I : Finset ι)
(s : ι → Set α)
{f : α → M}
(h : ∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j))
(x : α)
:
Set.indicator (Set.unionᵢ fun i => Set.unionᵢ fun h => s i) f x = Finset.sum I fun i => Set.indicator (s i) f x
theorem
Set.mulIndicator_finset_bunionᵢ_apply
{α : Type u_2}
{M : Type u_3}
[inst : CommMonoid M]
{ι : Type u_1}
(I : Finset ι)
(s : ι → Set α)
{f : α → M}
(h : ∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j))
(x : α)
:
Set.mulIndicator (Set.unionᵢ fun i => Set.unionᵢ fun h => s i) f x = Finset.prod I fun i => Set.mulIndicator (s i) f x
theorem
Set.indicator_mul
{α : Type u_1}
{M : Type u_2}
[inst : MulZeroClass M]
(s : Set α)
(f : α → M)
(g : α → M)
:
(Set.indicator s fun a => f a * g a) = fun a => Set.indicator s f a * Set.indicator s g a
theorem
Set.indicator_mul_left
{α : Type u_1}
{M : Type u_2}
[inst : MulZeroClass M]
{a : α}
(s : Set α)
(f : α → M)
(g : α → M)
:
Set.indicator s (fun a => f a * g a) a = Set.indicator s f a * g a
theorem
Set.indicator_mul_right
{α : Type u_1}
{M : Type u_2}
[inst : MulZeroClass M]
{a : α}
(s : Set α)
(f : α → M)
(g : α → M)
:
Set.indicator s (fun a => f a * g a) a = f a * Set.indicator s g a
theorem
Set.inter_indicator_mul
{α : Type u_1}
{M : Type u_2}
[inst : MulZeroClass M]
{t1 : Set α}
{t2 : Set α}
(f : α → M)
(g : α → M)
(x : α)
:
Set.indicator (t1 ∩ t2) (fun x => f x * g x) x = Set.indicator t1 f x * Set.indicator t2 g x
theorem
Set.inter_indicator_one
{α : Type u_1}
{M : Type u_2}
[inst : MulZeroOneClass M]
{s : Set α}
{t : Set α}
:
Set.indicator (s ∩ t) 1 = Set.indicator s 1 * Set.indicator t 1
theorem
Set.indicator_prod_one
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[inst : MulZeroOneClass M]
{s : Set α}
{t : Set β}
{x : α}
{y : β}
:
Set.indicator (s ×ˢ t) 1 (x, y) = Set.indicator s 1 x * Set.indicator t 1 y
theorem
Set.indicator_eq_zero_iff_not_mem
{α : Type u_1}
(M : Type u_2)
[inst : MulZeroOneClass M]
[inst : Nontrivial M]
{U : Set α}
{x : α}
:
Set.indicator U 1 x = 0 ↔ ¬x ∈ U
theorem
Set.indicator_eq_one_iff_mem
{α : Type u_1}
(M : Type u_2)
[inst : MulZeroOneClass M]
[inst : Nontrivial M]
{U : Set α}
{x : α}
:
Set.indicator U 1 x = 1 ↔ x ∈ U
theorem
Set.indicator_one_inj
{α : Type u_1}
(M : Type u_2)
[inst : MulZeroOneClass M]
[inst : Nontrivial M]
{U : Set α}
{V : Set α}
(h : Set.indicator U 1 = Set.indicator V 1)
:
U = V
theorem
Set.indicator_le_indicator
{α : Type u_2}
{M : Type u_1}
[inst : Zero M]
{s : Set α}
{f : α → M}
{g : α → M}
{a : α}
[inst : Preorder M]
(h : f a ≤ g a)
:
Set.indicator s f a ≤ Set.indicator s g a
theorem
Set.mulIndicator_le_mulIndicator
{α : Type u_2}
{M : Type u_1}
[inst : One M]
{s : Set α}
{f : α → M}
{g : α → M}
{a : α}
[inst : Preorder M]
(h : f a ≤ g a)
:
Set.mulIndicator s f a ≤ Set.mulIndicator s g a
theorem
Set.indicator_le_indicator_of_subset
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{s : Set α}
{t : Set α}
{f : α → M}
[inst : Preorder M]
(h : s ⊆ t)
(hf : ∀ (a : α), 0 ≤ f a)
(a : α)
:
Set.indicator s f a ≤ Set.indicator t f a
theorem
Set.mulIndicator_le_mulIndicator_of_subset
{α : Type u_1}
{M : Type u_2}
[inst : One M]
{s : Set α}
{t : Set α}
{f : α → M}
[inst : Preorder M]
(h : s ⊆ t)
(hf : ∀ (a : α), 1 ≤ f a)
(a : α)
:
Set.mulIndicator s f a ≤ Set.mulIndicator t f a
theorem
Set.indicator_unionᵢ_apply
{α : Type u_3}
{ι : Sort u_1}
{M : Type u_2}
[inst : CompleteLattice M]
[inst : Zero M]
(h1 : ⊥ = 0)
(s : ι → Set α)
(f : α → M)
(x : α)
:
Set.indicator (Set.unionᵢ fun i => s i) f x = ⨆ i, Set.indicator (s i) f x
theorem
Set.mulIndicator_unionᵢ_apply
{α : Type u_3}
{ι : Sort u_1}
{M : Type u_2}
[inst : CompleteLattice M]
[inst : One M]
(h1 : ⊥ = 1)
(s : ι → Set α)
(f : α → M)
(x : α)
:
Set.mulIndicator (Set.unionᵢ fun i => s i) f x = ⨆ i, Set.mulIndicator (s i) f x
theorem
Set.indicator_le_self
{α : Type u_1}
{M : Type u_2}
[inst : CanonicallyOrderedAddMonoid M]
(s : Set α)
(f : α → M)
:
Set.indicator s f ≤ f
theorem
Set.mulIndicator_le_self
{α : Type u_1}
{M : Type u_2}
[inst : CanonicallyOrderedMonoid M]
(s : Set α)
(f : α → M)
:
Set.mulIndicator s f ≤ f
theorem
Set.indicator_apply_le
{α : Type u_1}
{M : Type u_2}
[inst : CanonicallyOrderedAddMonoid M]
{a : α}
{s : Set α}
{f : α → M}
{g : α → M}
(hfg : a ∈ s → f a ≤ g a)
:
Set.indicator s f a ≤ g a
theorem
Set.mulIndicator_apply_le
{α : Type u_1}
{M : Type u_2}
[inst : CanonicallyOrderedMonoid M]
{a : α}
{s : Set α}
{f : α → M}
{g : α → M}
(hfg : a ∈ s → f a ≤ g a)
:
Set.mulIndicator s f a ≤ g a
theorem
Set.indicator_le
{α : Type u_1}
{M : Type u_2}
[inst : CanonicallyOrderedAddMonoid M]
{s : Set α}
{f : α → M}
{g : α → M}
(hfg : ∀ (a : α), a ∈ s → f a ≤ g a)
:
Set.indicator s f ≤ g
theorem
Set.mulIndicator_le
{α : Type u_1}
{M : Type u_2}
[inst : CanonicallyOrderedMonoid M]
{s : Set α}
{f : α → M}
{g : α → M}
(hfg : ∀ (a : α), a ∈ s → f a ≤ g a)
:
Set.mulIndicator s f ≤ g
theorem
Set.indicator_le_indicator_nonneg
{α : Type u_2}
{β : Type u_1}
[inst : LinearOrder β]
[inst : Zero β]
(s : Set α)
(f : α → β)
:
Set.indicator s f ≤ Set.indicator { x | 0 ≤ f x } f
theorem
Set.indicator_nonpos_le_indicator
{α : Type u_2}
{β : Type u_1}
[inst : LinearOrder β]
[inst : Zero β]
(s : Set α)
(f : α → β)
:
Set.indicator { x | f x ≤ 0 } f ≤ Set.indicator s f
theorem
AddMonoidHom.map_indicator
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : AddZeroClass M]
[inst : AddZeroClass N]
(f : M →+ N)
(s : Set α)
(g : α → M)
(x : α)
:
↑f (Set.indicator s g x) = Set.indicator s (↑f ∘ g) x
theorem
MonoidHom.map_mulIndicator
{α : Type u_3}
{M : Type u_1}
{N : Type u_2}
[inst : MulOneClass M]
[inst : MulOneClass N]
(f : M →* N)
(s : Set α)
(g : α → M)
(x : α)
:
↑f (Set.mulIndicator s g x) = Set.mulIndicator s (↑f ∘ g) x