mathlib documentation

algebra.indicator_function

Indicator function #

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

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

Equations
noncomputable def set.mul_indicator {α : Type u_1} {M : Type u_4} [has_one M] (s : set α) (f : α → M) :
α → M

mul_indicator s f a is f a if a ∈ s, 1 otherwise.

Equations
@[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)] :
@[simp]
theorem set.piecewise_eq_indicator {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f : α → M} [decidable_pred (λ (_x : α), _x s)] :
theorem set.mul_indicator_apply {α : Type u_1} {M : Type u_4} [has_one M] (s : set α) (f : α → M) (a : α) [decidable (a s)] :
s.mul_indicator f a = ite (a s) (f a) 1
theorem set.indicator_apply {α : Type u_1} {M : Type u_4} [has_zero M] (s : set α) (f : α → M) (a : α) [decidable (a s)] :
s.indicator f a = ite (a s) (f a) 0
@[simp]
theorem set.indicator_of_mem {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {a : α} (h : a s) (f : α → M) :
s.indicator f a = f a
@[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.indicator_of_not_mem {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {a : α} (h : a s) (f : α → M) :
s.indicator f a = 0
@[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) :
theorem set.indicator_eq_zero_or_self {α : Type u_1} {M : Type u_4} [has_zero M] (s : set α) (f : α → M) (a : α) :
s.indicator f a = 0 s.indicator f a = f a
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.indicator_apply_eq_self {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f : α → M} {a : α} :
s.indicator f a = f a a sf a = 0
@[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 sf a = 1
@[simp]
theorem set.mul_indicator_eq_self {α : Type u_1} {M : Type u_4} [has_one M] {s : set α} {f : α → M} :
@[simp]
theorem set.indicator_eq_self {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f : α → M} :
theorem set.indicator_eq_self_of_superset {α : Type u_1} {M : Type u_4} [has_zero M] {s t : set α} {f : α → M} (h1 : s.indicator f = f) (h2 : s t) :
t.indicator f = f
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) :
@[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 sf a = 1
@[simp]
theorem set.indicator_apply_eq_zero {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f : α → M} {a : α} :
s.indicator f a = 0 a sf a = 0
@[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} :
@[simp]
theorem set.mul_indicator_eq_one' {α : Type u_1} {M : Type u_4} [has_one M] {s : set α} {f : α → M} :
theorem set.mul_indicator_apply_ne_one {α : Type u_1} {M : Type u_4} [has_one M] {s : set α} {f : α → M} {a : α} :
theorem set.indicator_apply_ne_zero {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f : α → M} {a : α} :
@[simp]
theorem set.mul_support_mul_indicator {α : Type u_1} {M : Type u_4} [has_one M] {s : set α} {f : α → M} :
@[simp]
theorem set.support_indicator {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f : α → M} :
theorem set.mem_of_indicator_ne_zero {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f : α → M} {a : α} (h : s.indicator 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_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} :
theorem set.eq_on_indicator {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f : α → M} :
theorem set.support_indicator_subset {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f : α → M} :
theorem set.mul_support_mul_indicator_subset {α : Type u_1} {M : Type u_4} [has_one M] {s : set α} {f : α → M} :
@[simp]
theorem set.mul_indicator_mul_support {α : Type u_1} {M : Type u_4} [has_one M] {f : α → M} :
@[simp]
theorem set.indicator_support {α : Type u_1} {M : Type u_4} [has_zero M] {f : α → M} :
@[simp]
theorem set.mul_indicator_range_comp {α : Type u_1} {M : Type u_4} [has_one M] {ι : Sort u_2} (f : ι → α) (g : α → M) :
@[simp]
theorem set.indicator_range_comp {α : Type u_1} {M : Type u_4} [has_zero M] {ι : Sort u_2} (f : ι → α) (g : α → M) :
theorem set.indicator_congr {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f g : α → M} (h : set.eq_on f g s) :
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) :
@[simp]
theorem set.indicator_univ {α : Type u_1} {M : Type u_4} [has_zero M] (f : α → M) :
@[simp]
theorem set.mul_indicator_univ {α : Type u_1} {M : Type u_4} [has_one M] (f : α → M) :
@[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.indicator_empty {α : Type u_1} {M : Type u_4} [has_zero M] (f : α → M) :
.indicator f = λ (a : α), 0
theorem set.indicator_empty' {α : Type u_1} {M : Type u_4} [has_zero M] (f : α → M) :
theorem set.mul_indicator_empty' {α : Type u_1} {M : Type u_4} [has_one M] (f : α → M) :
@[simp]
theorem set.indicator_zero {α : Type u_1} (M : Type u_4) [has_zero M] (s : set α) :
s.indicator (λ (x : α), 0) = λ (x : α), 0
@[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.indicator_zero' {α : Type u_1} (M : Type u_4) [has_zero M] {s : set α} :
s.indicator 0 = 0
@[simp]
theorem set.mul_indicator_one' {α : Type u_1} (M : Type u_4) [has_one M] {s : set α} :
theorem set.mul_indicator_mul_indicator {α : Type u_1} {M : Type u_4} [has_one M] (s t : set α) (f : α → M) :
theorem set.indicator_indicator {α : Type u_1} {M : Type u_4} [has_zero M] (s t : set α) (f : α → M) :
@[simp]
theorem set.mul_indicator_inter_mul_support {α : Type u_1} {M : Type u_4} [has_one M] (s : set α) (f : α → M) :
@[simp]
theorem set.indicator_inter_support {α : Type u_1} {M : Type u_4} [has_zero M] (s : set α) (f : α → M) :
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.comp_indicator {α : Type u_1} {β : Type u_2} {M : Type u_4} [has_zero M] (h : M → β) (f : α → M) {s : set α} {x : α} [decidable_pred (λ (_x : α), _x s)] :
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.indicator_comp_right {α : Type u_1} {β : Type u_2} {M : Type u_4} [has_zero M] {s : set α} (f : β → α) {g : α → M} {x : β} :
(f ⁻¹' s).indicator (g f) x = s.indicator g (f x)
theorem set.indicator_image {α : Type u_1} {β : Type u_2} {M : Type u_4} [has_zero M] {s : set α} {f : β → M} {g : α → β} (hg : function.injective g) {x : α} :
(g '' s).indicator f (g x) = s.indicator (f g) 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.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) :
theorem set.indicator_comp_of_zero {α : Type u_1} {M : Type u_4} {N : Type u_5} [has_zero M] [has_zero N] {s : set α} {f : α → M} {g : M → N} (hg : g 0 = 0) :
s.indicator (g f) = g s.indicator f
theorem set.comp_indicator_const {α : Type u_1} {M : Type u_4} {N : Type u_5} [has_zero M] [has_zero N] {s : set α} (c : M) (f : M → N) (hf : f 0 = 0) :
(λ (x : α), f (s.indicator (λ (x : α), c) x)) = s.indicator (λ (x : α), f c)
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_preimage {α : Type u_1} {M : Type u_4} [has_one M] (s : set α) (f : α → M) (B : set M) :
s.mul_indicator f ⁻¹' B = s.ite (f ⁻¹' B) (1 ⁻¹' B)
theorem set.indicator_preimage {α : Type u_1} {M : Type u_4} [has_zero M] (s : set α) (f : α → M) (B : set M) :
s.indicator f ⁻¹' B = s.ite (f ⁻¹' B) (0 ⁻¹' B)
theorem set.mul_indicator_preimage_of_not_mem {α : Type u_1} {M : Type u_4} [has_one M] (s : set α) (f : α → M) {t : set M} (ht : 1 t) :
theorem set.indicator_preimage_of_not_mem {α : Type u_1} {M : Type u_4} [has_zero M] (s : set α) (f : α → M) {t : set M} (ht : 0 t) :
theorem set.mem_range_indicator {α : Type u_1} {M : Type u_4} [has_zero M] {r : M} {s : set α} {f : α → M} :
theorem set.mem_range_mul_indicator {α : Type u_1} {M : Type u_4} [has_one M] {r : M} {s : set α} {f : α → M} :
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 sr (f a) (g a)) :
r (s.mul_indicator f a) (s.mul_indicator g a)
theorem set.indicator_rel_indicator {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f g : α → M} {a : α} {r : M → M → Prop} (h1 : r 0 0) (ha : a sr (f a) (g a)) :
r (s.indicator f a) (s.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 : α) :
theorem set.indicator_union_add_inter_apply {α : Type u_1} {M : Type u_4} [add_zero_class M] (f : α → M) (s t : set α) (a : α) :
(s t).indicator f a + (s t).indicator f a = s.indicator f a + t.indicator f a
theorem set.indicator_union_add_inter {α : Type u_1} {M : Type u_4} [add_zero_class M] (f : α → M) (s t : set α) :
(s t).indicator f + (s t).indicator f = s.indicator f + t.indicator f
theorem set.mul_indicator_union_mul_inter {α : Type u_1} {M : Type u_4} [mul_one_class M] (f : α → M) (s t : set α) :
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) :
theorem set.indicator_union_of_not_mem_inter {α : Type u_1} {M : Type u_4} [add_zero_class M] {s t : set α} {a : α} (h : a s t) (f : α → M) :
(s t).indicator f a = s.indicator f a + t.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_union_of_disjoint {α : Type u_1} {M : Type u_4} [add_zero_class M] {s t : set α} (h : disjoint s t) (f : α → M) :
(s t).indicator f = λ (a : α), s.indicator f a + t.indicator f a
theorem set.indicator_add {α : Type u_1} {M : Type u_4} [add_zero_class M] (s : set α) (f g : α → M) :
s.indicator (λ (a : α), f a + g a) = λ (a : α), s.indicator f a + s.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 (λ (a : α), f a * g a) = λ (a : α), s.mul_indicator f a * s.mul_indicator g a
theorem set.indicator_add' {α : Type u_1} {M : Type u_4} [add_zero_class M] (s : set α) (f g : α → M) :
s.indicator (f + g) = s.indicator f + s.indicator g
theorem set.mul_indicator_mul' {α : Type u_1} {M : Type u_4} [mul_one_class M] (s : set α) (f g : α → M) :
@[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 : α) :
@[simp]
theorem set.indicator_compl_add_self_apply {α : Type u_1} {M : Type u_4} [add_zero_class M] (s : set α) (f : α → M) (a : α) :
s.indicator f a + s.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) :
@[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 : α) :
@[simp]
theorem set.indicator_self_add_compl_apply {α : Type u_1} {M : Type u_4} [add_zero_class M] (s : set α) (f : α → M) (a : α) :
s.indicator f a + s.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) :
@[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)) :
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)) :
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)) :
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)) :
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) :
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 α) :
(α → M) →* α → M

