mathlib documentation

analysis.normed_space.indicator_function

Indicator function and norm #

This file contains a few simple lemmas about set.indicator and norm.

Tags #

indicator, norm

theorem norm_indicator_eq_indicator_norm {α : Type u_1} {E : Type u_2} [seminormed_add_comm_group E] {s : set α} (f : α → E) (a : α) :

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

theorem nnnorm_indicator_eq_indicator_nnnorm {α : Type u_1} {E : Type u_2} [seminormed_add_comm_group E] {s : set α} (f : α → E) (a : α) :

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

theorem norm_indicator_le_of_subset {α : Type u_1} {E : Type u_2} [seminormed_add_comm_group E] {s t : set α} (h : s ⊆ t) (f : α → E) (a : α) :

∥s.indicator f a∥ ≤ ∥t.indicator f a∥

theorem indicator_norm_le_norm_self {α : Type u_1} {E : Type u_2} [seminormed_add_comm_group E] {s : set α} (f : α → E) (a : α) :

s.indicator (λ (a : α), ∥f a∥) a ≤ ∥f a∥

theorem norm_indicator_le_norm_self {α : Type u_1} {E : Type u_2} [seminormed_add_comm_group E] {s : set α} (f : α → E) (a : α) :

∥s.indicator f a∥ ≤ ∥f a∥