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

theorem nnnorm_indicator_eq_indicator_nnnorm {α : Type u_1} {E : Type u_2} [seminormed_add_comm_group E] {s : set α} (f : α → E) (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 : α) :