mathlib documentation

order.filter.indicator_function

Indicator function and filters

Properties of indicator functions involving =ᶠ and ≤ᶠ.

Tags

indicator, characteristic, filter

theorem indicator_eventually_eq {α : Type u_1} {M : Type u_3} [has_zero M] {s t : set α} {f g : α → M} {l : filter α} :
f =ᶠ[l 𝓟 s] gs =ᶠ[l] ts.indicator f =ᶠ[l] t.indicator g

theorem indicator_union_eventually_eq {α : Type u_1} {M : Type u_3} [add_monoid M] {s t : set α} {f : α → M} {l : filter α} :
(∀ᶠ (a : α) in l, a s t)(s t).indicator f =ᶠ[l] s.indicator f + t.indicator f

theorem indicator_eventually_le_indicator {α : Type u_1} {β : Type u_2} [has_zero β] [preorder β] {s : set α} {f g : α → β} {l : filter α} :

theorem tendsto_indicator_of_monotone {α : Type u_1} {β : Type u_2} {ι : Type u_3} [preorder ι] [has_zero β] (s : ι → set α) (hs : monotone s) (f : α → β) (a : α) :
filter.tendsto (λ (i : ι), (s i).indicator f a) filter.at_top (pure ((⋃ (i : ι), s i).indicator f a))

theorem tendsto_indicator_of_antimono {α : Type u_1} {β : Type u_2} {ι : Type u_3} [preorder ι] [has_zero β] (s : ι → set α) (hs : ∀ ⦃i j : ι⦄, i js j s i) (f : α → β) (a : α) :
filter.tendsto (λ (i : ι), (s i).indicator f a) filter.at_top (pure ((⋂ (i : ι), s i).indicator f a))

theorem tendsto_indicator_bUnion_finset {α : Type u_1} {β : Type u_2} {ι : Type u_3} [has_zero β] (s : ι → set α) (f : α → β) (a : α) :
filter.tendsto (λ (n : finset ι), (⋃ (i : ι) (H : i n), s i).indicator f a) filter.at_top (pure ((set.Union s).indicator f a))