# Indicator function and (e)norm #

This file contains a few simple lemmas about `Set.indicator`, `norm` and `enorm`.

## Tags #

indicator, norm

source
theorem enorm_indicator_eq_indicator_enorm {α : Type u_1} {ε : Type u_2} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {s : Set α} (f : α → ε) (a : α) :
‖s.indicator f a‖ₑ = s.indicator (fun (a : α) => ‖f a‖ₑ) a
source
theorem enorm_indicator_le_of_subset {α : Type u_1} {ε : Type u_2} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {s t : Set α} (h : s ⊆ t) (f : α → ε) (a : α) :
‖s.indicator f a‖ₑ ≤ ‖t.indicator f a‖ₑ
source
theorem indicator_enorm_le_enorm_self {α : Type u_1} {ε : Type u_2} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {s : Set α} (f : α → ε) (a : α) :
s.indicator (fun (a : α) => ‖f a‖ₑ) a ≤ ‖f a‖ₑ
source
theorem enorm_indicator_le_enorm_self {α : Type u_1} {ε : Type u_2} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {s : Set α} (f : α → ε) (a : α) :
‖s.indicator f a‖ₑ ≤ ‖f a‖ₑ
source
theorem norm_indicator_eq_indicator_norm {α : Type u_1} {E : Type u_2} [SeminormedAddGroup E] {s : Set α} (f : α → E) (a : α) :
‖s.indicator f a‖ = s.indicator (fun (a : α) => ‖f a‖) a
source
theorem nnnorm_indicator_eq_indicator_nnnorm {α : Type u_1} {E : Type u_2} [SeminormedAddGroup E] {s : Set α} (f : α → E) (a : α) :
‖s.indicator f a‖₊ = s.indicator (fun (a : α) => ‖f a‖₊) a
source
theorem norm_indicator_le_of_subset {α : Type u_1} {E : Type u_2} [SeminormedAddGroup E] {s t : Set α} (h : s ⊆ t) (f : α → E) (a : α) :
‖s.indicator f a‖ ≤ ‖t.indicator f a‖
source
theorem indicator_norm_le_norm_self {α : Type u_1} {E : Type u_2} [SeminormedAddGroup E] {s : Set α} (f : α → E) (a : α) :
s.indicator (fun (a : α) => ‖f a‖) a ≤ ‖f a‖
source
theorem norm_indicator_le_norm_self {α : Type u_1} {E : Type u_2} [SeminormedAddGroup E] {s : Set α} (f : α → E) (a : α) :
‖s.indicator f a‖ ≤ ‖f a‖