mathlib3 documentation

analysis.normed_space.indicator_function

Indicator function and norm #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : α) :
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 : α) :