mathlib documentation

data.indicator_function

Indicator function

indicator (s : set α) (f : α → β) (a : α) is f a if a ∈ s and is 0 otherwise.

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

def set.indicator {α : Type u_1} {β : Type u_3} [has_zero β] :
set α(α → β)α → β

indicator s f a is f a if a ∈ s, 0 otherwise.

Equations
@[simp]
theorem set.piecewise_eq_indicator {α : Type u_1} {β : Type u_3} [has_zero β] {f : α → β} {s : set α} :

theorem set.indicator_apply {α : Type u_1} {β : Type u_3} [has_zero β] (s : set α) (f : α → β) (a : α) :
s.indicator f a = ite (a s) (f a) 0

@[simp]
theorem set.indicator_of_mem {α : Type u_1} {β : Type u_3} [has_zero β] {s : set α} {a : α} (h : a s) (f : α → β) :
s.indicator f a = f a

@[simp]
theorem set.indicator_of_not_mem {α : Type u_1} {β : Type u_3} [has_zero β] {s : set α} {a : α} (h : a s) (f : α → β) :
s.indicator f a = 0

theorem set.indicator_eq_zero_or_self {α : Type u_1} {β : Type u_3} [has_zero β] (s : set α) (f : α → β) (a : α) :
s.indicator f a = 0 s.indicator f a = f a

theorem set.mem_of_indicator_ne_zero {α : Type u_1} {β : Type u_3} [has_zero β] {s : set α} {f : α → β} {a : α} :
s.indicator f a 0a s

If an indicator function is nonzero at a point, that point is in the set.

theorem set.eq_on_indicator {α : Type u_1} {β : Type u_3} [has_zero β] {s : set α} {f : α → β} :

theorem set.support_indicator {α : Type u_1} {β : Type u_3} [has_zero β] {s : set α} {f : α → β} :

theorem set.indicator_of_support_subset {α : Type u_1} {β : Type u_3} [has_zero β] {s : set α} {f : α → β} :

@[simp]
theorem set.indicator_support {α : Type u_1} {β : Type u_3} [has_zero β] {f : α → β} :

@[simp]
theorem set.indicator_range_comp {α : Type u_1} {β : Type u_3} [has_zero β] {ι : Sort u_2} (f : ι → α) (g : α → β) :

theorem set.indicator_congr {α : Type u_1} {β : Type u_3} [has_zero β] {s : set α} {f g : α → β} :
(∀ (a : α), a sf a = g a)s.indicator f = s.indicator g

@[simp]
theorem set.indicator_univ {α : Type u_1} {β : Type u_3} [has_zero β] (f : α → β) :

@[simp]
theorem set.indicator_empty {α : Type u_1} {β : Type u_3} [has_zero β] (f : α → β) :
.indicator f = λ (a : α), 0

@[simp]
theorem set.indicator_zero {α : Type u_1} (β : Type u_3) [has_zero β] (s : set α) :
s.indicator (λ (x : α), 0) = λ (x : α), 0

@[simp]
theorem set.indicator_zero' {α : Type u_1} (β : Type u_3) [has_zero β] {s : set α} :
s.indicator 0 = 0

theorem set.indicator_indicator {α : Type u_1} {β : Type u_3} [has_zero β] (s t : set α) (f : α → β) :

theorem set.comp_indicator {α : Type u_1} {β : Type u_3} {γ : Type u_4} [has_zero β] (h : β → γ) (f : α → β) {s : set α} {x : α} :
h (s.indicator f x) = s.piecewise (h f) (function.const α (h 0)) x

