Indicator function and filters #
Properties of indicator functions involving =ᶠ and ≤ᶠ≤ᶠ.
Tags #
indicator, characteristic, filter
theorem
indicator_eventuallyEq
{α : Type u_1}
{M : Type u_2}
[inst : Zero M]
{s : Set α}
{t : Set α}
{f : α → M}
{g : α → M}
{l : Filter α}
(hf : f =ᶠ[l ⊓ Filter.principal s] g)
(hs : s =ᶠ[l] t)
:
Set.indicator s f =ᶠ[l] Set.indicator t g
theorem
indicator_union_eventuallyEq
{α : Type u_1}
{M : Type u_2}
[inst : AddMonoid M]
{s : Set α}
{t : Set α}
{f : α → M}
{l : Filter α}
(h : Filter.Eventually (fun a => ¬a ∈ s ∩ t) l)
:
Set.indicator (s ∪ t) f =ᶠ[l] Set.indicator s f + Set.indicator t f
theorem
indicator_eventuallyLE_indicator
{α : Type u_1}
{β : Type u_2}
[inst : Zero β]
[inst : Preorder β]
{s : Set α}
{f : α → β}
{g : α → β}
{l : Filter α}
(h : f ≤ᶠ[l ⊓ Filter.principal s] g)
:
Set.indicator s f ≤ᶠ[l] Set.indicator s g
theorem
Monotone.tendsto_indicator
{α : Type u_3}
{β : Type u_2}
{ι : Type u_1}
[inst : Preorder ι]
[inst : Zero β]
(s : ι → Set α)
(hs : Monotone s)
(f : α → β)
(a : α)
:
Filter.Tendsto (fun i => Set.indicator (s i) f a) Filter.atTop (pure (Set.indicator (Set.unionᵢ fun i => s i) f a))
theorem
Antitone.tendsto_indicator
{α : Type u_3}
{β : Type u_2}
{ι : Type u_1}
[inst : Preorder ι]
[inst : Zero β]
(s : ι → Set α)
(hs : Antitone s)
(f : α → β)
(a : α)
:
Filter.Tendsto (fun i => Set.indicator (s i) f a) Filter.atTop (pure (Set.indicator (Set.interᵢ fun i => s i) f a))
theorem
tendsto_indicator_bunionᵢ_finset
{α : Type u_3}
{β : Type u_2}
{ι : Type u_1}
[inst : Zero β]
(s : ι → Set α)
(f : α → β)
(a : α)
:
Filter.Tendsto (fun n => Set.indicator (Set.unionᵢ fun i => Set.unionᵢ fun h => s i) f a) Filter.atTop
(pure (Set.indicator (Set.unionᵢ s) f a))
theorem
Filter.EventuallyEq.indicator
{α : Type u_2}
{β : Type u_1}
[inst : Zero β]
{l : Filter α}
{f : α → β}
{g : α → β}
{s : Set α}
(hfg : f =ᶠ[l] g)
:
Set.indicator s f =ᶠ[l] Set.indicator s g