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) : s.indicator f =ᶠ[l] 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 : f =ᶠ[l ⊓ Filter.principal s] g) (hs : s =ᶠ[l] t) : s.mulIndicator f =ᶠ[l] t.mulIndicator 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) : (s ∪ t).indicator f =ᶠ[l] s.indicator f + t.indicator 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) : (s ∪ t).mulIndicator f =ᶠ[l] s.mulIndicator f * t.mulIndicator 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) : s.indicator f ≤ᶠ[l] s.indicator 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) : s.mulIndicator f ≤ᶠ[l] s.mulIndicator 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 : ι) => (s i).indicator f a) =ᶠ[Filter.atTop] fun (x : ι) => (⋃ (i : ι), s i).indicator 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 : ι) => (s i).mulIndicator f a) =ᶠ[Filter.atTop] fun (x : ι) => (⋃ (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 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 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

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

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 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 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 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 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 : f =ᶠ[l] g) : Function.support f =ᶠ[l] Function.support g

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

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

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

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

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

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 : s.indicator f =ᶠ[l] t.indicator f) : s =ᶠ[l] t

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 : s.mulIndicator f =ᶠ[l] t.mulIndicator f) : s =ᶠ[l] t

theorem Filter.EventuallyEq.of_indicator_const {α : Type u_1} {β : Type u_2} [Zero β] {l : Filter α} {c : β} (hc : c ≠ 0) {s : Set α} {t : Set α} (h : (s.indicator fun (x : α) => c) =ᶠ[l] t.indicator fun (x : α) => c) : s =ᶠ[l] t

theorem Filter.EventuallyEq.of_mulIndicator_const {α : Type u_1} {β : Type u_2} [One β] {l : Filter α} {c : β} (hc : c ≠ 1) {s : Set α} {t : Set α} (h : (s.mulIndicator fun (x : α) => c) =ᶠ[l] t.mulIndicator fun (x : α) => c) : s =ᶠ[l] t

theorem Filter.indicator_const_eventuallyEq {α : Type u_1} {β : Type u_2} [Zero β] {l : Filter α} {c : β} (hc : c ≠ 0) {s : Set α} {t : Set α} : ((s.indicator fun (x : α) => c) =ᶠ[l] t.indicator fun (x : α) => c) ↔ s =ᶠ[l] t

theorem Filter.mulIndicator_const_eventuallyEq {α : Type u_1} {β : Type u_2} [One β] {l : Filter α} {c : β} (hc : c ≠ 1) {s : Set α} {t : Set α} : ((s.mulIndicator fun (x : α) => c) =ᶠ[l] t.mulIndicator fun (x : α) => c) ↔ s =ᶠ[l] t