Indicator function and filters #
Properties of additive and multiplicative indicator functions involving =ᶠ
and ≤ᶠ
.
Tags #
indicator, characteristic, filter
theorem
Monotone.tendsto_mulIndicator
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[Preorder ι]
[One β]
(s : ι → Set α)
(hs : Monotone s)
(f : α → β)
(a : α)
:
Filter.Tendsto (fun (i : ι) => (s i).mulIndicator f a) Filter.atTop (pure ((⋃ (i : ι), s i).mulIndicator f a))
theorem
Monotone.tendsto_indicator
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[Preorder ι]
[Zero β]
(s : ι → Set α)
(hs : Monotone s)
(f : α → β)
(a : α)
:
Filter.Tendsto (fun (i : ι) => (s i).indicator f a) Filter.atTop (pure ((⋃ (i : ι), s i).indicator f a))
theorem
Antitone.tendsto_mulIndicator
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[Preorder ι]
[One β]
(s : ι → Set α)
(hs : Antitone s)
(f : α → β)
(a : α)
:
Filter.Tendsto (fun (i : ι) => (s i).mulIndicator f a) Filter.atTop (pure ((⋂ (i : ι), s i).mulIndicator f a))
theorem
Antitone.tendsto_indicator
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[Preorder ι]
[Zero β]
(s : ι → Set α)
(hs : Antitone s)
(f : α → β)
(a : α)
:
Filter.Tendsto (fun (i : ι) => (s i).indicator f a) Filter.atTop (pure ((⋂ (i : ι), s i).indicator f a))
theorem
mulIndicator_biUnion_finset_eventuallyEq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[One β]
(s : ι → Set α)
(f : α → β)
(a : α)
:
(fun (n : Finset ι) => (⋃ i ∈ n, s i).mulIndicator f a) =ᶠ[Filter.atTop] fun (x : Finset ι) =>
(Set.iUnion s).mulIndicator f a
theorem
indicator_biUnion_finset_eventuallyEq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[Zero β]
(s : ι → Set α)
(f : α → β)
(a : α)
:
(fun (n : Finset ι) => (⋃ i ∈ n, s i).indicator f a) =ᶠ[Filter.atTop] fun (x : Finset ι) => (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
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))