Documentation

Mathlib.Analysis.NormedSpace.IndicatorFunction

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 : α) :
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 norm_indicator_le_of_subset {α : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {s : Set α} {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 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