Indicator function and (e)norm

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

Tags

indicator, norm

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

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

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

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

theorem indicator_enorm_le_enorm_self {α : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {s : Set α} (f : α → E) (a : α) : s.indicator (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 : α) : ‖s.indicator f a‖ ≤ ‖f a‖

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