set.mul_indicator as a monoid_hom.

Equations
noncomputable 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.

Equations
theorem set.indicator_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 : α) :
s.indicator (λ (x : α), r x f x) x = r x s.indicator f x
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) :
s.indicator (λ (x : α), r x f x) = λ (x : α), r x s.indicator f x
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 : α) :
s.indicator (λ (x : α), r f x) x = r s.indicator f 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) :
s.indicator (λ (x : α), r f x) = λ (x : α), r s.indicator f x
theorem set.indicator_neg' {α : Type u_1} {G : Type u_6} [add_group G] (s : set α) (f : α → G) :
theorem set.mul_indicator_inv' {α : Type u_1} {G : Type u_6} [group G] (s : set α) (f : α → G) :
theorem set.indicator_neg {α : Type u_1} {G : Type u_6} [add_group G] (s : set α) (f : α → G) :
s.indicator (λ (a : α), -f a) = λ (a : α), -s.indicator f a
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.indicator_sub {α : Type u_1} {G : Type u_6} [add_group G] (s : set α) (f g : α → G) :
s.indicator (λ (a : α), f a - g a) = λ (a : α), s.indicator f a - s.indicator g a
theorem set.mul_indicator_div' {α : Type u_1} {G : Type u_6} [group G] (s : set α) (f g : α → G) :
theorem set.indicator_sub' {α : Type u_1} {G : Type u_6} [add_group G] (s : set α) (f g : α → G) :
s.indicator (f - g) = s.indicator f - s.indicator g
theorem set.indicator_compl' {α : Type u_1} {G : Type u_6} [add_group G] (s : set α) (f : α → G) :
theorem set.mul_indicator_compl {α : Type u_1} {G : Type u_6} [group G] (s : set α) (f : α → G) :
theorem set.indicator_compl {α : Type u_1} {G : Type u_2} [add_group G] (s : set α) (f : α → G) :
theorem set.mul_indicator_diff {α : Type u_1} {G : Type u_6} [group G] {s t : set α} (h : s t) (f : α → G) :
theorem set.indicator_diff' {α : Type u_1} {G : Type u_6} [add_group G] {s t : set α} (h : s t) (f : α → G) :
(t \ s).indicator f = t.indicator f + -s.indicator f
theorem set.indicator_diff {α : Type u_1} {G : Type u_2} [add_group G] {s t : set α} (h : s t) (f : α → G) :
(t \ s).indicator f = t.indicator f - s.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) :
s.sum (λ (i : α), g i (f i)) = t.sum (λ (i : α), 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 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) :
s.sum (λ (i : α), f i) = t.sum (λ (i : α), 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 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)] :
s.sum (λ (i : ι), (t i).indicator (f i) (g i)) = (finset.filter (λ (i : ι), g i t i) s).sum (λ (i : ι), f i (g 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.indicator_finset_sum {α : Type u_1} {ι : Type u_3} {M : Type u_4} [add_comm_monoid M] (I : finset ι) (s : set α) (f : ι → α → M) :
s.indicator (I.sum (λ (i : ι), f i)) = I.sum (λ (i : ι), s.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} :
(∀ (i : ι), i I∀ (j : ι), j Ii jdisjoint (s i) (s j))((⋃ (i : ι) (H : i I), s i).mul_indicator f = λ (a : α), I.prod (λ (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} :
(∀ (i : ι), i I∀ (j : ι), j Ii jdisjoint (s i) (s j))((⋃ (i : ι) (H : i I), s i).indicator f = λ (a : α), I.sum (λ (i : ι), (s i).indicator f a))
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 Ii jdisjoint (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_finset_bUnion_apply {α : Type u_1} {M : Type u_4} [add_comm_monoid M] {ι : Type u_2} (I : finset ι) (s : ι → set α) {f : α → M} (h : ∀ (i : ι), i I∀ (j : ι), j Ii jdisjoint (s i) (s j)) (x : α) :
(⋃ (i : ι) (H : i I), s i).indicator f x = I.sum (λ (i : ι), (s i).indicator f x)
theorem set.indicator_mul {α : Type u_1} {M : Type u_4} [mul_zero_class M] (s : set α) (f g : α → M) :
s.indicator (λ (a : α), f a * g a) = λ (a : α), s.indicator f a * s.indicator g a
theorem set.indicator_mul_left {α : Type u_1} {M : Type u_4} [mul_zero_class M] {a : α} (s : set α) (f g : α → M) :
s.indicator (λ (a : α), f a * g a) a = s.indicator f a * g a
theorem set.indicator_mul_right {α : Type u_1} {M : Type u_4} [mul_zero_class M] {a : α} (s : set α) (f g : α → M) :
s.indicator (λ (a : α), f a * g a) a = f a * s.indicator g a
theorem set.inter_indicator_mul {α : Type u_1} {M : Type u_4} [mul_zero_class M] {t1 t2 : set α} (f g : α → M) (x : α) :
(t1 t2).indicator (λ (x : α), f x * g x) x = t1.indicator f x * t2.indicator g x
theorem set.inter_indicator_one {α : Type u_1} {M : Type u_4} [mul_zero_one_class M] {s t : set α} :
theorem set.indicator_prod_one {α : Type u_1} {β : Type u_2} {M : Type u_4} [mul_zero_one_class M] {s : set α} {t : set β} {x : α} {y : β} :
(s ×ˢ t).indicator 1 (x, y) = s.indicator 1 x * t.indicator 1 y
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 : α} :
U.indicator 1 x = 0 x U
theorem set.indicator_eq_one_iff_mem {α : Type u_1} (M : Type u_4) [mul_zero_one_class M] [nontrivial M] {U : set α} {x : α} :
U.indicator 1 x = 1 x U
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.indicator_apply_le' {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f : α → M} {a : α} {y : M} [has_le M] (hfg : a sf a y) (hg : a s0 y) :
s.indicator f a y
theorem set.mul_indicator_apply_le' {α : Type u_1} {M : Type u_4} [has_one M] {s : set α} {f : α → M} {a : α} {y : M} [has_le M] (hfg : a sf a y) (hg : a s1 y) :
theorem set.indicator_le' {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f g : α → M} [has_le M] (hfg : ∀ (a : α), a sf a g a) (hg : ∀ (a : α), a s0 g a) :
theorem set.mul_indicator_le' {α : Type u_1} {M : Type u_4} [has_one M] {s : set α} {f g : α → M} [has_le M] (hfg : ∀ (a : α), a sf a g a) (hg : ∀ (a : α), a s1 g a) :
theorem set.le_indicator_apply {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {g : α → M} {a : α} [has_le M] {y : M} (hfg : a sy g a) (hf : a sy 0) :
y s.indicator g a
theorem set.le_mul_indicator_apply {α : Type u_1} {M : Type u_4} [has_one M] {s : set α} {g : α → M} {a : α} [has_le M] {y : M} (hfg : a sy g a) (hf : a sy 1) :
theorem set.le_mul_indicator {α : Type u_1} {M : Type u_4} [has_one M] {s : set α} {f g : α → M} [has_le M] (hfg : ∀ (a : α), a sf a g a) (hf : ∀ (a : α), a sf a 1) :
theorem set.le_indicator {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f g : α → M} [has_le M] (hfg : ∀ (a : α), a sf a g a) (hf : ∀ (a : α), a sf a 0) :
theorem set.indicator_apply_nonneg {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f : α → M} {a : α} [preorder M] (h : a s0 f a) :
0 s.indicator f a
theorem set.one_le_mul_indicator_apply {α : Type u_1} {M : Type u_4} [has_one M] {s : set α} {f : α → M} {a : α} [preorder M] (h : a s1 f a) :
theorem set.indicator_nonneg {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f : α → M} [preorder M] (h : ∀ (a : α), a s0 f a) (a : α) :
0 s.indicator f a
theorem set.one_le_mul_indicator {α : Type u_1} {M : Type u_4} [has_one M] {s : set α} {f : α → M} [preorder M] (h : ∀ (a : α), a s1 f a) (a : α) :
theorem set.mul_indicator_apply_le_one {α : Type u_1} {M : Type u_4} [has_one M] {s : set α} {f : α → M} {a : α} [preorder M] (h : a sf a 1) :
theorem set.indicator_apply_nonpos {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f : α → M} {a : α} [preorder M] (h : a sf a 0) :
s.indicator f a 0
theorem set.indicator_nonpos {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f : α → M} [preorder M] (h : ∀ (a : α), a sf a 0) (a : α) :
s.indicator f a 0
theorem set.mul_indicator_le_one {α : Type u_1} {M : Type u_4} [has_one M] {s : set α} {f : α → M} [preorder M] (h : ∀ (a : α), a sf a 1) (a : α) :
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) :
theorem set.indicator_le_indicator {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f g : α → M} {a : α} [preorder M] (h : f a g a) :
s.indicator f a s.indicator g a
theorem set.indicator_le_indicator_of_subset {α : Type u_1} {M : Type u_4} [has_zero M] {s t : set α} {f : α → M} [preorder M] (h : s t) (hf : ∀ (a : α), 0 f a) (a : α) :
s.indicator f a t.indicator f 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 : α) :
theorem set.mul_indicator_le_self' {α : Type u_1} {M : Type u_4} [has_one M] {s : set α} {f : α → M} [preorder M] (hf : ∀ (x : α), x s1 f x) :
theorem set.indicator_le_self' {α : Type u_1} {M : Type u_4} [has_zero M] {s : set α} {f : α → M} [preorder M] (hf : ∀ (x : α), x s0 f x) :
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 : α) :
(⋃ (i : ι), s i).indicator f x = ⨆ (i : ι), (s i).indicator f x
theorem set.mul_indicator_le_self {α : Type u_1} {M : Type u_4} [canonically_ordered_monoid M] (s : set α) (f : α → M) :
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 sf a g a) :
s.indicator 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 sf 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 sf 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 sf a g a) :
theorem set.indicator_le_indicator_nonneg {α : Type u_1} {β : Type u_2} [linear_order β] [has_zero β] (s : set α) (f : α → β) :
s.indicator f {x : α | 0 f x}.indicator f
theorem set.indicator_nonpos_le_indicator {α : Type u_1} {β : Type u_2} [linear_order β] [has_zero β] (s : set α) (f : α → β) :
{x : α | f x 0}.indicator f s.indicator f
theorem add_monoid_hom.map_indicator {α : Type u_1} {M : Type u_2} {N : Type u_3} [add_zero_class M] [add_zero_class N] (f : M →+ N) (s : set α) (g : α → M) (x : α) :
f (s.indicator g x) = s.indicator (f g) x
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 : α) :