Indicator function #
indicator (s : set α) (f : α → β) (a : α)isf aifa ∈ sand is0otherwise.mul_indicator (s : set α) (f : α → β) (a : α)isf aifa ∈ 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.
Tags #
indicator, characteristic
mul_indicator s f a is f a if a ∈ s, 1 otherwise.
Equations
- s.mul_indicator f = λ (x : α), ite (x ∈ s) (f x) 1
@[simp]
theorem
set.piecewise_eq_mul_indicator
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{f : α → M} :
s.piecewise f 1 = s.mul_indicator f
theorem
set.mul_indicator_apply
{α : Type u_1}
{M : Type u_4}
[has_one M]
(s : set α)
(f : α → M)
(a : α) :
s.mul_indicator f a = ite (a ∈ s) (f a) 1
@[simp]
theorem
set.mul_indicator_of_mem
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{a : α}
(h : a ∈ s)
(f : α → M) :
s.mul_indicator f a = f a
@[simp]
theorem
set.mul_indicator_of_not_mem
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{a : α}
(h : a ∉ s)
(f : α → M) :
s.mul_indicator f a = 1
theorem
set.mul_indicator_eq_one_or_self
{α : Type u_1}
{M : Type u_4}
[has_one M]
(s : set α)
(f : α → M)
(a : α) :
s.mul_indicator f a = 1 ∨ s.mul_indicator f a = f a
@[simp]
theorem
set.mul_indicator_apply_eq_self
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{f : α → M}
{a : α} :
s.mul_indicator f a = f a ↔ a ∉ s → f a = 1
@[simp]
theorem
set.mul_indicator_eq_self
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{f : α → M} :
s.mul_indicator f = f ↔ function.mul_support f ⊆ s
@[simp]
theorem
set.indicator_eq_self
{α : Type u_1}
{M : Type u_4}
[has_zero M]
{s : set α}
{f : α → M} :
s.indicator f = f ↔ function.support f ⊆ s
theorem
set.mul_indicator_eq_self_of_superset
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s t : set α}
{f : α → M}
(h1 : s.mul_indicator f = f)
(h2 : s ⊆ t) :
t.mul_indicator f = f
@[simp]
theorem
set.mul_indicator_apply_eq_one
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{f : α → M}
{a : α} :
s.mul_indicator f a = 1 ↔ a ∈ s → f a = 1
@[simp]
theorem
set.indicator_eq_zero
{α : Type u_1}
{M : Type u_4}
[has_zero M]
{s : set α}
{f : α → M} :
(s.indicator f = λ (x : α), 0) ↔ disjoint (function.support f) s
@[simp]
theorem
set.mul_indicator_eq_one
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{f : α → M} :
(s.mul_indicator f = λ (x : α), 1) ↔ disjoint (function.mul_support f) s
@[simp]
theorem
set.indicator_eq_zero'
{α : Type u_1}
{M : Type u_4}
[has_zero M]
{s : set α}
{f : α → M} :
s.indicator f = 0 ↔ disjoint (function.support f) s
@[simp]
theorem
set.mul_indicator_eq_one'
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{f : α → M} :
s.mul_indicator f = 1 ↔ disjoint (function.mul_support f) s
@[simp]
theorem
set.mul_support_mul_indicator
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{f : α → M} :
function.mul_support (s.mul_indicator f) = s ∩ function.mul_support f
@[simp]
theorem
set.support_indicator
{α : Type u_1}
{M : Type u_4}
[has_zero M]
{s : set α}
{f : α → M} :
function.support (s.indicator f) = s ∩ function.support f
theorem
set.mem_of_mul_indicator_ne_one
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{f : α → M}
{a : α}
(h : s.mul_indicator f a ≠ 1) :
a ∈ s
If a multiplicative indicator function is not equal to one at a point, then that point is in the set.
theorem
set.eq_on_mul_indicator
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{f : α → M} :
set.eq_on (s.mul_indicator f) f s
theorem
set.support_indicator_subset
{α : Type u_1}
{M : Type u_4}
[has_zero M]
{s : set α}
{f : α → M} :
function.support (s.indicator f) ⊆ s
theorem
set.mul_support_mul_indicator_subset
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{f : α → M} :
function.mul_support (s.mul_indicator f) ⊆ s
@[simp]
theorem
set.mul_indicator_mul_support
{α : Type u_1}
{M : Type u_4}
[has_one M]
{f : α → M} :
(function.mul_support f).mul_indicator f = f
@[simp]
theorem
set.indicator_support
{α : Type u_1}
{M : Type u_4}
[has_zero M]
{f : α → M} :
(function.support f).indicator f = f
@[simp]
theorem
set.mul_indicator_range_comp
{α : Type u_1}
{M : Type u_4}
[has_one M]
{ι : Sort u_2}
(f : ι → α)
(g : α → M) :
(set.range f).mul_indicator g ∘ f = g ∘ f
theorem
set.mul_indicator_congr
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{f g : α → M}
(h : set.eq_on f g s) :
s.mul_indicator f = s.mul_indicator g
@[simp]
theorem
set.mul_indicator_univ
{α : Type u_1}
{M : Type u_4}
[has_one M]
(f : α → M) :
set.univ.mul_indicator f = f
@[simp]
theorem
set.mul_indicator_empty
{α : Type u_1}
{M : Type u_4}
[has_one M]
(f : α → M) :
∅.mul_indicator f = λ (a : α), 1
@[simp]
theorem
set.mul_indicator_one
{α : Type u_1}
(M : Type u_4)
[has_one M]
(s : set α) :
s.mul_indicator (λ (x : α), 1) = λ (x : α), 1
@[simp]
theorem
set.mul_indicator_one'
{α : Type u_1}
(M : Type u_4)
[has_one M]
{s : set α} :
s.mul_indicator 1 = 1
theorem
set.mul_indicator_mul_indicator
{α : Type u_1}
{M : Type u_4}
[has_one M]
(s t : set α)
(f : α → M) :
s.mul_indicator (t.mul_indicator f) = (s ∩ t).mul_indicator f
@[simp]
theorem
set.mul_indicator_inter_mul_support
{α : Type u_1}
{M : Type u_4}
[has_one M]
(s : set α)
(f : α → M) :
(s ∩ function.mul_support f).mul_indicator f = s.mul_indicator f
@[simp]
theorem
set.indicator_inter_support
{α : Type u_1}
{M : Type u_4}
[has_zero M]
(s : set α)
(f : α → M) :
(s ∩ function.support f).indicator f = s.indicator f
theorem
set.comp_mul_indicator
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[has_one M]
(h : M → β)
(f : α → M)
{s : set α}
{x : α} :
h (s.mul_indicator f x) = s.piecewise (h ∘ f) (function.const α (h 1)) x
theorem
set.comp_indicator
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[has_zero M]
(h : M → β)
(f : α → M)
{s : set α}
{x : α} :
h (s.indicator f x) = s.piecewise (h ∘ f) (function.const α (h 0)) x
theorem
set.mul_indicator_comp_right
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[has_one M]
{s : set α}
(f : β → α)
{g : α → M}
{x : β} :
(f ⁻¹' s).mul_indicator (g ∘ f) x = s.mul_indicator g (f x)
theorem
set.mul_indicator_comp_of_one
{α : Type u_1}
{M : Type u_4}
{N : Type u_5}
[has_one M]
[has_one N]
{s : set α}
{f : α → M}
{g : M → N}
(hg : g 1 = 1) :
s.mul_indicator (g ∘ f) = g ∘ s.mul_indicator f
theorem
set.mul_indicator_rel_mul_indicator
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{f g : α → M}
{a : α}
{r : M → M → Prop}
(h1 : r 1 1)
(ha : a ∈ s → r (f a) (g a)) :
r (s.mul_indicator f a) (s.mul_indicator g a)
theorem
set.mul_indicator_union_mul_inter_apply
{α : Type u_1}
{M : Type u_4}
[mul_one_class M]
(f : α → M)
(s t : set α)
(a : α) :
((s ∪ t).mul_indicator f a) * (s ∩ t).mul_indicator f a = (s.mul_indicator f a) * t.mul_indicator f a
theorem
set.mul_indicator_union_mul_inter
{α : Type u_1}
{M : Type u_4}
[mul_one_class M]
(f : α → M)
(s t : set α) :
((s ∪ t).mul_indicator f) * (s ∩ t).mul_indicator f = (s.mul_indicator f) * t.mul_indicator f
theorem
set.mul_indicator_union_of_not_mem_inter
{α : Type u_1}
{M : Type u_4}
[mul_one_class M]
{s t : set α}
{a : α}
(h : a ∉ s ∩ t)
(f : α → M) :
(s ∪ t).mul_indicator f a = (s.mul_indicator f a) * t.mul_indicator f a
theorem
set.mul_indicator_union_of_disjoint
{α : Type u_1}
{M : Type u_4}
[mul_one_class M]
{s t : set α}
(h : disjoint s t)
(f : α → M) :
(s ∪ t).mul_indicator f = λ (a : α), (s.mul_indicator f a) * t.mul_indicator f a
theorem
set.indicator_add
{α : Type u_1}
{M : Type u_4}
[add_zero_class M]
(s : set α)
(f g : α → M) :
theorem
set.mul_indicator_mul
{α : Type u_1}
{M : Type u_4}
[mul_one_class M]
(s : set α)
(f g : α → M) :
s.mul_indicator (λ (a : α), (f a) * g a) = λ (a : α), (s.mul_indicator f a) * s.mul_indicator g a
@[simp]
theorem
set.mul_indicator_compl_mul_self_apply
{α : Type u_1}
{M : Type u_4}
[mul_one_class M]
(s : set α)
(f : α → M)
(a : α) :
(sᶜ.mul_indicator f a) * s.mul_indicator f a = f a
@[simp]
theorem
set.indicator_compl_add_self_apply
{α : Type u_1}
{M : Type u_4}
[add_zero_class M]
(s : set α)
(f : α → M)
(a : α) :
@[simp]
theorem
set.mul_indicator_compl_mul_self
{α : Type u_1}
{M : Type u_4}
[mul_one_class M]
(s : set α)
(f : α → M) :
(sᶜ.mul_indicator f) * s.mul_indicator f = f
@[simp]
theorem
set.indicator_compl_add_self
{α : Type u_1}
{M : Type u_4}
[add_zero_class M]
(s : set α)
(f : α → M) :
@[simp]
theorem
set.mul_indicator_self_mul_compl_apply
{α : Type u_1}
{M : Type u_4}
[mul_one_class M]
(s : set α)
(f : α → M)
(a : α) :
(s.mul_indicator f a) * sᶜ.mul_indicator f a = f a
@[simp]
theorem
set.indicator_self_add_compl_apply
{α : Type u_1}
{M : Type u_4}
[add_zero_class M]
(s : set α)
(f : α → M)
(a : α) :
@[simp]
theorem
set.mul_indicator_self_mul_compl
{α : Type u_1}
{M : Type u_4}
[mul_one_class M]
(s : set α)
(f : α → M) :
(s.mul_indicator f) * sᶜ.mul_indicator f = f
@[simp]
theorem
set.indicator_self_add_compl
{α : Type u_1}
{M : Type u_4}
[add_zero_class M]
(s : set α)
(f : α → M) :
theorem
set.mul_indicator_mul_eq_left
{α : Type u_1}
{M : Type u_4}
[mul_one_class M]
{f g : α → M}
(h : disjoint (function.mul_support f) (function.mul_support g)) :
(function.mul_support f).mul_indicator (f * g) = f
theorem
set.indicator_add_eq_left
{α : Type u_1}
{M : Type u_4}
[add_zero_class M]
{f g : α → M}
(h : disjoint (function.support f) (function.support g)) :
(function.support f).indicator (f + g) = f
theorem
set.indicator_add_eq_right
{α : Type u_1}
{M : Type u_4}
[add_zero_class M]
{f g : α → M}
(h : disjoint (function.support f) (function.support g)) :
(function.support g).indicator (f + g) = g
theorem
set.mul_indicator_mul_eq_right
{α : Type u_1}
{M : Type u_4}
[mul_one_class M]
{f g : α → M}
(h : disjoint (function.mul_support f) (function.mul_support g)) :
(function.mul_support g).mul_indicator (f * g) = g
def
set.mul_indicator_hom
{α : Type u_1}
(M : Type u_2)
[mul_one_class M]
(s : set α) :
(α → M) →* α → M
set.mul_indicator as a monoid_hom.
Equations
- set.mul_indicator_hom M s = {to_fun := s.mul_indicator, map_one' := _, map_mul' := _}
def
set.indicator_hom
{α : Type u_1}
(M : Type u_2)
[add_zero_class M]
(s : set α) :
(α → M) →+ α → M
set.indicator as an add_monoid_hom.
theorem
set.indicator_smul
{α : Type u_1}
{M : Type u_4}
{A : Type u_6}
[add_monoid A]
[monoid M]
[distrib_mul_action M A]
(s : set α)
(r : M)
(f : α → A) :
theorem
set.mul_indicator_inv'
{α : Type u_1}
{G : Type u_6}
[group G]
(s : set α)
(f : α → G) :
s.mul_indicator f⁻¹ = (s.mul_indicator f)⁻¹
theorem
set.mul_indicator_inv
{α : Type u_1}
{G : Type u_6}
[group G]
(s : set α)
(f : α → G) :
s.mul_indicator (λ (a : α), (f a)⁻¹) = λ (a : α), (s.mul_indicator f a)⁻¹
theorem
set.mul_indicator_compl
{α : Type u_1}
{G : Type u_6}
[group G]
(s : set α)
(f : α → G) :
sᶜ.mul_indicator f = f * (s.mul_indicator f)⁻¹
theorem
set.mul_indicator_diff
{α : Type u_1}
{G : Type u_6}
[group G]
{s t : set α}
(h : s ⊆ t)
(f : α → G) :
(t \ s).mul_indicator f = (t.mul_indicator f) * (s.mul_indicator f)⁻¹
theorem
set.prod_mul_indicator_subset_of_eq_one
{α : Type u_1}
{M : Type u_4}
{N : Type u_5}
[comm_monoid M]
[has_one N]
(f : α → N)
(g : α → N → M)
{s t : finset α}
(h : s ⊆ t)
(hg : ∀ (a : α), g a 1 = 1) :
∏ (i : α) in s, g i (f i) = ∏ (i : α) in t, g i (↑s.mul_indicator 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_of_eq_zero
{α : Type u_1}
{M : Type u_4}
{N : Type u_5}
[add_comm_monoid M]
[has_zero N]
(f : α → N)
(g : α → N → M)
{s t : finset α}
(h : s ⊆ t)
(hg : ∀ (a : α), g a 0 = 0) :
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_mul_indicator_subset
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
(f : α → M)
{s t : finset α}
(h : s ⊆ t) :
∏ (i : α) in s, f i = ∏ (i : α) in t, ↑s.mul_indicator f i
theorem
set.sum_indicator_subset
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
(f : α → M)
{s t : finset α}
(h : s ⊆ t) :
Summing an indicator function over a possibly larger finset is
the same as summing the original function over the original
finset.
theorem
set.mul_indicator_finset_prod
{α : Type u_1}
{ι : Type u_3}
{M : Type u_4}
[comm_monoid M]
(I : finset ι)
(s : set α)
(f : ι → α → M) :
s.mul_indicator (∏ (i : ι) in I, f i) = ∏ (i : ι) in I, s.mul_indicator (f i)
theorem
set.indicator_finset_sum
{α : Type u_1}
{ι : Type u_3}
{M : Type u_4}
[add_comm_monoid M]
(I : finset ι)
(s : set α)
(f : ι → α → M) :
theorem
set.mul_indicator_finset_bUnion
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{ι : Type u_2}
(I : finset ι)
(s : ι → set α)
{f : α → M} :
(∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → disjoint (s i) (s j)) → ((⋃ (i : ι) (H : i ∈ I), s i).mul_indicator f = λ (a : α), ∏ (i : ι) in I, (s i).mul_indicator f a)
theorem
set.indicator_finset_bUnion
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
{ι : Type u_2}
(I : finset ι)
(s : ι → set α)
{f : α → M} :
theorem
set.indicator_mul
{α : Type u_1}
{M : Type u_4}
[mul_zero_class M]
(s : set α)
(f g : α → M) :
theorem
set.indicator_mul_left
{α : Type u_1}
{M : Type u_4}
[mul_zero_class M]
{a : α}
(s : set α)
(f g : α → M) :
theorem
set.indicator_mul_right
{α : Type u_1}
{M : Type u_4}
[mul_zero_class M]
{a : α}
(s : set α)
(f g : α → M) :
theorem
set.one_le_mul_indicator_apply
{α : Type u_1}
{M : Type u_4}
[has_one M]
[preorder M]
{s : set α}
{f : α → M}
{a : α}
(h : a ∈ s → 1 ≤ f a) :
1 ≤ s.mul_indicator f a
theorem
set.one_le_mul_indicator
{α : Type u_1}
{M : Type u_4}
[has_one M]
[preorder M]
{s : set α}
{f : α → M}
(h : ∀ (a : α), a ∈ s → 1 ≤ f a)
(a : α) :
1 ≤ s.mul_indicator f a
theorem
set.mul_indicator_apply_le_one
{α : Type u_1}
{M : Type u_4}
[has_one M]
[preorder M]
{s : set α}
{f : α → M}
{a : α}
(h : a ∈ s → f a ≤ 1) :
s.mul_indicator f a ≤ 1
theorem
set.mul_indicator_le_one
{α : Type u_1}
{M : Type u_4}
[has_one M]
[preorder M]
{s : set α}
{f : α → M}
(h : ∀ (a : α), a ∈ s → f a ≤ 1)
(a : α) :
s.mul_indicator f a ≤ 1
theorem
set.mul_indicator_le_mul_indicator
{α : Type u_1}
{M : Type u_4}
[has_one M]
[preorder M]
{s : set α}
{f g : α → M}
{a : α}
(h : f a ≤ g a) :
s.mul_indicator f a ≤ s.mul_indicator g a
theorem
set.mul_indicator_le_mul_indicator_of_subset
{α : Type u_1}
{M : Type u_4}
[has_one M]
[preorder M]
{s t : set α}
{f : α → M}
(h : s ⊆ t)
(hf : ∀ (a : α), 1 ≤ f a)
(a : α) :
s.mul_indicator f a ≤ t.mul_indicator f a
theorem
set.mul_indicator_le_self'
{α : Type u_1}
{M : Type u_4}
[has_one M]
[preorder M]
{s : set α}
{f : α → M}
(hf : ∀ (x : α), x ∉ s → 1 ≤ f x) :
s.mul_indicator f ≤ f
theorem
set.mul_indicator_Union_apply
{α : Type u_1}
{ι : Sort u_2}
{M : Type u_3}
[complete_lattice M]
[has_one M]
(h1 : ⊥ = 1)
(s : ι → set α)
(f : α → M)
(x : α) :
(⋃ (i : ι), s i).mul_indicator f x = ⨆ (i : ι), (s i).mul_indicator f x
theorem
set.indicator_Union_apply
{α : Type u_1}
{ι : Sort u_2}
{M : Type u_3}
[complete_lattice M]
[has_zero M]
(h1 : ⊥ = 0)
(s : ι → set α)
(f : α → M)
(x : α) :
theorem
set.mul_indicator_le_self
{α : Type u_1}
{M : Type u_4}
[canonically_ordered_monoid M]
(s : set α)
(f : α → M) :
s.mul_indicator f ≤ f
theorem
set.indicator_le_self
{α : Type u_1}
{M : Type u_4}
[canonically_ordered_add_monoid M]
(s : set α)
(f : α → M) :
theorem
set.indicator_apply_le
{α : Type u_1}
{M : Type u_4}
[canonically_ordered_add_monoid M]
{a : α}
{s : set α}
{f g : α → M}
(hfg : a ∈ s → f a ≤ g a) :
theorem
set.mul_indicator_apply_le
{α : Type u_1}
{M : Type u_4}
[canonically_ordered_monoid M]
{a : α}
{s : set α}
{f g : α → M}
(hfg : a ∈ s → f a ≤ g a) :
s.mul_indicator f a ≤ g a
theorem
set.indicator_le
{α : Type u_1}
{M : Type u_4}
[canonically_ordered_add_monoid M]
{s : set α}
{f g : α → M}
(hfg : ∀ (a : α), a ∈ s → f a ≤ g a) :
theorem
set.mul_indicator_le
{α : Type u_1}
{M : Type u_4}
[canonically_ordered_monoid M]
{s : set α}
{f g : α → M}
(hfg : ∀ (a : α), a ∈ s → f a ≤ g a) :
s.mul_indicator f ≤ g
theorem
add_monoid_hom.map_indicator
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[add_monoid M]
[add_monoid N]
(f : M →+ N)
(s : set α)
(g : α → M)
(x : α) :
theorem
monoid_hom.map_mul_indicator
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[monoid M]
[monoid N]
(f : M →* N)
(s : set α)
(g : α → M)
(x : α) :
⇑f (s.mul_indicator g x) = s.mul_indicator (⇑f ∘ g) x