theorem set.indicator_comp_right {α : Type u_1} {β : Type u_3} {γ : Type u_4} [has_zero β] {s : set α} (f : γ → α) {g : α → β} {x : γ} :
(f ⁻¹' s).indicator (g f) x = s.indicator g (f x)

theorem set.indicator_comp_of_zero {α : Type u_1} {β : Type u_3} {γ : Type u_4} [has_zero β] {s : set α} {f : α → β} [has_zero γ] {g : β → γ} :
g 0 = 0s.indicator (g f) = g s.indicator f

theorem set.indicator_preimage {α : Type u_1} {β : Type u_3} [has_zero β] (s : set α) (f : α → β) (B : set β) :
s.indicator f ⁻¹' B = s f ⁻¹' B s (λ (a : α), 0) ⁻¹' B

theorem set.indicator_preimage_of_not_mem {α : Type u_1} {β : Type u_3} [has_zero β] (s : set α) (f : α → β) {t : set β} :
0 ts.indicator f ⁻¹' t = s f ⁻¹' t

theorem set.mem_range_indicator {α : Type u_1} {β : Type u_3} [has_zero β] {r : β} {s : set α} {f : α → β} :

theorem set.indicator_rel_indicator {α : Type u_1} {β : Type u_3} [has_zero β] {s : set α} {f g : α → β} {a : α} {r : β → β → Prop} :
r 0 0(a sr (f a) (g a))r (s.indicator f a) (s.indicator g a)

theorem set.sum_indicator_subset_of_eq_zero {α : Type u_1} {β : Type u_3} [has_zero β] {γ : Type u_2} [add_comm_monoid γ] (f : α → β) (g : α → β → γ) {s₁ s₂ : finset α} :
s₁ s₂(∀ (a : α), g a 0 = 0)∑ (i : α) in s₁, g i (f i) = ∑ (i : α) in s₂, g i (s₁.indicator 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

  1. (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.sum_indicator_subset {α : Type u_1} {γ : Type u_2} [add_comm_monoid γ] (f : α → γ) {s₁ s₂ : finset α} :
s₁ s₂∑ (i : α) in s₁, f i = ∑ (i : α) in s₂, s₁.indicator 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.indicator_union_of_not_mem_inter {α : Type u_1} {β : Type u_3} [add_monoid β] {s t : set α} {a : α} (h : a s t) (f : α → β) :
(s t).indicator f a = s.indicator f a + t.indicator f a

theorem set.indicator_union_of_disjoint {α : Type u_1} {β : Type u_3} [add_monoid β] {s t : set α} (h : disjoint s t) (f : α → β) :
(s t).indicator f = λ (a : α), s.indicator f a + t.indicator f a

theorem set.indicator_add {α : Type u_1} {β : Type u_3} [add_monoid β] (s : set α) (f g : α → β) :
s.indicator (λ (a : α), f a + g a) = λ (a : α), s.indicator f a + s.indicator g a

@[simp]
theorem set.indicator_compl_add_self_apply {α : Type u_1} {β : Type u_3} [add_monoid β] (s : set α) (f : α → β) (a : α) :
s.indicator f a + s.indicator f a = f a

@[simp]
theorem set.indicator_compl_add_self {α : Type u_1} {β : Type u_3} [add_monoid β] (s : set α) (f : α → β) :

@[simp]
theorem set.indicator_self_add_compl_apply {α : Type u_1} {β : Type u_3} [add_monoid β] (s : set α) (f : α → β) (a : α) :
s.indicator f a + s.indicator f a = f a

@[simp]
theorem set.indicator_self_add_compl {α : Type u_1} {β : Type u_3} [add_monoid β] (s : set α) (f : α → β) :

@[instance]
def set.is_add_monoid_hom.indicator {α : Type u_1} (β : Type u_3) [add_monoid β] (s : set α) :
is_add_monoid_hom (λ (f : α → β), s.indicator f)

theorem set.indicator_smul {α : Type u_1} {β : Type u_3} [add_monoid β] {𝕜 : Type u_5} [monoid 𝕜] [distrib_mul_action 𝕜 β] (s : set α) (r : 𝕜) (f : α → β) :
s.indicator (λ (x : α), r f x) = λ (x : α), r s.indicator f x

theorem set.indicator_add_eq_left {α : Type u_1} {β : Type u_3} [add_monoid β] {f g : α → β} :
set.univ f ⁻¹' {0} g ⁻¹' {0}(f ⁻¹' {0}).indicator (f + g) = f

theorem set.indicator_add_eq_right {α : Type u_1} {β : Type u_3} [add_monoid β] {f g : α → β} :
set.univ f ⁻¹' {0} g ⁻¹' {0}(g ⁻¹' {0}).indicator (f + g) = g

@[instance]
def set.is_add_group_hom.indicator {α : Type u_1} (β : Type u_3) [add_group β] (s : set α) :
is_add_group_hom (λ (f : α → β), s.indicator f)

theorem set.indicator_neg {α : Type u_1} {β : Type u_3} [add_group β] (s : set α) (f : α → β) :
s.indicator (λ (a : α), -f a) = λ (a : α), -s.indicator f a

theorem set.indicator_sub {α : Type u_1} {β : Type u_3} [add_group β] (s : set α) (f g : α → β) :
s.indicator (λ (a : α), f a - g a) = λ (a : α), s.indicator f a - s.indicator g a

theorem set.indicator_compl {α : Type u_1} {β : Type u_3} [add_group β] (s : set α) (f : α → β) :

theorem set.indicator_finset_sum {α : Type u_1} {β : Type u_2} [add_comm_monoid β] {ι : Type u_3} (I : finset ι) (s : set α) (f : ι → α → β) :
s.indicator (∑ (i : ι) in I, f i) = ∑ (i : ι) in I, s.indicator (f i)

theorem set.indicator_finset_bUnion {α : Type u_1} {β : Type u_2} [add_comm_monoid β] {ι : Type u_3} (I : finset ι) (s : ι → set α) {f : α → β} :
(∀ (i : ι), i I∀ (j : ι), j Ii js i s j = )((⋃ (i : ι) (H : i I), s i).indicator f = λ (a : α), ∑ (i : ι) in I, (s i).indicator f a)

theorem set.indicator_mul {α : Type u_1} {β : Type u_3} [mul_zero_class β] (s : set α) (f g : α → β) :
s.indicator (λ (a : α), (f a) * g a) = λ (a : α), (s.indicator f a) * s.indicator g a

theorem set.indicator_mul_left {α : Type u_1} {β : Type u_3} [mul_zero_class β] {a : α} (s : set α) (f g : α → β) :
s.indicator (λ (a : α), (f a) * g a) a = (s.indicator f a) * g a

theorem set.indicator_mul_right {α : Type u_1} {β : Type u_3} [mul_zero_class β] {a : α} (s : set α) (f g : α → β) :
s.indicator (λ (a : α), (f a) * g a) a = (f a) * s.indicator g a

theorem set.indicator_prod_one {α : Type u_1} {α' : Type u_2} {β : Type u_3} [monoid_with_zero β] {s : set α} {t : set α'} {x : α} {y : α'} :
(s.prod t).indicator 1 (x, y) = (s.indicator 1 x) * t.indicator 1 y

theorem set.indicator_nonneg' {α : Type u_1} {β : Type u_3} [has_zero β] [preorder β] {s : set α} {f : α → β} {a : α} :
(a s0 f a)0 s.indicator f a

theorem set.indicator_nonneg {α : Type u_1} {β : Type u_3} [has_zero β] [preorder β] {s : set α} {f : α → β} (h : ∀ (a : α), a s0 f a) (a : α) :
0 s.indicator f a

theorem set.indicator_nonpos' {α : Type u_1} {β : Type u_3} [has_zero β] [preorder β] {s : set α} {f : α → β} {a : α} :
(a sf a 0)s.indicator f a 0

theorem set.indicator_nonpos {α : Type u_1} {β : Type u_3} [has_zero β] [preorder β] {s : set α} {f : α → β} (h : ∀ (a : α), a sf a 0) (a : α) :
s.indicator f a 0

theorem set.indicator_le' {α : Type u_1} {β : Type u_3} [has_zero β] [preorder β] {s : set α} {f g : α → β} :
(∀ (a : α), a sf a g a)(∀ (a : α), a s0 g a)s.indicator f g

theorem set.indicator_le_indicator {α : Type u_1} {β : Type u_3} [has_zero β] [preorder β] {s : set α} {f g : α → β} {a : α} :
f a g as.indicator f a s.indicator g a

theorem set.indicator_le_indicator_of_subset {α : Type u_1} {β : Type u_3} [has_zero β] [preorder β] {s t : set α} {f : α → β} (h : s t) (hf : ∀ (a : α), 0 f a) (a : α) :
s.indicator f a t.indicator f a

theorem set.indicator_le_self' {α : Type u_1} {β : Type u_3} [has_zero β] [preorder β] {s : set α} {f : α → β} :
(∀ (x : α), x s0 f x)s.indicator f f

theorem set.indicator_le_self {α : Type u_1} {β : Type u_2} [canonically_ordered_add_monoid β] (s : set α) (f : α → β) :

theorem set.indicator_le {α : Type u_1} {β : Type u_2} [canonically_ordered_add_monoid β] {s : set α} {f g : α → β} :
(∀ (a : α), a sf a g a)s.indicator f g

theorem set.indicator_Union_apply {α : Type u_1} {ι : Sort u_2} {β : Type u_3} [complete_lattice β] [has_zero β] (h0 : = 0) (s : ι → set α) (f : α → β) (x : α) :
(⋃ (i : ι), s i).indicator f x = ⨆ (i : ι), (s i).indicator f x

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 : α) :
f (s.indicator g x) = s.indicator (f g) x