# Indicator function and filters #

Properties of additive and multiplicative indicator functions involving `=ᶠ` and `≤ᶠ`.

## Tags #

indicator, characteristic, filter

source
theorem mulIndicator_eventuallyEq {α : Type u_1} {M : Type u_3} [One M] {s t : Set α} {f g : α → M} {l : Filter α} (hf : f =ᶠ[l ⊓ Filter.principal s] g) (hs : s =ᶠ[l] t) :
s.mulIndicator f =ᶠ[l] t.mulIndicator g
source
theorem indicator_eventuallyEq {α : Type u_1} {M : Type u_3} [Zero M] {s t : Set α} {f g : α → M} {l : Filter α} (hf : f =ᶠ[l ⊓ Filter.principal s] g) (hs : s =ᶠ[l] t) :
s.indicator f =ᶠ[l] t.indicator g
source
theorem mulIndicator_union_eventuallyEq {α : Type u_1} {M : Type u_3} [Monoid M] {s t : Set α} {f : α → M} {l : Filter α} (h : ∀ᶠ (a : α) in l, a ∉ s ∩ t) :
(s ∪ t).mulIndicator f =ᶠ[l] s.mulIndicator f * t.mulIndicator f
source
theorem indicator_union_eventuallyEq {α : Type u_1} {M : Type u_3} [AddMonoid 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 mulIndicator_eventuallyLE_mulIndicator {α : Type u_1} {β : Type u_2} [One β] [Preorder β] {s : Set α} {f g : α → β} {l : Filter α} (h : f ≤ᶠ[l ⊓ Filter.principal s] g) :
s.mulIndicator f ≤ᶠ[l] s.mulIndicator g
source
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) :
s.indicator f ≤ᶠ[l] s.indicator g
source
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 : ι) => (s i).mulIndicator f a) =ᶠ[Filter.atTop] fun (x : ι) => (⋃ (i : ι), s i).mulIndicator f a
source
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 : ι) => (s i).indicator f a) =ᶠ[Filter.atTop] fun (x : ι) => (⋃ (i : ι), s i).indicator f a
source
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))
source
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))
source
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 : ι) => (s i).mulIndicator f a) =ᶠ[Filter.atTop] fun (x : ι) => (⋂ (i : ι), s i).mulIndicator f a
source
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 : ι) => (s i).indicator f a) =ᶠ[Filter.atTop] fun (x : ι) => (⋂ (i : ι), s i).indicator f a
source
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))
source
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))
source
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
source
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
source
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))
source
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))
source
theorem Filter.EventuallyEq.mulSupport {α : Type u_1} {β : Type u_2} [One β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) :
Function.mulSupport f =ᶠ[l] Function.mulSupport g
source
theorem Filter.EventuallyEq.support {α : Type u_1} {β : Type u_2} [Zero β] {f g : α → β} {l : Filter α} (h : f =ᶠ[l] g) :
Function.support f =ᶠ[l] Function.support g
source
theorem Filter.EventuallyEq.mulIndicator {α : Type u_1} {β : Type u_2} [One β] {l : Filter α} {f g : α → β} {s : Set α} (hfg : f =ᶠ[l] g) :
s.mulIndicator f =ᶠ[l] s.mulIndicator g
source
theorem Filter.EventuallyEq.indicator {α : Type u_1} {β : Type u_2} [Zero β] {l : Filter α} {f g : α → β} {s : Set α} (hfg : f =ᶠ[l] g) :
s.indicator f =ᶠ[l] s.indicator g
source
theorem Filter.EventuallyEq.mulIndicator_one {α : Type u_1} {β : Type u_2} [One β] {l : Filter α} {f : α → β} {s : Set α} (hf : f =ᶠ[l] 1) :
s.mulIndicator f =ᶠ[l] 1
source
theorem Filter.EventuallyEq.indicator_zero {α : Type u_1} {β : Type u_2} [Zero β] {l : Filter α} {f : α → β} {s : Set α} (hf : f =ᶠ[l] 0) :
s.indicator f =ᶠ[l] 0
source
theorem Filter.EventuallyEq.of_mulIndicator {α : Type u_1} {β : Type u_2} [One β] {l : Filter α} {f : α → β} (hf : ∀ᶠ (x : α) in l, f x ≠ 1) {s t : Set α} (h : s.mulIndicator f =ᶠ[l] t.mulIndicator f) :
s =ᶠ[l] t
source
theorem Filter.EventuallyEq.of_indicator {α : Type u_1} {β : Type u_2} [Zero β] {l : Filter α} {f : α → β} (hf : ∀ᶠ (x : α) in l, f x ≠ 0) {s t : Set α} (h : s.indicator f =ᶠ[l] t.indicator f) :
s =ᶠ[l] t
source
theorem Filter.EventuallyEq.of_mulIndicator_const {α : Type u_1} {β : Type u_2} [One β] {l : Filter α} {c : β} (hc : c ≠ 1) {s t : Set α} (h : (s.mulIndicator fun (x : α) => c) =ᶠ[l] t.mulIndicator fun (x : α) => c) :
s =ᶠ[l] t
source
theorem Filter.EventuallyEq.of_indicator_const {α : Type u_1} {β : Type u_2} [Zero β] {l : Filter α} {c : β} (hc : c ≠ 0) {s t : Set α} (h : (s.indicator fun (x : α) => c) =ᶠ[l] t.indicator fun (x : α) => c) :
s =ᶠ[l] t
source
theorem Filter.mulIndicator_const_eventuallyEq {α : Type u_1} {β : Type u_2} [One β] {l : Filter α} {c : β} (hc : c ≠ 1) {s t : Set α} :
((s.mulIndicator fun (x : α) => c) =ᶠ[l] t.mulIndicator fun (x : α) => c) ↔ s =ᶠ[l] t
source
theorem Filter.indicator_const_eventuallyEq {α : Type u_1} {β : Type u_2} [Zero β] {l : Filter α} {c : β} (hc : c ≠ 0) {s t : Set α} :
((s.indicator fun (x : α) => c) =ᶠ[l] t.indicator fun (x : α) => c) ↔ s =ᶠ[l] t