Indicator function #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
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
@[simp]
theorem
set.piecewise_eq_mul_indicator
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{f : α → M}
[decidable_pred (λ (_x : α), _x ∈ s)] :
s.piecewise f 1 = s.mul_indicator f
@[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_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
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_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.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
theorem
set.mul_indicator_apply_ne_one
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{f : α → M}
{a : α} :
s.mul_indicator f a ≠ 1 ↔ a ∈ s ∩ function.mul_support f
@[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 1 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
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
theorem
set.mul_indicator_empty'
{α : Type u_1}
{M : Type u_4}
[has_one M]
(f : α → M) :
∅.mul_indicator f = 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
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 : α}
[decidable_pred (λ (_x : α), _x ∈ s)] :
h (s.mul_indicator f x) = s.piecewise (h ∘ f) (function.const α (h 1)) 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_image
{α : Type u_1}
{β : Type u_2}
{M : Type u_4}
[has_one M]
{s : set α}
{f : β → M}
{g : α → β}
(hg : function.injective g)
{x : α} :
(g '' s).mul_indicator f (g x) = s.mul_indicator (f ∘ g) x
theorem
set.comp_mul_indicator_const
{α : Type u_1}
{M : Type u_4}
{N : Type u_5}
[has_one M]
[has_one N]
{s : set α}
(c : M)
(f : M → N)
(hf : f 1 = 1) :
(λ (x : α), f (s.mul_indicator (λ (x : α), c) x)) = s.mul_indicator (λ (x : α), f c)
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.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
theorem
set.mul_indicator_mul'
{α : Type u_1}
{M : Type u_4}
[mul_one_class M]
(s : set α)
(f g : α → M) :
s.mul_indicator (f * g) = s.mul_indicator f * s.mul_indicator g
@[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.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.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.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
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
theorem
set.mul_indicator_mul_compl_eq_piecewise
{α : Type u_1}
{M : Type u_4}
[mul_one_class M]
{s : set α}
[decidable_pred (λ (_x : α), _x ∈ s)]
(f g : α → M) :
s.mul_indicator f * sᶜ.mul_indicator g = s.piecewise f g
theorem
set.indicator_add_compl_eq_piecewise
{α : Type u_1}
{M : Type u_4}
[add_zero_class M]
{s : set α}
[decidable_pred (λ (_x : α), _x ∈ s)]
(f g : α → M) :
noncomputable
def
set.mul_indicator_hom
{α : Type u_1}
(M : Type u_2)
[mul_one_class M]
(s : set α) :
set.mul_indicator as a monoid_hom.
Equations
- set.mul_indicator_hom M s = {to_fun := s.mul_indicator, map_one' := _, map_mul' := _}
set.indicator as an add_monoid_hom.
theorem
set.indicator_const_smul_apply
{α : 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)
(x : α) :
theorem
set.indicator_const_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_div
{α : Type u_1}
{G : Type u_6}
[group G]
(s : set α)
(f g : α → G) :
s.mul_indicator (λ (a : α), f a / g a) = λ (a : α), s.mul_indicator f a / s.mul_indicator g a
theorem
set.mul_indicator_div'
{α : Type u_1}
{G : Type u_6}
[group G]
(s : set α)
(f g : α → G) :
s.mul_indicator (f / g) = s.mul_indicator f / s.mul_indicator g
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) :
s.prod (λ (i : α), g i (f i)) = t.prod (λ (i : α), 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) :
s.prod (λ (i : α), f i) = t.prod (λ (i : α), ↑s.mul_indicator 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
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
finset.sum_indicator_eq_sum_filter
{α : Type u_1}
{ι : Type u_3}
{M : Type u_4}
[add_comm_monoid M]
(s : finset ι)
(f : ι → α → M)
(t : ι → set α)
(g : ι → α)
[decidable_pred (λ (i : ι), g i ∈ t i)] :
theorem
finset.prod_mul_indicator_eq_prod_filter
{α : Type u_1}
{ι : Type u_3}
{M : Type u_4}
[comm_monoid M]
(s : finset ι)
(f : ι → α → M)
(t : ι → set α)
(g : ι → α)
[decidable_pred (λ (i : ι), g i ∈ t i)] :
s.prod (λ (i : ι), (t i).mul_indicator (f i) (g i)) = (finset.filter (λ (i : ι), g i ∈ t i) s).prod (λ (i : ι), f i (g i))
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.prod (λ (i : ι), f i)) = I.prod (λ (i : ι), s.mul_indicator (f i))
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} :
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.mul_indicator_finset_bUnion_apply
{α : Type u_1}
{M : Type u_4}
[comm_monoid M]
{ι : Type u_2}
(I : finset ι)
(s : ι → set α)
{f : α → M}
(h : ∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → disjoint (s i) (s j))
(x : α) :
(⋃ (i : ι) (H : i ∈ I), s i).mul_indicator f x = I.prod (λ (i : ι), (s i).mul_indicator f x)
theorem
set.indicator_eq_zero_iff_not_mem
{α : Type u_1}
(M : Type u_4)
[mul_zero_one_class M]
[nontrivial M]
{U : set α}
{x : α} :
theorem
set.indicator_eq_one_iff_mem
{α : Type u_1}
(M : Type u_4)
[mul_zero_one_class M]
[nontrivial M]
{U : set α}
{x : α} :
theorem
set.indicator_one_inj
{α : Type u_1}
(M : Type u_4)
[mul_zero_one_class M]
[nontrivial M]
{U V : set α}
(h : U.indicator 1 = V.indicator 1) :
U = V
theorem
set.mul_indicator_le_mul_indicator
{α : Type u_1}
{M : Type u_4}
[has_one M]
{s : set α}
{f g : α → M}
{a : α}
[preorder M]
(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]
{s t : set α}
{f : α → M}
[preorder M]
(h : s ⊆ t)
(hf : ∀ (a : α), 1 ≤ f a)
(a : α) :
s.mul_indicator f a ≤ t.mul_indicator f a
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.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.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.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
monoid_hom.map_mul_indicator
{α : Type u_1}
{M : Type u_2}
{N : Type u_3}
[mul_one_class M]
[mul_one_class N]
(f : M →* N)
(s : set α)
(g : α → M)
(x : α) :
⇑f (s.mul_indicator g x) = s.mul_indicator (⇑f ∘ g) x