Documentation

Mathlib.Algebra.Order.Group.Indicator

Support of a function in an order #

This file relates the support of a function to order constructions.

theorem Function.support_sup {α : Type u_2} {M : Type u_4} [Zero M] [SemilatticeSup M] (f : αM) (g : αM) :
theorem Function.mulSupport_sup {α : Type u_2} {M : Type u_4} [One M] [SemilatticeSup M] (f : αM) (g : αM) :
theorem Function.support_inf {α : Type u_2} {M : Type u_4} [Zero M] [SemilatticeInf M] (f : αM) (g : αM) :
theorem Function.mulSupport_inf {α : Type u_2} {M : Type u_4} [One M] [SemilatticeInf M] (f : αM) (g : αM) :
theorem Function.support_max {α : Type u_2} {M : Type u_4} [Zero M] [LinearOrder M] (f : αM) (g : αM) :
(Function.support fun (x : α) => max (f x) (g x)) Function.support f Function.support g
theorem Function.mulSupport_max {α : Type u_2} {M : Type u_4} [One M] [LinearOrder M] (f : αM) (g : αM) :
theorem Function.support_min {α : Type u_2} {M : Type u_4} [Zero M] [LinearOrder M] (f : αM) (g : αM) :
(Function.support fun (x : α) => min (f x) (g x)) Function.support f Function.support g
theorem Function.mulSupport_min {α : Type u_2} {M : Type u_4} [One M] [LinearOrder M] (f : αM) (g : αM) :
theorem Function.support_iSup {ι : Sort u_1} {α : Type u_2} {M : Type u_4} [Zero M] [ConditionallyCompleteLattice M] [Nonempty ι] (f : ιαM) :
(Function.support fun (x : α) => ⨆ (i : ι), f i x) ⋃ (i : ι), Function.support (f i)
theorem Function.mulSupport_iSup {ι : Sort u_1} {α : Type u_2} {M : Type u_4} [One M] [ConditionallyCompleteLattice M] [Nonempty ι] (f : ιαM) :
(Function.mulSupport fun (x : α) => ⨆ (i : ι), f i x) ⋃ (i : ι), Function.mulSupport (f i)
theorem Function.support_iInf {ι : Sort u_1} {α : Type u_2} {M : Type u_4} [Zero M] [ConditionallyCompleteLattice M] [Nonempty ι] (f : ιαM) :
(Function.support fun (x : α) => ⨅ (i : ι), f i x) ⋃ (i : ι), Function.support (f i)
theorem Function.mulSupport_iInf {ι : Sort u_1} {α : Type u_2} {M : Type u_4} [One M] [ConditionallyCompleteLattice M] [Nonempty ι] (f : ιαM) :
(Function.mulSupport fun (x : α) => ⨅ (i : ι), f i x) ⋃ (i : ι), Function.mulSupport (f i)
theorem Set.indicator_apply_le' {α : Type u_2} {M : Type u_4} [LE M] [Zero M] {s : Set α} {f : αM} {a : α} {y : M} (hfg : a sf a y) (hg : as0 y) :
s.indicator f a y
theorem Set.mulIndicator_apply_le' {α : Type u_2} {M : Type u_4} [LE M] [One M] {s : Set α} {f : αM} {a : α} {y : M} (hfg : a sf a y) (hg : as1 y) :
s.mulIndicator f a y
theorem Set.indicator_le' {α : Type u_2} {M : Type u_4} [LE M] [Zero M] {s : Set α} {f : αM} {g : αM} (hfg : as, f a g a) (hg : as, 0 g a) :
s.indicator f g
theorem Set.mulIndicator_le' {α : Type u_2} {M : Type u_4} [LE M] [One M] {s : Set α} {f : αM} {g : αM} (hfg : as, f a g a) (hg : as, 1 g a) :
s.mulIndicator f g
theorem Set.le_indicator_apply {α : Type u_2} {M : Type u_4} [LE M] [Zero M] {s : Set α} {g : αM} {a : α} {y : M} (hfg : a sy g a) (hf : asy 0) :
y s.indicator g a
theorem Set.le_mulIndicator_apply {α : Type u_2} {M : Type u_4} [LE M] [One M] {s : Set α} {g : αM} {a : α} {y : M} (hfg : a sy g a) (hf : asy 1) :
y s.mulIndicator g a
theorem Set.le_indicator {α : Type u_2} {M : Type u_4} [LE M] [Zero M] {s : Set α} {f : αM} {g : αM} (hfg : as, f a g a) (hf : as, f a 0) :
f s.indicator g
theorem Set.le_mulIndicator {α : Type u_2} {M : Type u_4} [LE M] [One M] {s : Set α} {f : αM} {g : αM} (hfg : as, f a g a) (hf : as, f a 1) :
f s.mulIndicator g
theorem Set.indicator_apply_nonneg {α : Type u_2} {M : Type u_4} [Preorder M] [Zero M] {s : Set α} {f : αM} {a : α} (h : a s0 f a) :
0 s.indicator f a
theorem Set.one_le_mulIndicator_apply {α : Type u_2} {M : Type u_4} [Preorder M] [One M] {s : Set α} {f : αM} {a : α} (h : a s1 f a) :
1 s.mulIndicator f a
theorem Set.indicator_nonneg {α : Type u_2} {M : Type u_4} [Preorder M] [Zero M] {s : Set α} {f : αM} (h : as, 0 f a) (a : α) :
0 s.indicator f a
theorem Set.one_le_mulIndicator {α : Type u_2} {M : Type u_4} [Preorder M] [One M] {s : Set α} {f : αM} (h : as, 1 f a) (a : α) :
1 s.mulIndicator f a
theorem Set.indicator_apply_nonpos {α : Type u_2} {M : Type u_4} [Preorder M] [Zero M] {s : Set α} {f : αM} {a : α} (h : a sf a 0) :
s.indicator f a 0
theorem Set.mulIndicator_apply_le_one {α : Type u_2} {M : Type u_4} [Preorder M] [One M] {s : Set α} {f : αM} {a : α} (h : a sf a 1) :
s.mulIndicator f a 1
theorem Set.indicator_nonpos {α : Type u_2} {M : Type u_4} [Preorder M] [Zero M] {s : Set α} {f : αM} (h : as, f a 0) (a : α) :
s.indicator f a 0
theorem Set.mulIndicator_le_one {α : Type u_2} {M : Type u_4} [Preorder M] [One M] {s : Set α} {f : αM} (h : as, f a 1) (a : α) :
s.mulIndicator f a 1
theorem Set.indicator_le_indicator {α : Type u_2} {M : Type u_4} [Preorder M] [Zero M] {s : Set α} {f : αM} {g : αM} {a : α} (h : f a g a) :
s.indicator f a s.indicator g a
theorem Set.mulIndicator_le_mulIndicator {α : Type u_2} {M : Type u_4} [Preorder M] [One M] {s : Set α} {f : αM} {g : αM} {a : α} (h : f a g a) :
s.mulIndicator f a s.mulIndicator g a
theorem Set.indicator_le_indicator_of_subset {α : Type u_2} {M : Type u_4} [Preorder M] [Zero M] {s : Set α} {t : Set α} {f : αM} (h : s t) (hf : ∀ (a : α), 0 f a) (a : α) :
s.indicator f a t.indicator f a
theorem Set.mulIndicator_le_mulIndicator_of_subset {α : Type u_2} {M : Type u_4} [Preorder M] [One M] {s : Set α} {t : Set α} {f : αM} (h : s t) (hf : ∀ (a : α), 1 f a) (a : α) :
s.mulIndicator f a t.mulIndicator f a
theorem Set.indicator_le_self' {α : Type u_2} {M : Type u_4} [Preorder M] [Zero M] {s : Set α} {f : αM} (hf : xs, 0 f x) :
s.indicator f f
theorem Set.mulIndicator_le_self' {α : Type u_2} {M : Type u_4} [Preorder M] [One M] {s : Set α} {f : αM} (hf : xs, 1 f x) :
s.mulIndicator f f
theorem Set.indicator_le_indicator_nonneg {α : Type u_2} {M : Type u_4} [Zero M] [LinearOrder M] (s : Set α) (f : αM) :
s.indicator f {a : α | 0 f a}.indicator f
theorem Set.indicator_nonpos_le_indicator {α : Type u_2} {M : Type u_4} [Zero M] [LinearOrder M] (s : Set α) (f : αM) :
{a : α | f a 0}.indicator f s.indicator f
theorem Set.indicator_iUnion_apply {ι : Sort u_1} {α : Type u_2} {M : Type u_4} [CompleteLattice M] [Zero M] (h1 : = 0) (s : ιSet α) (f : αM) (x : α) :
(⋃ (i : ι), s i).indicator f x = ⨆ (i : ι), (s i).indicator f x
theorem Set.mulIndicator_iUnion_apply {ι : Sort u_1} {α : Type u_2} {M : Type u_4} [CompleteLattice M] [One M] (h1 : = 1) (s : ιSet α) (f : αM) (x : α) :
(⋃ (i : ι), s i).mulIndicator f x = ⨆ (i : ι), (s i).mulIndicator f x
theorem Set.indicator_iInter_apply {ι : Sort u_1} {α : Type u_2} {M : Type u_4} [CompleteLattice M] [Zero M] [Nonempty ι] (h1 : = 0) (s : ιSet α) (f : αM) (x : α) :
(⋂ (i : ι), s i).indicator f x = ⨅ (i : ι), (s i).indicator f x
theorem Set.mulIndicator_iInter_apply {ι : Sort u_1} {α : Type u_2} {M : Type u_4} [CompleteLattice M] [One M] [Nonempty ι] (h1 : = 1) (s : ιSet α) (f : αM) (x : α) :
(⋂ (i : ι), s i).mulIndicator f x = ⨅ (i : ι), (s i).mulIndicator f x
theorem Set.indicator_le_self {α : Type u_2} {M : Type u_4} [CanonicallyOrderedAddCommMonoid M] (s : Set α) (f : αM) :
s.indicator f f
theorem Set.mulIndicator_le_self {α : Type u_2} {M : Type u_4} [CanonicallyOrderedCommMonoid M] (s : Set α) (f : αM) :
s.mulIndicator f f
theorem Set.indicator_apply_le {α : Type u_2} {M : Type u_4} [CanonicallyOrderedAddCommMonoid M] {a : α} {s : Set α} {f : αM} {g : αM} (hfg : a sf a g a) :
s.indicator f a g a
theorem Set.mulIndicator_apply_le {α : Type u_2} {M : Type u_4} [CanonicallyOrderedCommMonoid M] {a : α} {s : Set α} {f : αM} {g : αM} (hfg : a sf a g a) :
s.mulIndicator f a g a
theorem Set.indicator_le {α : Type u_2} {M : Type u_4} [CanonicallyOrderedAddCommMonoid M] {s : Set α} {f : αM} {g : αM} (hfg : as, f a g a) :
s.indicator f g
theorem Set.mulIndicator_le {α : Type u_2} {M : Type u_4} [CanonicallyOrderedCommMonoid M] {s : Set α} {f : αM} {g : αM} (hfg : as, f a g a) :
s.mulIndicator f g
theorem Set.abs_indicator_symmDiff {α : Type u_2} {M : Type u_4} [LinearOrderedAddCommGroup M] (s : Set α) (t : Set α) (f : αM) (x : α) :
|(symmDiff s t).indicator f x| = |s.indicator f x - t.indicator f x|
theorem Set.mabs_mulIndicator_symmDiff {α : Type u_2} {M : Type u_4} [LinearOrderedCommGroup M] (s : Set α) (t : Set α) (f : αM) (x : α) :
mabs ((symmDiff s t).mulIndicator f x) = mabs (s.mulIndicator f x / t.mulIndicator f x)