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 : f =ᶠ[l ⊓ Filter.principal s] g)
(hs : s =ᶠ[l] t)
:
Set.indicator s f =ᶠ[l] Set.indicator t g
theorem
mulIndicator_eventuallyEq
{α : Type u_1}
{M : Type u_3}
[One M]
{s : Set α}
{t : Set α}
{f : α → M}
{g : α → M}
{l : Filter α}
(hf : f =ᶠ[l ⊓ Filter.principal s] g)
(hs : s =ᶠ[l] t)
:
Set.mulIndicator s f =ᶠ[l] Set.mulIndicator t g
theorem
indicator_union_eventuallyEq
{α : Type u_1}
{M : Type u_3}
[AddMonoid M]
{s : Set α}
{t : Set α}
{f : α → M}
{l : Filter α}
(h : ∀ᶠ (a : α) in l, a ∉ s ∩ t)
:
Set.indicator (s ∪ t) f =ᶠ[l] Set.indicator s f + Set.indicator t f
theorem
mulIndicator_union_eventuallyEq
{α : Type u_1}
{M : Type u_3}
[Monoid M]
{s : Set α}
{t : Set α}
{f : α → M}
{l : Filter α}
(h : ∀ᶠ (a : α) in l, a ∉ s ∩ t)
:
Set.mulIndicator (s ∪ t) f =ᶠ[l] Set.mulIndicator s f * Set.mulIndicator t f
theorem
indicator_eventuallyLE_indicator
{α : Type u_1}
{β : Type u_2}
[Zero β]
[Preorder β]
{s : Set α}
{f : α → β}
{g : α → β}
{l : Filter α}
(h : f ≤ᶠ[l ⊓ Filter.principal s] g)
:
Set.indicator s f ≤ᶠ[l] Set.indicator s g
theorem
mulIndicator_eventuallyLE_mulIndicator
{α : Type u_1}
{β : Type u_2}
[One β]
[Preorder β]
{s : Set α}
{f : α → β}
{g : α → β}
{l : Filter α}
(h : f ≤ᶠ[l ⊓ Filter.principal s] g)
:
Set.mulIndicator s f ≤ᶠ[l] Set.mulIndicator s g
theorem
Monotone.indicator_eventuallyEq_iUnion
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[Preorder ι]
[Zero β]
(s : ι → Set α)
(hs : Monotone s)
(f : α → β)
(a : α)
:
(fun (i : ι) => Set.indicator (s i) f a) =ᶠ[Filter.atTop] fun (x : ι) => Set.indicator (⋃ (i : ι), s i) f a
theorem
Monotone.mulIndicator_eventuallyEq_iUnion
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[Preorder ι]
[One β]
(s : ι → Set α)
(hs : Monotone s)
(f : α → β)
(a : α)
:
(fun (i : ι) => Set.mulIndicator (s i) f a) =ᶠ[Filter.atTop] fun (x : ι) => Set.mulIndicator (⋃ (i : ι), s i) 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 : ι) => Set.indicator (s i) f a) Filter.atTop (pure (Set.indicator (⋃ (i : ι), s i) f a))
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 : ι) => Set.mulIndicator (s i) f a) Filter.atTop (pure (Set.mulIndicator (⋃ (i : ι), s i) f a))
theorem
Antitone.indicator_eventuallyEq_iInter
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[Preorder ι]
[Zero β]
(s : ι → Set α)
(hs : Antitone s)
(f : α → β)
(a : α)
:
(fun (i : ι) => Set.indicator (s i) f a) =ᶠ[Filter.atTop] fun (x : ι) => Set.indicator (⋂ (i : ι), s i) f a
theorem
Antitone.mulIndicator_eventuallyEq_iInter
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[Preorder ι]
[One β]
(s : ι → Set α)
(hs : Antitone s)
(f : α → β)
(a : α)
:
(fun (i : ι) => Set.mulIndicator (s i) f a) =ᶠ[Filter.atTop] fun (x : ι) => Set.mulIndicator (⋂ (i : ι), s i) 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 : ι) => Set.indicator (s i) f a) Filter.atTop (pure (Set.indicator (⋂ (i : ι), s i) 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 : ι) => Set.mulIndicator (s i) f a) Filter.atTop (pure (Set.mulIndicator (⋂ (i : ι), s i) f a))
theorem
indicator_biUnion_finset_eventuallyEq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[Zero β]
(s : ι → Set α)
(f : α → β)
(a : α)
:
(fun (n : Finset ι) => Set.indicator (⋃ i ∈ n, s i) f a) =ᶠ[Filter.atTop] fun (x : Finset ι) =>
Set.indicator (Set.iUnion s) f a
theorem
mulIndicator_biUnion_finset_eventuallyEq
{α : Type u_1}
{β : Type u_2}
{ι : Type u_5}
[One β]
(s : ι → Set α)
(f : α → β)
(a : α)
:
(fun (n : Finset ι) => Set.mulIndicator (⋃ i ∈ n, s i) f a) =ᶠ[Filter.atTop] fun (x : Finset ι) =>
Set.mulIndicator (Set.iUnion s) 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 ι) => Set.indicator (⋃ i ∈ n, s i) f a) Filter.atTop
(pure (Set.indicator (Set.iUnion s) 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 ι) => Set.mulIndicator (⋃ i ∈ n, s i) f a) Filter.atTop
(pure (Set.mulIndicator (Set.iUnion s) f a))
theorem
Filter.EventuallyEq.indicator
{α : Type u_1}
{β : Type u_2}
[Zero β]
{l : Filter α}
{f : α → β}
{g : α → β}
{s : Set α}
(hfg : f =ᶠ[l] g)
:
Set.indicator s f =ᶠ[l] Set.indicator s g
theorem
Filter.EventuallyEq.mulIndicator
{α : Type u_1}
{β : Type u_2}
[One β]
{l : Filter α}
{f : α → β}
{g : α → β}
{s : Set α}
(hfg : f =ᶠ[l] g)
:
Set.mulIndicator s f =ᶠ[l] Set.mulIndicator s g
theorem
Filter.EventuallyEq.of_indicator
{α : Type u_1}
{β : Type u_2}
[Zero β]
{l : Filter α}
{f : α → β}
(hf : ∀ᶠ (x : α) in l, f x ≠ 0)
{s : Set α}
{t : Set α}
(h : Set.indicator s f =ᶠ[l] Set.indicator t f)
:
theorem
Filter.EventuallyEq.of_mulIndicator
{α : Type u_1}
{β : Type u_2}
[One β]
{l : Filter α}
{f : α → β}
(hf : ∀ᶠ (x : α) in l, f x ≠ 1)
{s : Set α}
{t : Set α}
(h : Set.mulIndicator s f =ᶠ[l] Set.mulIndicator t f)
:
theorem
Filter.EventuallyEq.of_indicator_const
{α : Type u_1}
{β : Type u_2}
[Zero β]
{l : Filter α}
{c : β}
(hc : c ≠ 0)
{s : Set α}
{t : Set α}
(h : (Set.indicator s fun (x : α) => c) =ᶠ[l] Set.indicator t fun (x : α) => c)
:
theorem
Filter.EventuallyEq.of_mulIndicator_const
{α : Type u_1}
{β : Type u_2}
[One β]
{l : Filter α}
{c : β}
(hc : c ≠ 1)
{s : Set α}
{t : Set α}
(h : (Set.mulIndicator s fun (x : α) => c) =ᶠ[l] Set.mulIndicator t fun (x : α) => c)
: