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_2} [has_zero β] (s : set α) (f : α → β) (a : α) :

β

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

Equations

s.indicator f = λ (x : α), ite (x ∈ s) (f x) 0

@[simp]

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

s.piecewise f 0 = s.indicator f

theorem set.indicator_apply {α : Type u_1} {β : Type u_2} [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_2} [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_2} [has_zero β] {s : set α} {a : α} (h : a ∉ s) (f : α → β) :

s.indicator f a = 0

theorem set.mem_of_indicator_ne_zero {α : Type u_1} {β : Type u_2} [has_zero β] {s : set α} {f : α → β} {a : α} (h : s.indicator f a ≠ 0) :

a ∈ 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_2} [has_zero β] {s : set α} {f : α → β} :

set.eq_on (s.indicator f) f s

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

function.support (s.indicator f) ⊆ s

@[simp]

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

(set.range f).indicator g ∘ f = g ∘ f

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

s.indicator f = s.indicator g

@[simp]

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

set.univ.indicator f = f

@[simp]

theorem set.indicator_empty {α : Type u_1} {β : Type u_2} [has_zero β] (f : α → β) :

∅.indicator f = λ (a : α), 0

@[simp]

theorem set.indicator_zero {α : Type u_1} (β : Type u_2) [has_zero β] (s : set α) :

s.indicator (λ (x : α), 0) = λ (x : α), 0

@[simp]

theorem set.indicator_zero' {α : Type u_1} (β : Type u_2) [has_zero β] {s : set α} :

s.indicator 0 = 0

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

s.indicator (t.indicator f) = (s ∩ t).indicator f

theorem set.comp_indicator {α : Type u_1} {β : Type u_2} {γ : Type u_3} [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_of_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero β] {s : set α} {f : α → β} [has_zero γ] {g : β → γ} (hg : g 0 = 0) :

s.indicator (g ∘ f) = g ∘ s.indicator f

theorem set.indicator_preimage {α : Type u_1} {β : Type u_2} [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_2} [has_zero β] (s : set α) (f : α → β) {t : set β} (ht : 0 ∉ t) :

s.indicator f ⁻¹' t = s ∩ f ⁻¹' t

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

r ∈ set.range (s.indicator f) ↔ r = 0 ∧ s ≠ set.univ ∨ r ∈ f '' s

theorem set.indicator_rel_indicator {α : Type u_1} {β : Type u_2} [has_zero β] {s : set α} {f g : α → β} {a : α} {r : β → β → Prop} (h0 : r 0 0) (ha : a ∈ s → r (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_2} [has_zero β] {γ : Type u_3} [add_comm_monoid γ] (f : α → β) (g : α → β → γ) {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) (hg : ∀ (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

(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 α} (h : 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_2} [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_2} [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_2} [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_2} [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_2} [add_monoid β] (s : set α) (f : α → β) :

sᶜ.indicator f + s.indicator f = f

@[simp]

theorem set.indicator_self_add_compl_apply {α : Type u_1} {β : Type u_2} [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_2} [add_monoid β] (s : set α) (f : α → β) :

s.indicator f + sᶜ.indicator f = f

@[instance]

def set.is_add_monoid_hom.indicator {α : Type u_1} (β : Type u_2) [add_monoid β] (s : set α) :

is_add_monoid_hom (λ (f : α → β), s.indicator f)

theorem set.indicator_smul {α : Type u_1} {β : Type u_2} [add_monoid β] {𝕜 : Type u_4} [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_2} [add_monoid β] {f g : α → β} (h : set.univ ⊆ f ⁻¹' {0} ∪ g ⁻¹' {0}) :

(f ⁻¹' {0})ᶜ.indicator (f + g) = f

theorem set.indicator_add_eq_right {α : Type u_1} {β : Type u_2} [add_monoid β] {f g : α → β} (h : 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_2) [add_group β] (s : set α) :

is_add_group_hom (λ (f : α → β), s.indicator f)

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

s.indicator (λ (a : α), -f a) = λ (a : α), -s.indicator f a

theorem set.indicator_sub {α : Type u_1} {β : Type u_2} [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_2} [add_group β] (s : set α) (f : α → β) :

sᶜ.indicator f = f - s.indicator 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 : α → β} (a : ∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → s 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_2} [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_nonneg' {α : Type u_1} {β : Type u_2} [has_zero β] [preorder β] {s : set α} {f : α → β} {a : α} (h : a ∈ s → 0 ≤ f a) :

0 ≤ s.indicator f a

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

0 ≤ s.indicator f a

theorem set.indicator_nonpos' {α : Type u_1} {β : Type u_2} [has_zero β] [preorder β] {s : set α} {f : α → β} {a : α} (h : a ∈ s → f a ≤ 0) :

s.indicator f a ≤ 0

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

s.indicator f a ≤ 0

theorem set.indicator_le' {α : Type u_1} {β : Type u_2} [has_zero β] [preorder β] {s : set α} {f g : α → β} (hfg : ∀ (a : α), a ∈ s → f a ≤ g a) (hg : ∀ (a : α), a ∉ s → 0 ≤ g a) :

s.indicator f ≤ g

theorem set.indicator_le_indicator {α : Type u_1} {β : Type u_2} [has_zero β] [preorder β] {s : set α} {f g : α → β} {a : α} (h : f a ≤ g a) :

s.indicator f a ≤ s.indicator g a

theorem set.indicator_le_indicator_of_subset {α : Type u_1} {β : Type u_2} [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_2} [has_zero β] [preorder β] {s : set α} {f : α → β} (hf : ∀ (x : α), x ∉ s → 0 ≤ f x) :

s.indicator f ≤ f

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

s.indicator f ≤ f

theorem set.indicator_le {α : Type u_1} {β : Type u_2} [canonically_ordered_add_monoid β] {s : set α} {f g : α → β} (hfg : ∀ (a : α), a ∈ s → f 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