Documentation

Mathlib.Order.Filter.IndicatorFunction

Indicator function and filters #

Properties of indicator functions involving =ᶠ and ≤ᶠ≤ᶠ.

Tags #

indicator, characteristic, filter

theorem indicator_eventuallyEq {α : Type u_1} {M : Type u_2} [inst : Zero M] {s : Set α} {t : Set α} {f : αM} {g : αM} {l : Filter α} (hf : f =ᶠ[l Filter.principal s] g) (hs : s =ᶠ[l] t) :
theorem indicator_union_eventuallyEq {α : Type u_1} {M : Type u_2} [inst : AddMonoid M] {s : Set α} {t : Set α} {f : αM} {l : Filter α} (h : Filter.Eventually (fun a => ¬a s t) l) :
theorem indicator_eventuallyLE_indicator {α : Type u_1} {β : Type u_2} [inst : Zero β] [inst : Preorder β] {s : Set α} {f : αβ} {g : αβ} {l : Filter α} (h : f ≤ᶠ[l Filter.principal s] g) :
theorem Monotone.tendsto_indicator {α : Type u_3} {β : Type u_2} {ι : Type u_1} [inst : Preorder ι] [inst : Zero β] (s : ιSet α) (hs : Monotone s) (f : αβ) (a : α) :
Filter.Tendsto (fun i => Set.indicator (s i) f a) Filter.atTop (pure (Set.indicator (Set.unionᵢ fun i => s i) f a))
theorem Antitone.tendsto_indicator {α : Type u_3} {β : Type u_2} {ι : Type u_1} [inst : Preorder ι] [inst : Zero β] (s : ιSet α) (hs : Antitone s) (f : αβ) (a : α) :
Filter.Tendsto (fun i => Set.indicator (s i) f a) Filter.atTop (pure (Set.indicator (Set.interᵢ fun i => s i) f a))
theorem tendsto_indicator_bunionᵢ_finset {α : Type u_3} {β : Type u_2} {ι : Type u_1} [inst : Zero β] (s : ιSet α) (f : αβ) (a : α) :
Filter.Tendsto (fun n => Set.indicator (Set.unionᵢ fun i => Set.unionᵢ fun h => s i) f a) Filter.atTop (pure (Set.indicator (Set.unionᵢ s) f a))
theorem Filter.EventuallyEq.support {α : Type u_2} {β : Type u_1} [inst : Zero β] {f : αβ} {g : αβ} {l : Filter α} (h : f =ᶠ[l] g) :
theorem Filter.EventuallyEq.indicator {α : Type u_2} {β : Type u_1} [inst : Zero β] {l : Filter α} {f : αβ} {g : αβ} {s : Set α} (hfg : f =ᶠ[l] g) :
theorem Filter.EventuallyEq.indicator_zero {α : Type u_2} {β : Type u_1} [inst : Zero β] {l : Filter α} {f : αβ} {s : Set α} (hf : f =ᶠ[l] 0) :