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 : Filter ι) {β : Type u_4} {p : ι → Prop} [DecidablePred p] {q : Prop} [Decidable q] {a : β} {b : β} {F : Filter β} {G : Filter β} (haG : {a}ᶜ ∈ G) (hbF : {b}ᶜ ∈ F) (haF : Filter.principal {a} ≤ F) (hbG : Filter.principal {b} ≤ 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 β] [TopologicalSpace β] {ι : Type u_3} (L : Filter ι) {As : ι → Set α} (b : β) (nhd_b : {0}ᶜ ∈ nhds b) (nhd_o : {b}ᶜ ∈ nhds 0) (x : α) : Filter.Tendsto (fun (i : ι) => (As i).indicator (fun (x : α) => b) x) L (nhds (A.indicator (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 β] [TopologicalSpace β] {ι : Type u_3} (L : Filter ι) {As : ι → Set α} (b : β) (nhd_b : {0}ᶜ ∈ nhds b) (nhd_o : {b}ᶜ ∈ nhds 0) : Filter.Tendsto (fun (i : ι) => (As i).indicator fun (x : α) => b) L (nhds (A.indicator 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 β] [TopologicalSpace β] {ι : Type u_3} (L : Filter ι) {As : ι → Set α} [T1Space β] (b : β) [NeZero b] (x : α) : Filter.Tendsto (fun (i : ι) => (As i).indicator (fun (x : α) => b) x) L (nhds (A.indicator (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 β] [TopologicalSpace β] {ι : Type u_3} (L : Filter ι) {As : ι → Set α} [T1Space β] (b : β) [NeZero b] : Filter.Tendsto (fun (i : ι) => (As i).indicator fun (x : α) => b) L (nhds (A.indicator 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 β] [TopologicalSpace β] {ι : Type u_3} (L : Filter ι) {As : ι → Set α} (b : β) (nhd_b : {0}ᶜ ∈ nhds b) (nhd_o : {b}ᶜ ∈ nhds 0) : Filter.Tendsto (fun (i : ι) => (As i).indicator fun (x : α) => b) L (nhds (A.indicator 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 β] [TopologicalSpace β] {ι : Type u_3} (L : Filter ι) {As : ι → Set α} [T1Space β] (b : β) [NeZero b] : Filter.Tendsto (fun (i : ι) => (As i).indicator fun (x : α) => b) L (nhds (A.indicator fun (x : α) => b)) ↔ Filter.Tendsto As L (Filter.pi fun (x : α) => pure (x ∈ A))