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 α} (hf : f =ᶠ[l ⊓ 𝓟 s] g) (hs : s =ᶠ[l] t) :

s.indicator f =ᶠ[l] t.indicator g

source

theorem indicator_union_eventually_eq {α : Type u_1} {M : Type u_3} [add_monoid M] {s t : set α} {f : α → M} {l : filter α} (h : ∀ᶠ (a : α) in l, a ∉ s ∩ t) :

(s ∪ t).indicator f =ᶠ[l] s.indicator f + t.indicator f

source

theorem indicator_eventually_le_indicator {α : Type u_1} {β : Type u_2} [has_zero β] [preorder β] {s : set α} {f g : α → β} {l : filter α} (h : f ≤ᶠ[l ⊓ 𝓟 s] g) :

s.indicator f ≤ᶠ[l] s.indicator g

source

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

source

theorem tendsto_indicator_of_antimono {α : Type u_1} {β : Type u_2} {ι : Type u_3} [preorder ι] [has_zero β] (s : ι → set α) (hs : ∀ ⦃i j : ι⦄, i ≤ j → s j ⊆ s i) (f : α → β) (a : α) :

filter.tendsto (λ (i : ι), (s i).indicator f a) filter.at_top (pure ((⋂ (i : ι), s i).indicator f a))

source

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