-
Notifications
You must be signed in to change notification settings - Fork 307
/
IndicatorConstPointwise.lean
123 lines (104 loc) · 5.81 KB
/
IndicatorConstPointwise.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
/-
Copyright (c) 2023 Kalle Kytölä. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kalle Kytölä
-/
import Mathlib.Algebra.Function.Indicator
import Mathlib.Topology.Separation
/-!
# 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).
-/
open Filter Topology
variable {α : Type*} {A : Set α}
variable {β : Type*} [Zero β] [TopologicalSpace β]
variable {ι : Type*} (L : Filter ι) {As : ι → Set α}
lemma tendsto_ite {β : Type*} {p : ι → Prop} [DecidablePred p] {q : Prop} [Decidable q]
{a b : β} {F G : Filter β}
(haG : {a}ᶜ ∈ G) (hbF : {b}ᶜ ∈ F) (haF : principal {a} ≤ F) (hbG : principal {b} ≤ G) :
Tendsto (fun i ↦ if p i then a else b) L (if q then F else G) ↔ ∀ᶠ i in L, p i ↔ q := by
constructor <;> intro h
· by_cases hq : q
· simp only [hq, ite_true] at h
filter_upwards [mem_map.mp (h hbF)] with i hi
simp only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
ite_eq_right_iff, not_forall, exists_prop] at hi
tauto
· simp only [hq, ite_false] at h
filter_upwards [mem_map.mp (h haG)] with i hi
simp only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
ite_eq_left_iff, not_forall, exists_prop] at hi
tauto
· have obs : (fun _ ↦ if q then a else b) =ᶠ[L] (fun i ↦ if p i then a else b) := by
filter_upwards [h] with i hi
simp only [hi]
apply Tendsto.congr' obs
by_cases hq : q
· simp only [hq, iff_true, ite_true]
apply le_trans _ haF
simp only [principal_singleton, le_pure_iff, mem_map, Set.mem_singleton_iff,
Set.preimage_const_of_mem, univ_mem]
· simp only [hq, ite_false]
apply le_trans _ hbG
simp only [principal_singleton, le_pure_iff, mem_map, Set.mem_singleton_iff,
Set.preimage_const_of_mem, univ_mem]
lemma tendsto_indicator_const_apply_iff_eventually' (b : β)
(nhd_b : {0}ᶜ ∈ 𝓝 b) (nhd_o : {b}ᶜ ∈ 𝓝 0) (x : α) :
Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b) x) L (𝓝 (A.indicator (fun (_ : α) ↦ b) x))
↔ ∀ᶠ i in L, (x ∈ As i ↔ x ∈ A) := by
classical
have heart := @tendsto_ite ι L β (fun i ↦ x ∈ As i) _ (x ∈ A) _ b 0 (𝓝 b) (𝓝 (0 : β))
nhd_o nhd_b ?_ ?_
convert heart
· by_cases hxA : x ∈ A <;> simp [hxA]
· simp only [principal_singleton, le_def, mem_pure]
exact fun s s_nhd ↦ mem_of_mem_nhds s_nhd
· simp only [principal_singleton, le_def, mem_pure]
exact fun s s_nhd ↦ mem_of_mem_nhds s_nhd
lemma tendsto_indicator_const_iff_forall_eventually'
(b : β) (nhd_b : {0}ᶜ ∈ 𝓝 b) (nhd_o : {b}ᶜ ∈ 𝓝 0) :
Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b)) L (𝓝 (A.indicator (fun (_ : α) ↦ b)))
↔ ∀ x, ∀ᶠ i in L, (x ∈ As i ↔ x ∈ A) := by
simp_rw [tendsto_pi_nhds]
apply forall_congr'
exact tendsto_indicator_const_apply_iff_eventually' L b nhd_b nhd_o
/-- 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] lemma tendsto_indicator_const_apply_iff_eventually [T1Space β] (b : β) [NeZero b]
(x : α) :
Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b) x) L (𝓝 (A.indicator (fun (_ : α) ↦ b) x))
↔ ∀ᶠ i in L, (x ∈ As i ↔ x ∈ A) := by
apply tendsto_indicator_const_apply_iff_eventually' _ b
· simp only [compl_singleton_mem_nhds_iff, ne_eq, NeZero.ne, not_false_eq_true]
· simp only [compl_singleton_mem_nhds_iff, ne_eq, (NeZero.ne b).symm, not_false_eq_true]
/-- 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`. -/
@[simp] lemma tendsto_indicator_const_iff_forall_eventually [T1Space β] (b : β) [NeZero b] :
Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b)) L (𝓝 (A.indicator (fun (_ : α) ↦ b)))
↔ ∀ x, ∀ᶠ i in L, (x ∈ As i ↔ x ∈ A) := by
apply tendsto_indicator_const_iff_forall_eventually' _ b
· simp only [compl_singleton_mem_nhds_iff, ne_eq, NeZero.ne, not_false_eq_true]
· simp only [compl_singleton_mem_nhds_iff, ne_eq, (NeZero.ne b).symm, not_false_eq_true]
lemma tendsto_indicator_const_iff_tendsto_pi_pure'
(b : β) (nhd_b : {0}ᶜ ∈ 𝓝 b) (nhd_o : {b}ᶜ ∈ 𝓝 0) :
Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b)) L (𝓝 (A.indicator (fun (_ : α) ↦ b)))
↔ (Tendsto As L <| Filter.pi (pure <| · ∈ A)) := by
rw [tendsto_indicator_const_iff_forall_eventually' _ b nhd_b nhd_o, tendsto_pi]
simp_rw [tendsto_pure]
aesop
lemma tendsto_indicator_const_iff_tendsto_pi_pure [T1Space β] (b : β) [NeZero b] :
Tendsto (fun i ↦ (As i).indicator (fun (_ : α) ↦ b)) L (𝓝 (A.indicator (fun (_ : α) ↦ b)))
↔ (Tendsto As L <| Filter.pi (pure <| · ∈ A)) := by
rw [tendsto_indicator_const_iff_forall_eventually _ b, tendsto_pi]
simp_rw [tendsto_pure]
aesop