# Indicator function #

In this file, we prove basic results about the indicator of a set.

- `Set.indicator (s : Set α) (f : α → β) (a : α)` is `f a` if `a ∈ s` and is `0` otherwise.
- `Set.mulIndicator (s : Set α) (f : α → β) (a : α)` is `f a` if `a ∈ s` and is `1` 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 `fun _ ↦ 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

source
theorem Set.mulIndicator_union_mul_inter_apply {α : Type u_1} {M : Type u_3} [MulOneClass M] (f : α → M) (s t : Set α) (a : α) :
(s ∪ t).mulIndicator f a * (s ∩ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
source
theorem Set.indicator_union_add_inter_apply {α : Type u_1} {M : Type u_3} [AddZeroClass 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
source
theorem Set.mulIndicator_union_mul_inter {α : Type u_1} {M : Type u_3} [MulOneClass M] (f : α → M) (s t : Set α) :
(s ∪ t).mulIndicator f * (s ∩ t).mulIndicator f = s.mulIndicator f * t.mulIndicator f
source
theorem Set.indicator_union_add_inter {α : Type u_1} {M : Type u_3} [AddZeroClass M] (f : α → M) (s t : Set α) :
(s ∪ t).indicator f + (s ∩ t).indicator f = s.indicator f + t.indicator f
source
theorem Set.mulIndicator_union_of_notMem_inter {α : Type u_1} {M : Type u_3} [MulOneClass M] {s t : Set α} {a : α} (h : a ∉ s ∩ t) (f : α → M) :
(s ∪ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
source
theorem Set.indicator_union_of_notMem_inter {α : Type u_1} {M : Type u_3} [AddZeroClass M] {s t : Set α} {a : α} (h : a ∉ s ∩ t) (f : α → M) :
(s ∪ t).indicator f a = s.indicator f a + t.indicator f a
source
@[deprecated Set.indicator_union_of_notMem_inter (since := "2025-05-23")]
theorem Set.indicator_union_of_not_mem_inter {α : Type u_1} {M : Type u_3} [AddZeroClass M] {s t : Set α} {a : α} (h : a ∉ s ∩ t) (f : α → M) :
(s ∪ t).indicator f a = s.indicator f a + t.indicator f a

Alias of `Set.indicator_union_of_notMem_inter`.

source
@[deprecated Set.mulIndicator_union_of_notMem_inter (since := "2025-05-23")]
theorem Set.mulIndicator_union_of_not_mem_inter {α : Type u_1} {M : Type u_3} [MulOneClass M] {s t : Set α} {a : α} (h : a ∉ s ∩ t) (f : α → M) :
(s ∪ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a

Alias of `Set.mulIndicator_union_of_notMem_inter`.

source
theorem Set.mulIndicator_union_of_disjoint {α : Type u_1} {M : Type u_3} [MulOneClass M] {s t : Set α} (h : Disjoint s t) (f : α → M) :
(s ∪ t).mulIndicator f = fun (a : α) => s.mulIndicator f a * t.mulIndicator f a
source
theorem Set.indicator_union_of_disjoint {α : Type u_1} {M : Type u_3} [AddZeroClass M] {s t : Set α} (h : Disjoint s t) (f : α → M) :
(s ∪ t).indicator f = fun (a : α) => s.indicator f a + t.indicator f a
source
theorem Set.mulIndicator_symmDiff {α : Type u_1} {M : Type u_3} [MulOneClass M] (s t : Set α) (f : α → M) :
(symmDiff s t).mulIndicator f = (s \ t).mulIndicator f * (t \ s).mulIndicator f
source
theorem Set.indicator_symmDiff {α : Type u_1} {M : Type u_3} [AddZeroClass M] (s t : Set α) (f : α → M) :
(symmDiff s t).indicator f = (s \ t).indicator f + (t \ s).indicator f
source
theorem Set.mulIndicator_mul {α : Type u_1} {M : Type u_3} [MulOneClass M] (s : Set α) (f g : α → M) :
(s.mulIndicator fun (a : α) => f a * g a) = fun (a : α) => s.mulIndicator f a * s.mulIndicator g a
source
theorem Set.indicator_add {α : Type u_1} {M : Type u_3} [AddZeroClass M] (s : Set α) (f g : α → M) :
(s.indicator fun (a : α) => f a + g a) = fun (a : α) => s.indicator f a + s.indicator g a
source
theorem Set.mulIndicator_mul' {α : Type u_1} {M : Type u_3} [MulOneClass M] (s : Set α) (f g : α → M) :
s.mulIndicator (f * g) = s.mulIndicator f * s.mulIndicator g
source
theorem Set.indicator_add' {α : Type u_1} {M : Type u_3} [AddZeroClass M] (s : Set α) (f g : α → M) :
s.indicator (f + g) = s.indicator f + s.indicator g
source
@[simp]
theorem Set.mulIndicator_compl_mul_self_apply {α : Type u_1} {M : Type u_3} [MulOneClass M] (s : Set α) (f : α → M) (a : α) :
s ᶜ.mulIndicator f a * s.mulIndicator f a = f a
source
@[simp]
theorem Set.indicator_compl_add_self_apply {α : Type u_1} {M : Type u_3} [AddZeroClass M] (s : Set α) (f : α → M) (a : α) :
s ᶜ.indicator f a + s.indicator f a = f a
source
@[simp]
theorem Set.mulIndicator_compl_mul_self {α : Type u_1} {M : Type u_3} [MulOneClass M] (s : Set α) (f : α → M) :
s ᶜ.mulIndicator f * s.mulIndicator f = f
source
@[simp]
theorem Set.indicator_compl_add_self {α : Type u_1} {M : Type u_3} [AddZeroClass M] (s : Set α) (f : α → M) :
s ᶜ.indicator f + s.indicator f = f
source
@[simp]
theorem Set.mulIndicator_self_mul_compl_apply {α : Type u_1} {M : Type u_3} [MulOneClass M] (s : Set α) (f : α → M) (a : α) :
s.mulIndicator f a * s ᶜ.mulIndicator f a = f a
source
@[simp]
theorem Set.indicator_self_add_compl_apply {α : Type u_1} {M : Type u_3} [AddZeroClass M] (s : Set α) (f : α → M) (a : α) :
s.indicator f a + s ᶜ.indicator f a = f a
source
@[simp]
theorem Set.mulIndicator_self_mul_compl {α : Type u_1} {M : Type u_3} [MulOneClass M] (s : Set α) (f : α → M) :
s.mulIndicator f * s ᶜ.mulIndicator f = f
source
@[simp]
theorem Set.indicator_self_add_compl {α : Type u_1} {M : Type u_3} [AddZeroClass M] (s : Set α) (f : α → M) :
s.indicator f + s ᶜ.indicator f = f
source
theorem Set.mulIndicator_mul_eq_left {α : Type u_1} {M : Type u_3} [MulOneClass M] {f g : α → M} (h : Disjoint (Function.mulSupport f) (Function.mulSupport g)) :
(Function.mulSupport f).mulIndicator (f * g) = f
source
theorem Set.indicator_add_eq_left {α : Type u_1} {M : Type u_3} [AddZeroClass M] {f g : α → M} (h : Disjoint (Function.support f) (Function.support g)) :
(Function.support f).indicator (f + g) = f
source
theorem Set.mulIndicator_mul_eq_right {α : Type u_1} {M : Type u_3} [MulOneClass M] {f g : α → M} (h : Disjoint (Function.mulSupport f) (Function.mulSupport g)) :
(Function.mulSupport g).mulIndicator (f * g) = g
source
theorem Set.indicator_add_eq_right {α : Type u_1} {M : Type u_3} [AddZeroClass M] {f g : α → M} (h : Disjoint (Function.support f) (Function.support g)) :
(Function.support g).indicator (f + g) = g
source
theorem Set.mulIndicator_mul_compl_eq_piecewise {α : Type u_1} {M : Type u_3} [MulOneClass M] {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (f g : α → M) :
s.mulIndicator f * s ᶜ.mulIndicator g = s.piecewise f g
source
theorem Set.indicator_add_compl_eq_piecewise {α : Type u_1} {M : Type u_3} [AddZeroClass M] {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (f g : α → M) :
s.indicator f + s ᶜ.indicator g = s.piecewise f g
source
noncomputable def Set.mulIndicatorHom {α : Type u_5} (M : Type u_6) [MulOneClass M] (s : Set α) :
(α → M) →* α → M

`Set.mulIndicator` as a `monoidHom`.

Equations

- Set.mulIndicatorHom M s = { toFun := s.mulIndicator, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
noncomputable def Set.indicatorHom {α : Type u_5} (M : Type u_6) [AddZeroClass M] (s : Set α) :
(α → M) →+ α → M

`Set.indicator` as an `addMonoidHom`.

Equations

- Set.indicatorHom M s = { toFun := s.indicator, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
theorem Set.mulIndicator_inv' {α : Type u_1} {G : Type u_5} [Group G] (s : Set α) (f : α → G) :
s.mulIndicator f⁻¹ = (s.mulIndicator f)⁻¹
source
theorem Set.indicator_neg' {α : Type u_1} {G : Type u_5} [AddGroup G] (s : Set α) (f : α → G) :
s.indicator (-f) = -s.indicator f
source
theorem Set.mulIndicator_inv {α : Type u_1} {G : Type u_5} [Group G] (s : Set α) (f : α → G) :
(s.mulIndicator fun (a : α) => (f a)⁻¹) = fun (a : α) => (s.mulIndicator f a)⁻¹
source
theorem Set.indicator_neg {α : Type u_1} {G : Type u_5} [AddGroup G] (s : Set α) (f : α → G) :
(s.indicator fun (a : α) => -f a) = fun (a : α) => -s.indicator f a
source
theorem Set.mulIndicator_div {α : Type u_1} {G : Type u_5} [Group G] (s : Set α) (f g : α → G) :
(s.mulIndicator fun (a : α) => f a / g a) = fun (a : α) => s.mulIndicator f a / s.mulIndicator g a
source
theorem Set.indicator_sub {α : Type u_1} {G : Type u_5} [AddGroup G] (s : Set α) (f g : α → G) :
(s.indicator fun (a : α) => f a - g a) = fun (a : α) => s.indicator f a - s.indicator g a
source
theorem Set.mulIndicator_div' {α : Type u_1} {G : Type u_5} [Group G] (s : Set α) (f g : α → G) :
s.mulIndicator (f / g) = s.mulIndicator f / s.mulIndicator g
source
theorem Set.indicator_sub' {α : Type u_1} {G : Type u_5} [AddGroup G] (s : Set α) (f g : α → G) :
s.indicator (f - g) = s.indicator f - s.indicator g
source
theorem Set.mulIndicator_compl {α : Type u_1} {G : Type u_5} [Group G] (s : Set α) (f : α → G) :
s ᶜ.mulIndicator f = f * (s.mulIndicator f)⁻¹
source
theorem Set.indicator_compl' {α : Type u_1} {G : Type u_5} [AddGroup G] (s : Set α) (f : α → G) :
s ᶜ.indicator f = f + -s.indicator f
source
theorem Set.mulIndicator_compl' {α : Type u_1} {G : Type u_5} [Group G] (s : Set α) (f : α → G) :
s ᶜ.mulIndicator f = f / s.mulIndicator f
source
theorem Set.indicator_compl {α : Type u_1} {G : Type u_5} [AddGroup G] (s : Set α) (f : α → G) :
s ᶜ.indicator f = f - s.indicator f
source
theorem Set.mulIndicator_diff {α : Type u_1} {G : Type u_5} [Group G] {s t : Set α} (h : s ⊆ t) (f : α → G) :
(t \ s).mulIndicator f = t.mulIndicator f * (s.mulIndicator f)⁻¹
source
theorem Set.indicator_diff' {α : Type u_1} {G : Type u_5} [AddGroup G] {s t : Set α} (h : s ⊆ t) (f : α → G) :
(t \ s).indicator f = t.indicator f + -s.indicator f
source
theorem Set.mulIndicator_diff' {α : Type u_1} {G : Type u_5} [Group G] {s t : Set α} (h : s ⊆ t) (f : α → G) :
(t \ s).mulIndicator f = t.mulIndicator f / s.mulIndicator f
source
theorem Set.indicator_diff {α : Type u_1} {G : Type u_5} [AddGroup G] {s t : Set α} (h : s ⊆ t) (f : α → G) :
(t \ s).indicator f = t.indicator f - s.indicator f
source
theorem Set.apply_mulIndicator_symmDiff {α : Type u_1} {β : Type u_2} {G : Type u_5} [Group G] {g : G → β} (hg : ∀ (x : G), g x⁻¹ = g x) (s t : Set α) (f : α → G) (x : α) :
g ((symmDiff s t).mulIndicator f x) = g (s.mulIndicator f x / t.mulIndicator f x)
source
theorem Set.apply_indicator_symmDiff {α : Type u_1} {β : Type u_2} {G : Type u_5} [AddGroup G] {g : G → β} (hg : ∀ (x : G), g (-x) = g x) (s t : Set α) (f : α → G) (x : α) :
g ((symmDiff s t).indicator f x) = g (s.indicator f x - t.indicator f x)
source
theorem MonoidHom.map_mulIndicator {α : Type u_1} {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] (f : M →* N) (s : Set α) (g : α → M) (x : α) :
f (s.mulIndicator g x) = s.mulIndicator (⇑f ∘ g) x
source
theorem AddMonoidHom.map_indicator {α : Type u_1} {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (s : Set α) (g : α → M) (x : α) :
f (s.indicator g x) = s.indicator (⇑f ∘ g) x