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} [normed_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} [normed_group E] {s : set α} (f : α → E) (a : α) :
nnnorm (s.indicator f a) = s.indicator (λ (a : α), nnnorm (f a)) a
theorem norm_indicator_le_of_subset {α : Type u_1} {E : Type u_2} [normed_group E] {s t : set α} (h : s t) (f : α → E) (a : α) :
theorem indicator_norm_le_norm_self {α : Type u_1} {E : Type u_2} [normed_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} [normed_group E] {s : set α} (f : α → E) (a : α) :