Indicator function and filters #
Properties of additive and multiplicative indicator functions involving =ᶠ
and ≤ᶠ
.
Tags #
indicator, characteristic, filter
theorem
indicator_eventuallyEq
{α : Type u_1}
{M : Type u_3}
[Zero M]
{s : Set α}
{t : Set α}
{f : α → M}
{g : α → M}
{l : Filter α}
(hf : (l ⊓ Filter.principal s).EventuallyEq f g)
(hs : l.EventuallyEq s t)
:
l.EventuallyEq (s.indicator f) (t.indicator g)
theorem
mulIndicator_eventuallyEq
{α : Type u_1}
{M : Type u_3}
[One M]
{s : Set α}
{t : Set α}
{f : α → M}
{g : α → M}
{l : Filter α}
(hf : (l ⊓ Filter.principal s).EventuallyEq f g)
(hs : l.EventuallyEq s t)
:
l.EventuallyEq (s.mulIndicator f) (t.mulIndicator g)
theorem
indicator_eventuallyLE_indicator
{α : Type u_1}
{β : Type u_2}
[Zero β]
[Preorder β]
{s : Set α}
{f : α → β}
{g : α → β}
{l : Filter α}
(h : (l ⊓ Filter.principal s).EventuallyLE f g)
:
l.EventuallyLE (s.indicator f) (s.indicator g)
theorem
mulIndicator_eventuallyLE_mulIndicator
{α : Type u_1}
{β : Type u_2}
[One β]
[Preorder β]
{s : Set α}
{f : α → β}
{g : α → β}
{l : Filter α}
(h : (l ⊓ Filter.principal s).EventuallyLE f g)
:
l.EventuallyLE (s.mulIndicator f) (s.mulIndicator g)
theorem
indicator_biUnion_finset_eventuallyEq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[Zero β]
(s : ι → Set α)
(f : α → β)
(a : α)
:
Filter.atTop.EventuallyEq (fun (n : Finset ι) => (⋃ i ∈ n, s i).indicator f a) fun (x : Finset ι) =>
(Set.iUnion s).indicator f a
theorem
mulIndicator_biUnion_finset_eventuallyEq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[One β]
(s : ι → Set α)
(f : α → β)
(a : α)
:
Filter.atTop.EventuallyEq (fun (n : Finset ι) => (⋃ i ∈ n, s i).mulIndicator f a) fun (x : Finset ι) =>
(Set.iUnion s).mulIndicator f a
theorem
tendsto_indicator_biUnion_finset
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[Zero β]
(s : ι → Set α)
(f : α → β)
(a : α)
:
Filter.Tendsto (fun (n : Finset ι) => (⋃ i ∈ n, s i).indicator f a) Filter.atTop (pure ((Set.iUnion s).indicator f a))
theorem
tendsto_mulIndicator_biUnion_finset
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[One β]
(s : ι → Set α)
(f : α → β)
(a : α)
:
Filter.Tendsto (fun (n : Finset ι) => (⋃ i ∈ n, s i).mulIndicator f a) Filter.atTop
(pure ((Set.iUnion s).mulIndicator f a))
theorem
Filter.EventuallyEq.support
{α : Type u_1}
{β : Type u_2}
[Zero β]
{f : α → β}
{g : α → β}
{l : Filter α}
(h : l.EventuallyEq f g)
:
l.EventuallyEq (Function.support f) (Function.support g)
theorem
Filter.EventuallyEq.mulSupport
{α : Type u_1}
{β : Type u_2}
[One β]
{f : α → β}
{g : α → β}
{l : Filter α}
(h : l.EventuallyEq f g)
:
l.EventuallyEq (Function.mulSupport f) (Function.mulSupport g)