Documentation

Mathlib.Algebra.IndicatorFunction

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} [inst : Zero M] (s : Set α) (f : αM) :
αM

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

Equations
noncomputable def Set.mulIndicator {α : Type u_1} {M : Type u_2} [inst : One M] (s : Set α) (f : αM) :
αM

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

Equations
@[simp]
theorem Set.piecewise_eq_indicator {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} [inst : DecidablePred fun x => x s] :
@[simp]
theorem Set.piecewise_eq_mulIndicator {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} [inst : DecidablePred fun x => x s] :
theorem Set.indicator_apply {α : Type u_1} {M : Type u_2} [inst : Zero M] (s : Set α) (f : αM) (a : α) [inst : Decidable (a s)] :
Set.indicator s f a = if a s then f a else 0
theorem Set.mulIndicator_apply {α : Type u_1} {M : Type u_2} [inst : One M] (s : Set α) (f : αM) (a : α) [inst : Decidable (a s)] :
Set.mulIndicator s f a = if a s then f a else 1
@[simp]
theorem Set.indicator_of_mem {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {a : α} (h : a s) (f : αM) :
Set.indicator s f a = f a
@[simp]
theorem Set.mulIndicator_of_mem {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {a : α} (h : a s) (f : αM) :
@[simp]
theorem Set.indicator_of_not_mem {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {a : α} (h : ¬a s) (f : αM) :
@[simp]
theorem Set.mulIndicator_of_not_mem {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {a : α} (h : ¬a s) (f : αM) :
theorem Set.indicator_eq_zero_or_self {α : Type u_1} {M : Type u_2} [inst : Zero M] (s : Set α) (f : αM) (a : α) :
Set.indicator s f a = 0 Set.indicator s f a = f a
theorem Set.mulIndicator_eq_one_or_self {α : Type u_1} {M : Type u_2} [inst : One M] (s : Set α) (f : αM) (a : α) :
@[simp]
theorem Set.indicator_apply_eq_self {α : Type u_2} {M : Type u_1} [inst : Zero M] {s : Set α} {f : αM} {a : α} :
Set.indicator s f a = f a ¬a sf a = 0
@[simp]
theorem Set.mulIndicator_apply_eq_self {α : Type u_2} {M : Type u_1} [inst : One M] {s : Set α} {f : αM} {a : α} :
Set.mulIndicator s f a = f a ¬a sf a = 1
@[simp]
theorem Set.indicator_eq_self {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} :
@[simp]
theorem Set.mulIndicator_eq_self {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} :
theorem Set.indicator_eq_self_of_superset {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {t : Set α} {f : αM} (h1 : Set.indicator s f = f) (h2 : s t) :
theorem Set.mulIndicator_eq_self_of_superset {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {t : Set α} {f : αM} (h1 : Set.mulIndicator s f = f) (h2 : s t) :
@[simp]
theorem Set.indicator_apply_eq_zero {α : Type u_2} {M : Type u_1} [inst : Zero M] {s : Set α} {f : αM} {a : α} :
Set.indicator s f a = 0 a sf a = 0
@[simp]
theorem Set.mulIndicator_apply_eq_one {α : Type u_2} {M : Type u_1} [inst : One M] {s : Set α} {f : αM} {a : α} :
Set.mulIndicator s f a = 1 a sf a = 1
@[simp]
theorem Set.indicator_eq_zero {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} :
@[simp]
theorem Set.mulIndicator_eq_one {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} :
@[simp]
theorem Set.indicator_eq_zero' {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} :
@[simp]
theorem Set.mulIndicator_eq_one' {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} :
theorem Set.indicator_apply_ne_zero {α : Type u_2} {M : Type u_1} [inst : Zero M] {s : Set α} {f : αM} {a : α} :
theorem Set.mulIndicator_apply_ne_one {α : Type u_2} {M : Type u_1} [inst : One M] {s : Set α} {f : αM} {a : α} :
@[simp]
theorem Set.support_indicator {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} :
@[simp]
theorem Set.mulSupport_mulIndicator {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} :
theorem Set.mem_of_indicator_ne_zero {α : Type u_2} {M : Type u_1} [inst : Zero M] {s : Set α} {f : αM} {a : α} (h : Set.indicator s 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_mulIndicator_ne_one {α : Type u_2} {M : Type u_1} [inst : One M] {s : Set α} {f : αM} {a : α} (h : Set.mulIndicator s 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.eqOn_indicator {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} :
theorem Set.eqOn_mulIndicator {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} :
theorem Set.support_indicator_subset {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} :
theorem Set.mulSupport_mulIndicator_subset {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} :
@[simp]
theorem Set.indicator_support {α : Type u_1} {M : Type u_2} [inst : Zero M] {f : αM} :
@[simp]
theorem Set.mulIndicator_mulSupport {α : Type u_1} {M : Type u_2} [inst : One M] {f : αM} :
@[simp]
theorem Set.indicator_range_comp {α : Type u_3} {M : Type u_2} [inst : Zero M] {ι : Sort u_1} (f : ια) (g : αM) :
@[simp]
theorem Set.mulIndicator_range_comp {α : Type u_3} {M : Type u_2} [inst : One M] {ι : Sort u_1} (f : ια) (g : αM) :
theorem Set.indicator_congr {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} {g : αM} (h : Set.EqOn f g s) :
theorem Set.mulIndicator_congr {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} {g : αM} (h : Set.EqOn f g s) :
@[simp]
theorem Set.indicator_univ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : αM) :
Set.indicator Set.univ f = f
@[simp]
theorem Set.mulIndicator_univ {α : Type u_1} {M : Type u_2} [inst : One M] (f : αM) :
Set.mulIndicator Set.univ f = f
@[simp]
theorem Set.indicator_empty {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : αM) :
Set.indicator f = fun x => 0
@[simp]
theorem Set.mulIndicator_empty {α : Type u_1} {M : Type u_2} [inst : One M] (f : αM) :
Set.mulIndicator f = fun x => 1
theorem Set.indicator_empty' {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : αM) :
theorem Set.mulIndicator_empty' {α : Type u_1} {M : Type u_2} [inst : One M] (f : αM) :
@[simp]
theorem Set.indicator_zero {α : Type u_1} (M : Type u_2) [inst : Zero M] (s : Set α) :
(Set.indicator s fun x => 0) = fun x => 0
@[simp]
theorem Set.mulIndicator_one {α : Type u_1} (M : Type u_2) [inst : One M] (s : Set α) :
(Set.mulIndicator s fun x => 1) = fun x => 1
@[simp]
theorem Set.indicator_zero' {α : Type u_1} (M : Type u_2) [inst : Zero M] {s : Set α} :
@[simp]
theorem Set.mulIndicator_one' {α : Type u_1} (M : Type u_2) [inst : One M] {s : Set α} :
theorem Set.indicator_indicator {α : Type u_1} {M : Type u_2} [inst : Zero M] (s : Set α) (t : Set α) (f : αM) :
theorem Set.mulIndicator_mulIndicator {α : Type u_1} {M : Type u_2} [inst : One M] (s : Set α) (t : Set α) (f : αM) :
@[simp]
theorem Set.indicator_inter_support {α : Type u_1} {M : Type u_2} [inst : Zero M] (s : Set α) (f : αM) :
@[simp]
theorem Set.mulIndicator_inter_mulSupport {α : Type u_1} {M : Type u_2} [inst : One M] (s : Set α) (f : αM) :
theorem Set.comp_indicator {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] (h : Mβ) (f : αM) {s : Set α} {x : α} [inst : DecidablePred fun x => x s] :
h (Set.indicator s f x) = Set.piecewise s (h f) (Function.const α (h 0)) x
theorem Set.comp_mulIndicator {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : One M] (h : Mβ) (f : αM) {s : Set α} {x : α} [inst : DecidablePred fun x => x s] :
h (Set.mulIndicator s f x) = Set.piecewise s (h f) (Function.const α (h 1)) x
theorem Set.indicator_comp_right {α : Type u_1} {β : Type u_3} {M : Type u_2} [inst : Zero M] {s : Set α} (f : βα) {g : αM} {x : β} :
Set.indicator (f ⁻¹' s) (g f) x = Set.indicator s g (f x)
theorem Set.mulIndicator_comp_right {α : Type u_1} {β : Type u_3} {M : Type u_2} [inst : One M] {s : Set α} (f : βα) {g : αM} {x : β} :
Set.mulIndicator (f ⁻¹' s) (g f) x = Set.mulIndicator s g (f x)
theorem Set.indicator_image {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] {s : Set α} {f : βM} {g : αβ} (hg : Function.Injective g) {x : α} :
Set.indicator (g '' s) f (g x) = Set.indicator s (f g) x
theorem Set.mulIndicator_image {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : One M] {s : Set α} {f : βM} {g : αβ} (hg : Function.Injective g) {x : α} :
Set.mulIndicator (g '' s) f (g x) = Set.mulIndicator s (f g) x
theorem Set.indicator_comp_of_zero {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : Zero M] [inst : Zero N] {s : Set α} {f : αM} {g : MN} (hg : g 0 = 0) :
theorem Set.mulIndicator_comp_of_one {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : One M] [inst : One N] {s : Set α} {f : αM} {g : MN} (hg : g 1 = 1) :
theorem Set.comp_indicator_const {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : Zero M] [inst : Zero N] {s : Set α} (c : M) (f : MN) (hf : f 0 = 0) :
(fun x => f (Set.indicator s (fun x => c) x)) = Set.indicator s fun x => f c
theorem Set.comp_mulIndicator_const {α : Type u_3} {M : Type u_2} {N : Type u_1} [inst : One M] [inst : One N] {s : Set α} (c : M) (f : MN) (hf : f 1 = 1) :
(fun x => f (Set.mulIndicator s (fun x => c) x)) = Set.mulIndicator s fun x => f c
theorem Set.indicator_preimage {α : Type u_1} {M : Type u_2} [inst : Zero M] (s : Set α) (f : αM) (B : Set M) :
theorem Set.mulIndicator_preimage {α : Type u_1} {M : Type u_2} [inst : One M] (s : Set α) (f : αM) (B : Set M) :
theorem Set.indicator_zero_preimage {α : Type u_2} {M : Type u_1} [inst : Zero M] {t : Set α} (s : Set M) :
Set.indicator t 0 ⁻¹' s {Set.univ, }
theorem Set.mulIndicator_one_preimage {α : Type u_2} {M : Type u_1} [inst : One M] {t : Set α} (s : Set M) :
Set.mulIndicator t 1 ⁻¹' s {Set.univ, }
theorem Set.indicator_const_preimage_eq_union {α : Type u_1} {M : Type u_2} [inst : Zero M] (U : Set α) (s : Set M) (a : M) [inst : Decidable (a s)] [inst : Decidable (0 s)] :
(Set.indicator U fun x => a) ⁻¹' s = (if a s then U else ) if 0 s then U else
theorem Set.mulIndicator_const_preimage_eq_union {α : Type u_1} {M : Type u_2} [inst : One M] (U : Set α) (s : Set M) (a : M) [inst : Decidable (a s)] [inst : Decidable (1 s)] :
(Set.mulIndicator U fun x => a) ⁻¹' s = (if a s then U else ) if 1 s then U else
theorem Set.indicator_const_preimage {α : Type u_1} {M : Type u_2} [inst : Zero M] (U : Set α) (s : Set M) (a : M) :
(Set.indicator U fun x => a) ⁻¹' s {Set.univ, U, U, }
theorem Set.mulIndicator_const_preimage {α : Type u_1} {M : Type u_2} [inst : One M] (U : Set α) (s : Set M) (a : M) :
(Set.mulIndicator U fun x => a) ⁻¹' s {Set.univ, U, U, }
theorem Set.indicator_one_preimage {α : Type u_2} {M : Type u_1} [inst : One M] [inst : Zero M] (U : Set α) (s : Set M) :
Set.indicator U 1 ⁻¹' s {Set.univ, U, U, }
theorem Set.indicator_preimage_of_not_mem {α : Type u_1} {M : Type u_2} [inst : Zero M] (s : Set α) (f : αM) {t : Set M} (ht : ¬0 t) :
theorem Set.mulIndicator_preimage_of_not_mem {α : Type u_1} {M : Type u_2} [inst : One M] (s : Set α) (f : αM) {t : Set M} (ht : ¬1 t) :
theorem Set.mem_range_indicator {α : Type u_1} {M : Type u_2} [inst : Zero M] {r : M} {s : Set α} {f : αM} :
r Set.range (Set.indicator s f) r = 0 s Set.univ r f '' s
theorem Set.mem_range_mulIndicator {α : Type u_1} {M : Type u_2} [inst : One M] {r : M} {s : Set α} {f : αM} :
r Set.range (Set.mulIndicator s f) r = 1 s Set.univ r f '' s
theorem Set.indicator_rel_indicator {α : Type u_2} {M : Type u_1} [inst : Zero M] {s : Set α} {f : αM} {g : αM} {a : α} {r : MMProp} (h1 : r 0 0) (ha : a sr (f a) (g a)) :
r (Set.indicator s f a) (Set.indicator s g a)
theorem Set.mulIndicator_rel_mulIndicator {α : Type u_2} {M : Type u_1} [inst : One M] {s : Set α} {f : αM} {g : αM} {a : α} {r : MMProp} (h1 : r 1 1) (ha : a sr (f a) (g a)) :
theorem Set.indicator_union_add_inter_apply {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (f : αM) (s : Set α) (t : Set α) (a : α) :
theorem Set.mulIndicator_union_mul_inter_apply {α : Type u_1} {M : Type u_2} [inst : MulOneClass M] (f : αM) (s : Set α) (t : Set α) (a : α) :
theorem Set.indicator_union_add_inter {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (f : αM) (s : Set α) (t : Set α) :
theorem Set.mulIndicator_union_mul_inter {α : Type u_1} {M : Type u_2} [inst : MulOneClass M] (f : αM) (s : Set α) (t : Set α) :
theorem Set.indicator_union_of_not_mem_inter {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] {s : Set α} {t : Set α} {a : α} (h : ¬a s t) (f : αM) :
theorem Set.mulIndicator_union_of_not_mem_inter {α : Type u_1} {M : Type u_2} [inst : MulOneClass M] {s : Set α} {t : Set α} {a : α} (h : ¬a s t) (f : αM) :
theorem Set.indicator_union_of_disjoint {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] {s : Set α} {t : Set α} (h : Disjoint s t) (f : αM) :
Set.indicator (s t) f = fun a => Set.indicator s f a + Set.indicator t f a
theorem Set.mulIndicator_union_of_disjoint {α : Type u_1} {M : Type u_2} [inst : MulOneClass M] {s : Set α} {t : Set α} (h : Disjoint s t) (f : αM) :
theorem Set.indicator_add {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (s : Set α) (f : αM) (g : αM) :
(Set.indicator s fun a => f a + g a) = fun a => Set.indicator s f a + Set.indicator s g a
theorem Set.mulIndicator_mul {α : Type u_1} {M : Type u_2} [inst : MulOneClass M] (s : Set α) (f : αM) (g : αM) :
(Set.mulIndicator s fun a => f a * g a) = fun a => Set.mulIndicator s f a * Set.mulIndicator s g a
theorem Set.indicator_add' {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (s : Set α) (f : αM) (g : αM) :
theorem Set.mulIndicator_mul' {α : Type u_1} {M : Type u_2} [inst : MulOneClass M] (s : Set α) (f : αM) (g : αM) :
@[simp]
theorem Set.indicator_compl_add_self_apply {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (s : Set α) (f : αM) (a : α) :
Set.indicator (s) f a + Set.indicator s f a = f a
@[simp]
theorem Set.mulIndicator_compl_mul_self_apply {α : Type u_1} {M : Type u_2} [inst : MulOneClass M] (s : Set α) (f : αM) (a : α) :
@[simp]
theorem Set.indicator_compl_add_self {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (s : Set α) (f : αM) :
@[simp]
theorem Set.mulIndicator_compl_mul_self {α : Type u_1} {M : Type u_2} [inst : MulOneClass M] (s : Set α) (f : αM) :
@[simp]
theorem Set.indicator_self_add_compl_apply {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (s : Set α) (f : αM) (a : α) :
Set.indicator s f a + Set.indicator (s) f a = f a
@[simp]
theorem Set.mulIndicator_self_mul_compl_apply {α : Type u_1} {M : Type u_2} [inst : MulOneClass M] (s : Set α) (f : αM) (a : α) :
@[simp]
theorem Set.indicator_self_add_compl {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] (s : Set α) (f : αM) :
@[simp]
theorem Set.mulIndicator_self_mul_compl {α : Type u_1} {M : Type u_2} [inst : MulOneClass M] (s : Set α) (f : αM) :
theorem Set.indicator_add_eq_left {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] {f : αM} {g : αM} (h : Disjoint (Function.support f) (Function.support g)) :
theorem Set.mulIndicator_mul_eq_left {α : Type u_1} {M : Type u_2} [inst : MulOneClass M] {f : αM} {g : αM} (h : Disjoint (Function.mulSupport f) (Function.mulSupport g)) :
theorem Set.indicator_add_eq_right {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] {f : αM} {g : αM} (h : Disjoint (Function.support f) (Function.support g)) :
theorem Set.mulIndicator_mul_eq_right {α : Type u_1} {M : Type u_2} [inst : MulOneClass M] {f : αM} {g : αM} (h : Disjoint (Function.mulSupport f) (Function.mulSupport g)) :
theorem Set.indicator_add_compl_eq_piecewise {α : Type u_1} {M : Type u_2} [inst : AddZeroClass M] {s : Set α} [inst : DecidablePred fun x => x s] (f : αM) (g : αM) :
theorem Set.mulIndicator_mul_compl_eq_piecewise {α : Type u_1} {M : Type u_2} [inst : MulOneClass M] {s : Set α} [inst : DecidablePred fun x => x s] (f : αM) (g : αM) :
def Set.indicatorHom.proof_1 {α : Type u_1} (M : Type u_2) [inst : AddZeroClass M] (s : Set α) :
(Set.indicator s fun x => 0) = fun x => 0
Equations
noncomputable def Set.indicatorHom {α : Type u_1} (M : Type u_2) [inst : AddZeroClass M] (s : Set α) :
(αM) →+ αM

Set.indicator as an addMonoidHom.

Equations
  • One or more equations did not get rendered due to their size.
noncomputable def Set.mulIndicatorHom {α : Type u_1} (M : Type u_2) [inst : MulOneClass M] (s : Set α) :
(αM) →* αM

Set.mulIndicator as a monoidHom.

Equations
  • One or more equations did not get rendered due to their size.
theorem Set.indicator_smul_apply {α : Type u_1} {M : Type u_3} {A : Type u_2} [inst : AddMonoid A] [inst : Monoid M] [inst : DistribMulAction M A] (s : Set α) (r : αM) (f : αA) (x : α) :
Set.indicator s (fun x => r x f x) x = r x Set.indicator s f x
theorem Set.indicator_smul {α : Type u_1} {M : Type u_3} {A : Type u_2} [inst : AddMonoid A] [inst : Monoid M] [inst : DistribMulAction M A] (s : Set α) (r : αM) (f : αA) :
(Set.indicator s fun x => r x f x) = fun x => r x Set.indicator s f x
theorem Set.indicator_const_smul_apply {α : Type u_1} {M : Type u_3} {A : Type u_2} [inst : AddMonoid A] [inst : Monoid M] [inst : DistribMulAction M A] (s : Set α) (r : M) (f : αA) (x : α) :
Set.indicator s (fun x => r f x) x = r Set.indicator s f x
theorem Set.indicator_const_smul {α : Type u_1} {M : Type u_3} {A : Type u_2} [inst : AddMonoid A] [inst : Monoid M] [inst : DistribMulAction M A] (s : Set α) (r : M) (f : αA) :
(Set.indicator s fun x => r f x) = fun x => r Set.indicator s f x
theorem Set.indicator_neg' {α : Type u_1} {G : Type u_2} [inst : AddGroup G] (s : Set α) (f : αG) :
theorem Set.mulIndicator_inv' {α : Type u_1} {G : Type u_2} [inst : Group G] (s : Set α) (f : αG) :
theorem Set.indicator_neg {α : Type u_1} {G : Type u_2} [inst : AddGroup G] (s : Set α) (f : αG) :
(Set.indicator s fun a => -f a) = fun a => -Set.indicator s f a
theorem Set.mulIndicator_inv {α : Type u_1} {G : Type u_2} [inst : Group G] (s : Set α) (f : αG) :
(Set.mulIndicator s fun a => (f a)⁻¹) = fun a => (Set.mulIndicator s f a)⁻¹
theorem Set.indicator_sub {α : Type u_1} {G : Type u_2} [inst : AddGroup G] (s : Set α) (f : αG) (g : αG) :
(Set.indicator s fun a => f a - g a) = fun a => Set.indicator s f a - Set.indicator s g a
theorem Set.mulIndicator_div {α : Type u_1} {G : Type u_2} [inst : Group G] (s : Set α) (f : αG) (g : αG) :
(Set.mulIndicator s fun a => f a / g a) = fun a => Set.mulIndicator s f a / Set.mulIndicator s g a
theorem Set.indicator_sub' {α : Type u_1} {G : Type u_2} [inst : AddGroup G] (s : Set α) (f : αG) (g : αG) :
theorem Set.mulIndicator_div' {α : Type u_1} {G : Type u_2} [inst : Group G] (s : Set α) (f : αG) (g : αG) :
theorem Set.indicator_compl' {α : Type u_1} {G : Type u_2} [inst : AddGroup G] (s : Set α) (f : αG) :
theorem Set.mulIndicator_compl {α : Type u_1} {G : Type u_2} [inst : Group G] (s : Set α) (f : αG) :
theorem Set.indicator_compl {α : Type u_2} {G : Type u_1} [inst : AddGroup G] (s : Set α) (f : αG) :
theorem Set.indicator_diff' {α : Type u_1} {G : Type u_2} [inst : AddGroup G] {s : Set α} {t : Set α} (h : s t) (f : αG) :
theorem Set.mulIndicator_diff {α : Type u_1} {G : Type u_2} [inst : Group G] {s : Set α} {t : Set α} (h : s t) (f : αG) :
theorem Set.indicator_diff {α : Type u_2} {G : Type u_1} [inst : AddGroup G] {s : Set α} {t : Set α} (h : s t) (f : αG) :
theorem Set.sum_indicator_subset_of_eq_zero {α : Type u_2} {M : Type u_3} {N : Type u_1} [inst : AddCommMonoid M] [inst : Zero N] (f : αN) (g : αNM) {s : Finset α} {t : Finset α} (h : s t) (hg : ∀ (a : α), g a 0 = 0) :
(Finset.sum s fun i => g i (f i)) = Finset.sum t fun i => g i (Set.indicator (s) 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_mulIndicator_subset_of_eq_one {α : Type u_2} {M : Type u_3} {N : Type u_1} [inst : CommMonoid M] [inst : One N] (f : αN) (g : αNM) {s : Finset α} {t : Finset α} (h : s t) (hg : ∀ (a : α), g a 1 = 1) :
(Finset.prod s fun i => g i (f i)) = Finset.prod t fun i => g i (Set.mulIndicator (s) 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 {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (f : αM) {s : Finset α} {t : Finset α} (h : s t) :
(Finset.sum s fun i => f i) = Finset.sum t fun i => Set.indicator (s) 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.prod_mulIndicator_subset {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] (f : αM) {s : Finset α} {t : Finset α} (h : s t) :
(Finset.prod s fun i => f i) = Finset.prod t fun i => Set.mulIndicator (s) 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 Finset.sum_indicator_eq_sum_filter {α : Type u_2} {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (s : Finset ι) (f : ιαM) (t : ιSet α) (g : ια) [inst : DecidablePred fun i => g i t i] :
(Finset.sum s fun i => Set.indicator (t i) (f i) (g i)) = Finset.sum (Finset.filter (fun i => g i t i) s) fun i => f i (g i)
theorem Finset.prod_mulIndicator_eq_prod_filter {α : Type u_2} {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (s : Finset ι) (f : ιαM) (t : ιSet α) (g : ια) [inst : DecidablePred fun i => g i t i] :
(Finset.prod s fun i => Set.mulIndicator (t i) (f i) (g i)) = Finset.prod (Finset.filter (fun i => g i t i) s) fun i => f i (g i)
theorem Set.indicator_finset_sum {α : Type u_2} {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (I : Finset ι) (s : Set α) (f : ιαM) :
Set.indicator s (Finset.sum I fun i => f i) = Finset.sum I fun i => Set.indicator s (f i)
theorem Set.mulIndicator_finset_prod {α : Type u_2} {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (I : Finset ι) (s : Set α) (f : ιαM) :
Set.mulIndicator s (Finset.prod I fun i => f i) = Finset.prod I fun i => Set.mulIndicator s (f i)
theorem Set.indicator_finset_bunionᵢ {α : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] {ι : Type u_1} (I : Finset ι) (s : ιSet α) {f : αM} :
(∀ (i : ι), i I∀ (j : ι), j Ii jDisjoint (s i) (s j)) → Set.indicator (Set.unionᵢ fun i => Set.unionᵢ fun h => s i) f = fun a => Finset.sum I fun i => Set.indicator (s i) f a
theorem Set.mulIndicator_finset_bunionᵢ {α : Type u_2} {M : Type u_3} [inst : CommMonoid M] {ι : Type u_1} (I : Finset ι) (s : ιSet α) {f : αM} :
(∀ (i : ι), i I∀ (j : ι), j Ii jDisjoint (s i) (s j)) → Set.mulIndicator (Set.unionᵢ fun i => Set.unionᵢ fun h => s i) f = fun a => Finset.prod I fun i => Set.mulIndicator (s i) f a
theorem Set.indicator_finset_bunionᵢ_apply {α : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] {ι : Type u_1} (I : Finset ι) (s : ιSet α) {f : αM} (h : ∀ (i : ι), i I∀ (j : ι), j Ii jDisjoint (s i) (s j)) (x : α) :
Set.indicator (Set.unionᵢ fun i => Set.unionᵢ fun h => s i) f x = Finset.sum I fun i => Set.indicator (s i) f x
theorem Set.mulIndicator_finset_bunionᵢ_apply {α : Type u_2} {M : Type u_3} [inst : CommMonoid M] {ι : Type u_1} (I : Finset ι) (s : ιSet α) {f : αM} (h : ∀ (i : ι), i I∀ (j : ι), j Ii jDisjoint (s i) (s j)) (x : α) :
Set.mulIndicator (Set.unionᵢ fun i => Set.unionᵢ fun h => s i) f x = Finset.prod I fun i => Set.mulIndicator (s i) f x
theorem Set.indicator_mul {α : Type u_1} {M : Type u_2} [inst : MulZeroClass M] (s : Set α) (f : αM) (g : αM) :
(Set.indicator s fun a => f a * g a) = fun a => Set.indicator s f a * Set.indicator s g a
theorem Set.indicator_mul_left {α : Type u_1} {M : Type u_2} [inst : MulZeroClass M] {a : α} (s : Set α) (f : αM) (g : αM) :
Set.indicator s (fun a => f a * g a) a = Set.indicator s f a * g a
theorem Set.indicator_mul_right {α : Type u_1} {M : Type u_2} [inst : MulZeroClass M] {a : α} (s : Set α) (f : αM) (g : αM) :
Set.indicator s (fun a => f a * g a) a = f a * Set.indicator s g a
theorem Set.inter_indicator_mul {α : Type u_1} {M : Type u_2} [inst : MulZeroClass M] {t1 : Set α} {t2 : Set α} (f : αM) (g : αM) (x : α) :
Set.indicator (t1 t2) (fun x => f x * g x) x = Set.indicator t1 f x * Set.indicator t2 g x
theorem Set.inter_indicator_one {α : Type u_1} {M : Type u_2} [inst : MulZeroOneClass M] {s : Set α} {t : Set α} :
theorem Set.indicator_prod_one {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : MulZeroOneClass M] {s : Set α} {t : Set β} {x : α} {y : β} :
Set.indicator (s ×ˢ t) 1 (x, y) = Set.indicator s 1 x * Set.indicator t 1 y
theorem Set.indicator_eq_zero_iff_not_mem {α : Type u_1} (M : Type u_2) [inst : MulZeroOneClass M] [inst : Nontrivial M] {U : Set α} {x : α} :
Set.indicator U 1 x = 0 ¬x U
theorem Set.indicator_eq_one_iff_mem {α : Type u_1} (M : Type u_2) [inst : MulZeroOneClass M] [inst : Nontrivial M] {U : Set α} {x : α} :
Set.indicator U 1 x = 1 x U
theorem Set.indicator_one_inj {α : Type u_1} (M : Type u_2) [inst : MulZeroOneClass M] [inst : Nontrivial M] {U : Set α} {V : Set α} (h : Set.indicator U 1 = Set.indicator V 1) :
U = V
theorem Set.indicator_apply_le' {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} {a : α} {y : M} [inst : LE M] (hfg : a sf a y) (hg : ¬a s0 y) :
theorem Set.mulIndicator_apply_le' {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} {a : α} {y : M} [inst : LE M] (hfg : a sf a y) (hg : ¬a s1 y) :
theorem Set.indicator_le' {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} {g : αM} [inst : LE M] (hfg : ∀ (a : α), a sf a g a) (hg : ∀ (a : α), ¬a s0 g a) :
theorem Set.mulIndicator_le' {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} {g : αM} [inst : 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_2} [inst : Zero M] {s : Set α} {g : αM} {a : α} [inst : LE M] {y : M} (hfg : a sy g a) (hf : ¬a sy 0) :
theorem Set.le_mulIndicator_apply {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {g : αM} {a : α} [inst : LE M] {y : M} (hfg : a sy g a) (hf : ¬a sy 1) :
theorem Set.le_indicator {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} {g : αM} [inst : LE M] (hfg : ∀ (a : α), a sf a g a) (hf : ∀ (a : α), ¬a sf a 0) :
theorem Set.le_mulIndicator {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} {g : αM} [inst : LE M] (hfg : ∀ (a : α), a sf a g a) (hf : ∀ (a : α), ¬a sf a 1) :
theorem Set.indicator_apply_nonneg {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} {a : α} [inst : Preorder M] (h : a s0 f a) :
theorem Set.one_le_mulIndicator_apply {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} {a : α} [inst : Preorder M] (h : a s1 f a) :
theorem Set.indicator_nonneg {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} [inst : Preorder M] (h : ∀ (a : α), a s0 f a) (a : α) :
theorem Set.one_le_mulIndicator {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} [inst : Preorder M] (h : ∀ (a : α), a s1 f a) (a : α) :
theorem Set.indicator_apply_nonpos {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} {a : α} [inst : Preorder M] (h : a sf a 0) :
theorem Set.mulIndicator_apply_le_one {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} {a : α} [inst : Preorder M] (h : a sf a 1) :
theorem Set.indicator_nonpos {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} [inst : Preorder M] (h : ∀ (a : α), a sf a 0) (a : α) :
theorem Set.mulIndicator_le_one {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} [inst : Preorder M] (h : ∀ (a : α), a sf a 1) (a : α) :
theorem Set.indicator_le_indicator {α : Type u_2} {M : Type u_1} [inst : Zero M] {s : Set α} {f : αM} {g : αM} {a : α} [inst : Preorder M] (h : f a g a) :
theorem Set.mulIndicator_le_mulIndicator {α : Type u_2} {M : Type u_1} [inst : One M] {s : Set α} {f : αM} {g : αM} {a : α} [inst : Preorder M] (h : f a g a) :
theorem Set.indicator_le_indicator_of_subset {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {t : Set α} {f : αM} [inst : Preorder M] (h : s t) (hf : ∀ (a : α), 0 f a) (a : α) :
theorem Set.mulIndicator_le_mulIndicator_of_subset {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {t : Set α} {f : αM} [inst : Preorder M] (h : s t) (hf : ∀ (a : α), 1 f a) (a : α) :
theorem Set.indicator_le_self' {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {f : αM} [inst : Preorder M] (hf : ∀ (x : α), ¬x s0 f x) :
theorem Set.mulIndicator_le_self' {α : Type u_1} {M : Type u_2} [inst : One M] {s : Set α} {f : αM} [inst : Preorder M] (hf : ∀ (x : α), ¬x s1 f x) :
theorem Set.indicator_unionᵢ_apply {α : Type u_3} {ι : Sort u_1} {M : Type u_2} [inst : CompleteLattice M] [inst : Zero M] (h1 : = 0) (s : ιSet α) (f : αM) (x : α) :
Set.indicator (Set.unionᵢ fun i => s i) f x = i, Set.indicator (s i) f x
theorem Set.mulIndicator_unionᵢ_apply {α : Type u_3} {ι : Sort u_1} {M : Type u_2} [inst : CompleteLattice M] [inst : One M] (h1 : = 1) (s : ιSet α) (f : αM) (x : α) :
Set.mulIndicator (Set.unionᵢ fun i => s i) f x = i, Set.mulIndicator (s i) f x
theorem Set.indicator_le_self {α : Type u_1} {M : Type u_2} [inst : CanonicallyOrderedAddMonoid M] (s : Set α) (f : αM) :
theorem Set.mulIndicator_le_self {α : Type u_1} {M : Type u_2} [inst : CanonicallyOrderedMonoid M] (s : Set α) (f : αM) :
theorem Set.indicator_apply_le {α : Type u_1} {M : Type u_2} [inst : CanonicallyOrderedAddMonoid M] {a : α} {s : Set α} {f : αM} {g : αM} (hfg : a sf a g a) :
Set.indicator s f a g a
theorem Set.mulIndicator_apply_le {α : Type u_1} {M : Type u_2} [inst : CanonicallyOrderedMonoid M] {a : α} {s : Set α} {f : αM} {g : αM} (hfg : a sf a g a) :
theorem Set.indicator_le {α : Type u_1} {M : Type u_2} [inst : CanonicallyOrderedAddMonoid M] {s : Set α} {f : αM} {g : αM} (hfg : ∀ (a : α), a sf a g a) :
theorem Set.mulIndicator_le {α : Type u_1} {M : Type u_2} [inst : CanonicallyOrderedMonoid M] {s : Set α} {f : αM} {g : αM} (hfg : ∀ (a : α), a sf a g a) :
theorem Set.indicator_le_indicator_nonneg {α : Type u_2} {β : Type u_1} [inst : LinearOrder β] [inst : Zero β] (s : Set α) (f : αβ) :
Set.indicator s f Set.indicator { x | 0 f x } f
theorem Set.indicator_nonpos_le_indicator {α : Type u_2} {β : Type u_1} [inst : LinearOrder β] [inst : Zero β] (s : Set α) (f : αβ) :
Set.indicator { x | f x 0 } f Set.indicator s f
theorem AddMonoidHom.map_indicator {α : Type u_3} {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (s : Set α) (g : αM) (x : α) :
f (Set.indicator s g x) = Set.indicator s (f g) x
theorem MonoidHom.map_mulIndicator {α : Type u_3} {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) (s : Set α) (g : αM) (x : α) :
f (Set.mulIndicator s g x) = Set.mulIndicator s (f g) x