Documentation

Mathlib.Order.Filter.IndicatorFunction

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, as 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, as 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 ι) => (⋃ in, 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 ι) => (⋃ in, 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 ι) => (⋃ in, 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 ι) => (⋃ in, 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) :
theorem Filter.EventuallyEq.mulSupport {α : Type u_1} {β : Type u_2} [One β] {f : αβ} {g : αβ} {l : Filter α} (h : f =ᶠ[l] 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