# Pointwise convergence of indicator functions #

In this file, we prove the equivalence of three different ways to phrase that the indicator functions of sets converge pointwise.

## Main results #

For A a set, (Asᵢ) an indexed collection of sets, under mild conditions, the following are equivalent:

(a) the indicator functions of Asᵢ tend to the indicator function of A pointwise;

(b) for every x, we eventually have that x ∈ Asᵢ holds iff x ∈ A holds;

(c) Tendsto As _ <| Filter.pi (pure <| · ∈ A).

The results stating these in the case when the indicators take values in a Fréchet space are:

• tendsto_indicator_const_iff_forall_eventually is the equivalence (a) ↔ (b);
• tendsto_indicator_const_iff_tendsto_pi_pure is the equivalence (a) ↔ (c).
theorem tendsto_ite {ι : Type u_3} (L : ) {β : Type u_4} {p : ιProp} [] {q : Prop} [] {a : β} {b : β} {F : } {G : } (haG : {a} G) (hbF : {b} F) (haF : F) (hbG : G) :
Filter.Tendsto (fun (i : ι) => if p i then a else b) L (if q then F else G) ∀ᶠ (i : ι) in L, p i q
theorem tendsto_indicator_const_apply_iff_eventually' {α : Type u_1} {A : Set α} {β : Type u_2} [Zero β] [] {ι : Type u_3} (L : ) {As : ιSet α} (b : β) (nhd_b : {0} nhds b) (nhd_o : {b} nhds 0) (x : α) :
Filter.Tendsto (fun (i : ι) => Set.indicator (As i) (fun (x : α) => b) x) L (nhds (Set.indicator A (fun (x : α) => b) x)) ∀ᶠ (i : ι) in L, x As i x A
theorem tendsto_indicator_const_iff_forall_eventually' {α : Type u_1} {A : Set α} {β : Type u_2} [Zero β] [] {ι : Type u_3} (L : ) {As : ιSet α} (b : β) (nhd_b : {0} nhds b) (nhd_o : {b} nhds 0) :
Filter.Tendsto (fun (i : ι) => Set.indicator (As i) fun (x : α) => b) L (nhds (Set.indicator A fun (x : α) => b)) ∀ (x : α), ∀ᶠ (i : ι) in L, x As i x A
@[simp]
theorem tendsto_indicator_const_apply_iff_eventually {α : Type u_1} {A : Set α} {β : Type u_2} [Zero β] [] {ι : Type u_3} (L : ) {As : ιSet α} [] (b : β) [] (x : α) :
Filter.Tendsto (fun (i : ι) => Set.indicator (As i) (fun (x : α) => b) x) L (nhds (Set.indicator A (fun (x : α) => b) x)) ∀ᶠ (i : ι) in L, x As i x A

The indicator functions of Asᵢ evaluated at x tend to the indicator function of A evaluated at x if and only if we eventually have the equivalence x ∈ Asᵢ ↔ x ∈ A.

@[simp]
theorem tendsto_indicator_const_iff_forall_eventually {α : Type u_1} {A : Set α} {β : Type u_2} [Zero β] [] {ι : Type u_3} (L : ) {As : ιSet α} [] (b : β) [] :
Filter.Tendsto (fun (i : ι) => Set.indicator (As i) fun (x : α) => b) L (nhds (Set.indicator A fun (x : α) => b)) ∀ (x : α), ∀ᶠ (i : ι) in L, x As i x A

The indicator functions of Asᵢ tend to the indicator function of A pointwise if and only if for every x, we eventually have the equivalence x ∈ Asᵢ ↔ x ∈ A.

theorem tendsto_indicator_const_iff_tendsto_pi_pure' {α : Type u_1} {A : Set α} {β : Type u_2} [Zero β] [] {ι : Type u_3} (L : ) {As : ιSet α} (b : β) (nhd_b : {0} nhds b) (nhd_o : {b} nhds 0) :
Filter.Tendsto (fun (i : ι) => Set.indicator (As i) fun (x : α) => b) L (nhds (Set.indicator A fun (x : α) => b)) Filter.Tendsto As L (Filter.pi fun (x : α) => pure (x A))
theorem tendsto_indicator_const_iff_tendsto_pi_pure {α : Type u_1} {A : Set α} {β : Type u_2} [Zero β] [] {ι : Type u_3} (L : ) {As : ιSet α} [] (b : β) [] :
Filter.Tendsto (fun (i : ι) => Set.indicator (As i) fun (x : α) => b) L (nhds (Set.indicator A fun (x : α) => b)) Filter.Tendsto As L (Filter.pi fun (x : α) => pure (x A))