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} [SeminormedAddCommGroup E] {s : Set α} (f : α → E) (a : α) : ‖Set.indicator s f a‖ = Set.indicator s (fun (a : α) => ‖f a‖) a

theorem nnnorm_indicator_eq_indicator_nnnorm {α : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {s : Set α} (f : α → E) (a : α) : ‖Set.indicator s f a‖₊ = Set.indicator s (fun (a : α) => ‖f a‖₊) a

theorem norm_indicator_le_of_subset {α : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {s : Set α} {t : Set α} (h : s ⊆ t) (f : α → E) (a : α) : ‖Set.indicator s f a‖ ≤ ‖Set.indicator t f a‖

theorem indicator_norm_le_norm_self {α : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {s : Set α} (f : α → E) (a : α) : Set.indicator s (fun (a : α) => ‖f a‖) a ≤ ‖f a‖

theorem norm_indicator_le_norm_self {α : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {s : Set α} (f : α → E) (a : α) : ‖Set.indicator s f a‖ ≤ ‖f a‖