norm_indicator_eq_indicator_norm
theorem norm_indicator_eq_indicator_norm :
∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedAddCommGroup E] {s : Set α} (f : α → E) (a : α),
‖s.indicator f a‖ = s.indicator (fun a => ‖f a‖) a
The theorem `norm_indicator_eq_indicator_norm` states that for any type `α`, any seminormed additive commutative group `E`, any set `s` of type `α` and any function `f` from `α` to `E`, and for any element `a` of type `α`, the norm of the indicator function of `s` applied to the function `f` at `a` is equal to the indicator function of `s` applied to the function that maps `a` to the norm of `f` at `a`. In mathematical terms, this states that ‖1[s](f(a))‖ = 1[s](‖f(a)‖), where 1[s] denotes the indicator function of the set `s`.
More concisely: For any seminormed additive commutative group E, set s, and function f, the norm of the indicator function of set s applied to function f at an element a equals the indicator function of set s applied to the norm function of f at element a. In other words, ‖1[s](f(a))‖ = 1[s](‖f(a)‖).
|
nnnorm_indicator_eq_indicator_nnnorm
theorem nnnorm_indicator_eq_indicator_nnnorm :
∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedAddCommGroup E] {s : Set α} (f : α → E) (a : α),
‖s.indicator f a‖₊ = s.indicator (fun a => ‖f a‖₊) a
The theorem `nnnorm_indicator_eq_indicator_nnnorm` states that for any type `α`, any semi-normed additive commutative group `E`, any set `s` of elements of type `α`, any function `f` from `α` to `E`, and any element `a` of type `α`, the non-negative norm (`‖‖₊`) of the set indicator function applied to `s`, `f`, and `a` is equal to the set indicator function applied to `s`, the function mapping each element to its non-negative norm, and `a`. In simpler terms, it says that the non-negative norm of the indicator function of a set is the same as the indicator function of the non-negative norm.
More concisely: For any semi-normed additive commutative group E, set s ⊆ α, function f : α → E, and element a ∈ α, the non-negative norm ∥IndicATOR s∥₊(a) = IndicATOR {x : α | ∥f x∥₊ ≤ ∥f a∥₊}(a).
|