Skip to content

Commit

Permalink
chore(topology/algebra/ordered): move code, add missing lemmas (#5481)
Browse files Browse the repository at this point in the history 
* merge two sections about `linear_ordered_add_comm_group`;
* add missing lemmas about limits of `f * g` when one of `f`, `g` tends to `-∞`, and another tends to a positive or negative constant;
* drop `neg_preimage_closure` in favor of the new `neg_closure` in `topology/algebra/group`.
  • Loading branch information
@urkud
urkud committed Dec 30, 2020
1 parent 5e86589 commit 8545aa6
Show file tree
Hide file tree
Showing 2 changed files with 134 additions and 139 deletions.
19 changes: 6 additions & 13 deletions src/topology/algebra/group.lean
View file
Expand Up @@ -174,14 +174,14 @@ protected def homeomorph.inv : G ≃ₜ G :=

@[to_additive]
lemma nhds_one_symm : comap has_inv.inv (𝓝 (1 : G)) = 𝓝 (1 : G) :=
begin
have lim : tendsto has_inv.inv (𝓝 (1 : G)) (𝓝 1),
{ simpa only [one_inv] using tendsto_inv (1 : G) },
exact comap_eq_of_inverse _ inv_involutive.comp_self lim lim,
end
((homeomorph.inv G).comap_nhds_eq _).trans (congr_arg nhds one_inv)

variable {G}

@[to_additive]
lemma inv_closure (s : set G) : (closure s)⁻¹ = closure s⁻¹ :=
(homeomorph.inv G).preimage_closure s

@[to_additive exists_nhds_half_neg]
lemma exists_nhds_split_inv {s : set G} (hs : s ∈ 𝓝 (1 : G)) :
∃ V ∈ 𝓝 (1 : G), ∀ (v ∈ V) (w ∈ V), v / w ∈ s :=
Expand All @@ -192,14 +192,7 @@ by simpa only [div_eq_mul_inv, nhds_prod_eq, mem_prod_self_iff, prod_subset_iff,

@[to_additive]
lemma nhds_translation_mul_inv (x : G) : comap (λ y : G, y * x⁻¹) (𝓝 1) = 𝓝 x :=
begin
refine comap_eq_of_inverse (λ y : G, y * x) _ _ _,
{ funext x, simp },
{ rw ← mul_right_inv x,
exact tendsto_id.mul tendsto_const_nhds },
{ suffices : tendsto (λ y : G, y * x) (𝓝 1) (𝓝 (1 * x)), { simpa },
exact tendsto_id.mul tendsto_const_nhds }
end
((homeomorph.mul_right x⁻¹).comap_nhds_eq 1).trans $ show 𝓝 (1 * x⁻¹⁻¹) = 𝓝 x, by simp

@[to_additive]
lemma topological_group.ext {G : Type*} [group G] {t t' : topological_space G}
Expand Down
254 changes: 128 additions & 126 deletions src/topology/algebra/ordered.lean
View file
Expand Up @@ -1353,6 +1353,95 @@ section linear_ordered_add_comm_group
variables [topological_space α] [linear_ordered_add_comm_group α] [order_topology α]
variables {l : filter β} {f g : β → α}

local notation `|` x `|` := abs x

lemma nhds_eq_infi_abs_sub (a : α) : 𝓝 a = (⨅r>0, 𝓟 {b | |a - b| < r}) :=
begin
simp only [le_antisymm_iff, nhds_eq_order, le_inf_iff, le_infi_iff, le_principal_iff, mem_Ioi,
mem_Iio, abs_sub_lt_iff, @sub_lt_iff_lt_add _ _ _ _ a, @sub_lt _ _ a, set_of_and],
refine ⟨_, _, _⟩,
{ intros ε ε0,
exact inter_mem_inf_sets
(mem_infi_sets (a - ε) $ mem_infi_sets (sub_lt_self a ε0) (mem_principal_self _))
(mem_infi_sets (ε + a) $ mem_infi_sets (by simpa) (mem_principal_self _)) },
{ intros b hb,
exact mem_infi_sets (a - b) (mem_infi_sets (sub_pos.2 hb) (by simp [Ioi])) },
{ intros b hb,
exact mem_infi_sets (b - a) (mem_infi_sets (sub_pos.2 hb) (by simp [Iio])) }
end

lemma order_topology_of_nhds_abs {α : Type*} [topological_space α] [linear_ordered_add_comm_group α]
(h_nhds : ∀a:α, 𝓝 a = (⨅r>0, 𝓟 {b | |a - b| < r})) : order_topology α :=
begin
refine ⟨eq_of_nhds_eq_nhds $ λ a, _⟩,
rw [h_nhds],
letI := preorder.topology α, letI : order_topology α := ⟨rfl⟩,
exact (nhds_eq_infi_abs_sub a).symm
end

lemma linear_ordered_add_comm_group.tendsto_nhds {x : filter β} {a : α} :
tendsto f x (𝓝 a) ↔ ∀ ε > (0 : α), ∀ᶠ b in x, |f b - a| < ε :=
by simp [nhds_eq_infi_abs_sub, abs_sub a]

lemma eventually_abs_sub_lt (a : α) {ε : α} (hε : 0 < ε) : ∀ᶠ x in 𝓝 a, |x - a| < ε :=
(nhds_eq_infi_abs_sub a).symm ▸ mem_infi_sets ε
(mem_infi_sets hε $ by simp only [abs_sub, mem_principal_self])

@[priority 100] -- see Note [lower instance priority]
instance linear_ordered_add_comm_group.topological_add_group : topological_add_group α :=
{ continuous_add :=
begin
refine continuous_iff_continuous_at.2 _,
rintro ⟨a, b⟩,
refine linear_ordered_add_comm_group.tendsto_nhds.2 (λ ε ε0, _),
rcases dense_or_discrete 0 ε with (⟨δ, δ0, δε⟩|⟨h₁, h₂⟩),
{ -- If there exists `δ ∈ (0, ε)`, then we choose `δ`-nhd of `a` and `(ε-δ)`-nhd of `b`
filter_upwards [prod_mem_nhds_sets (eventually_abs_sub_lt a δ0)
(eventually_abs_sub_lt b (sub_pos.2 δε))],
rintros ⟨x, y⟩ ⟨hx : |x - a| < δ, hy : |y - b| < ε - δ⟩,
rw [add_sub_comm],
calc |x - a + (y - b)| ≤ |x - a| + |y - b| : abs_add _ _
... < δ + (ε - δ) : add_lt_add hx hy
... = ε : add_sub_cancel'_right _ _ },
{ -- Otherewise `ε`-nhd of each point `a` is `{a}`
have hε : ∀ {x y}, abs (x - y) < ε → x = y,
{ intros x y h,
simpa [sub_eq_zero] using h₂ _ h },
filter_upwards [prod_mem_nhds_sets (eventually_abs_sub_lt a ε0)
(eventually_abs_sub_lt b ε0)],
rintros ⟨x, y⟩ ⟨hx : |x - a| < ε, hy : |y - b| < ε⟩,
simpa [hε hx, hε hy] }
end,
continuous_neg := continuous_iff_continuous_at.2 $ λ a,
linear_ordered_add_comm_group.tendsto_nhds.2 $ λ ε ε0,
(eventually_abs_sub_lt a ε0).mono $ λ x hx, by rwa [neg_sub_neg, abs_sub] }

@[continuity]
lemma continuous_abs : continuous (abs : α → α) := continuous_id.max continuous_neg

lemma filter.tendsto.abs {f : β → α} {a : α} {l : filter β} (h : tendsto f l (𝓝 a)) :
tendsto (λ x, |f x|) l (𝓝 (|a|)) :=
(continuous_abs.tendsto _).comp h

section

variables [topological_space β] {b : β} {a : α} {s : set β}

lemma continuous.abs (h : continuous f) : continuous (λ x, |f x|) := continuous_abs.comp h

lemma continuous_at.abs (h : continuous_at f b) : continuous_at (λ x, |f x|) b := h.abs

lemma continuous_within_at.abs (h : continuous_within_at f s b) :
continuous_within_at (λ x, |f x|) s b := h.abs

lemma continuous_on.abs (h : continuous_on f s) : continuous_on (λ x, |f x|) s :=
λ x hx, (h x hx).abs

lemma tendsto_abs_nhds_within_zero : tendsto (abs : α → α) (𝓝[{0}ᶜ] 0) (𝓝[Ioi 0] 0) :=
(continuous_abs.tendsto' (0 : α) 0 abs_zero).inf $ tendsto_principal_principal.2 $ λ x, abs_pos.2

end

/-- In a linearly ordered additive commutative group with the order topology, if `f` tends to `C`
and `g` tends to `at_top` then `f + g` tends to `at_top`. -/
lemma filter.tendsto.add_at_top {C : α} (hf : tendsto f l (𝓝 C)) (hg : tendsto g l at_top) :
Expand Down Expand Up @@ -1385,11 +1474,9 @@ by { conv in (_ + _) { rw add_comm }, exact hg.add_at_bot hf }
end linear_ordered_add_comm_group

section linear_ordered_field
variables [linear_ordered_field α]
variables [linear_ordered_field α] [topological_space α] [order_topology α]
variables {l : filter β} {f g : β → α}

variables [topological_space α] [order_topology α]

/-- In a linearly ordered field with the order topology, if `f` tends to `at_top` and `g` tends to
a positive constant `C` then `f * g` tends to `at_top`. -/
lemma filter.tendsto.at_top_mul {C : α} (hC : 0 < C) (hf : tendsto f l at_top)
Expand All @@ -1414,17 +1501,45 @@ a negative constant `C` then `f * g` tends to `at_bot`. -/
lemma filter.tendsto.at_top_mul_neg {C : α} (hC : C < 0) (hf : tendsto f l at_top)
(hg : tendsto g l (𝓝 C)) :
tendsto (λ x, (f x * g x)) l at_bot :=
begin
rcases exists_between hC with ⟨C', hCC', hC'0⟩,
refine tendsto_at_bot_mono' _ _ (hf.at_top_mul_neg_const hC'0),
filter_upwards [hg.eventually (gt_mem_nhds hCC'), hf.eventually (eventually_ge_at_top 0)],
exact λ x hg hf, mul_le_mul_of_nonneg_left hg.le hf
end
by simpa only [(∘), neg_mul_eq_mul_neg, neg_neg]
using tendsto_neg_at_top_at_bot.comp (hf.at_top_mul (neg_pos.2 hC) hg.neg)

end linear_ordered_field
/-- In a linearly ordered field with the order topology, if `f` tends to a negative constant `C` and
`g` tends to `at_top` then `f * g` tends to `at_bot`. -/
lemma filter.tendsto.neg_mul_at_top {C : α} (hC : C < 0) (hf : tendsto f l (𝓝 C))
(hg : tendsto g l at_top) :
tendsto (λ x, (f x * g x)) l at_bot :=
by simpa only [mul_comm] using hg.at_top_mul_neg hC hf

section linear_ordered_field
variables [linear_ordered_field α] [topological_space α] [order_topology α]
/-- In a linearly ordered field with the order topology, if `f` tends to `at_bot` and `g` tends to
a positive constant `C` then `f * g` tends to `at_bot`. -/
lemma filter.tendsto.at_bot_mul {C : α} (hC : 0 < C) (hf : tendsto f l at_bot)
(hg : tendsto g l (𝓝 C)) :
tendsto (λ x, (f x * g x)) l at_bot :=
by simpa [(∘)]
using tendsto_neg_at_top_at_bot.comp ((tendsto_neg_at_bot_at_top.comp hf).at_top_mul hC hg)

/-- In a linearly ordered field with the order topology, if `f` tends to `at_bot` and `g` tends to
a negative constant `C` then `f * g` tends to `at_top`. -/
lemma filter.tendsto.at_bot_mul_neg {C : α} (hC : C < 0) (hf : tendsto f l at_bot)
(hg : tendsto g l (𝓝 C)) :
tendsto (λ x, (f x * g x)) l at_top :=
by simpa [(∘)]
using tendsto_neg_at_bot_at_top.comp ((tendsto_neg_at_bot_at_top.comp hf).at_top_mul_neg hC hg)

/-- In a linearly ordered field with the order topology, if `f` tends to a positive constant `C` and
`g` tends to `at_bot` then `f * g` tends to `at_bot`. -/
lemma filter.tendsto.mul_at_bot {C : α} (hC : 0 < C) (hf : tendsto f l (𝓝 C))
(hg : tendsto g l at_bot) :
tendsto (λ x, (f x * g x)) l at_bot :=
by simpa only [mul_comm] using hg.at_bot_mul hC hf

/-- In a linearly ordered field with the order topology, if `f` tends to a negative constant `C` and
`g` tends to `at_bot` then `f * g` tends to `at_top`. -/
lemma filter.tendsto.neg_mul_at_bot {C : α} (hC : C < 0) (hf : tendsto f l (𝓝 C))
(hg : tendsto g l at_bot) :
tendsto (λ x, (f x * g x)) l at_top :=
by simpa only [mul_comm] using hg.at_bot_mul_neg hC hf

/-- The function `x ↦ x⁻¹` tends to `+∞` on the right of `0`. -/
lemma tendsto_inv_zero_at_top : tendsto (λx:α, x⁻¹) (𝓝[set.Ioi (0:α)] 0) at_top :=
Expand All @@ -1447,8 +1562,6 @@ end
lemma tendsto_inv_at_top_zero : tendsto (λr:α, r⁻¹) at_top (𝓝 0) :=
tendsto_inv_at_top_zero'.mono_right inf_le_left

variables {l : filter β} {f : β → α}

lemma tendsto.inv_tendsto_at_top (h : tendsto f l at_top) : tendsto (f⁻¹) l (𝓝 0) :=
tendsto_inv_at_top_zero.comp h

Expand All @@ -1458,8 +1571,7 @@ tendsto_inv_zero_at_top.comp h
/-- The function `x^(-n)` tends to `0` at `+∞` for any positive natural `n`.
A version for positive real powers exists as `tendsto_rpow_neg_at_top`. -/
lemma tendsto_pow_neg_at_top {n : ℕ} (hn : 1 ≤ n) : tendsto (λ x : α, x ^ (-(n:ℤ))) at_top (𝓝 0) :=
tendsto.congr' (eventually_eq_of_mem (Ioi_mem_at_top 0) (λ x hx, (fpow_neg x n).symm))
(tendsto.inv_tendsto_at_top (tendsto_pow_at_top hn))
tendsto.congr (λ x, (fpow_neg x n).symm) (tendsto.inv_tendsto_at_top (tendsto_pow_at_top hn))

end linear_ordered_field

Expand All @@ -1469,22 +1581,6 @@ lemma preimage_neg [add_group α] : preimage (has_neg.neg : α → α) = image (
lemma filter.map_neg [add_group α] : map (has_neg.neg : α → α) = comap (has_neg.neg : α → α) :=
funext $ assume f, map_eq_comap_of_inverse (funext neg_neg) (funext neg_neg)

section topological_add_group

variables [topological_space α] [ordered_add_comm_group α] [topological_add_group α]

lemma neg_preimage_closure {s : set α} : (λr:α, -r) ⁻¹' closure s = closure ((λr:α, -r) '' s) :=
have (λr:α, -r) ∘ (λr:α, -r) = id, from funext neg_neg,
by rw [preimage_neg]; exact
(subset.antisymm (image_closure_subset_closure_image continuous_neg) $
calc closure ((λ (r : α), -r) '' s) = (λr, -r) '' ((λr, -r) '' closure ((λ (r : α), -r) '' s)) :
by rw [←image_comp, this, image_id]
... ⊆ (λr, -r) '' closure ((λr, -r) '' ((λ (r : α), -r) '' s)) :
monotone_image $ image_closure_subset_closure_image continuous_neg
... = _ : by rw [←image_comp, this, image_id])

end topological_add_group

section order_topology

variables [topological_space α] [topological_space β]
Expand Down Expand Up @@ -2526,100 +2622,6 @@ end liminf_limsup

end order_topology

section linear_ordered_add_comm_group

variables [linear_ordered_add_comm_group α] [topological_space α]

local notation `|` x `|` := abs x

lemma nhds_eq_infi_abs_sub [order_topology α] (a : α) :
𝓝 a = (⨅r>0, 𝓟 {b | |a - b| < r}) :=
begin
simp only [le_antisymm_iff, nhds_eq_order, le_inf_iff, le_infi_iff, le_principal_iff, mem_Ioi,
mem_Iio, abs_sub_lt_iff, @sub_lt_iff_lt_add _ _ _ _ a, @sub_lt _ _ a, set_of_and],
refine ⟨_, _, _⟩,
{ intros ε ε0,
exact inter_mem_inf_sets
(mem_infi_sets (a - ε) $ mem_infi_sets (sub_lt_self a ε0) (mem_principal_self _))
(mem_infi_sets (ε + a) $ mem_infi_sets (by simpa) (mem_principal_self _)) },
{ intros b hb,
exact mem_infi_sets (a - b) (mem_infi_sets (sub_pos.2 hb) (by simp [Ioi])) },
{ intros b hb,
exact mem_infi_sets (b - a) (mem_infi_sets (sub_pos.2 hb) (by simp [Iio])) }
end

lemma order_topology_of_nhds_abs (h_nhds : ∀a:α, 𝓝 a = (⨅r>0, 𝓟 {b | |a - b| < r})) :
order_topology α :=
begin
refine ⟨eq_of_nhds_eq_nhds $ λ a, _⟩,
rw [h_nhds],
letI := preorder.topology α, letI : order_topology α := ⟨rfl⟩,
exact (nhds_eq_infi_abs_sub a).symm
end

variables [order_topology α]

lemma linear_ordered_add_comm_group.tendsto_nhds {f : β → α} {x : filter β} {a : α} :
tendsto f x (𝓝 a) ↔ ∀ ε > (0 : α), ∀ᶠ b in x, |f b - a| < ε :=
by simp [nhds_eq_infi_abs_sub, abs_sub a]

lemma eventually_abs_sub_lt (a : α) {ε : α} (hε : 0 < ε) : ∀ᶠ x in 𝓝 a, |x - a| < ε :=
(nhds_eq_infi_abs_sub a).symm ▸ mem_infi_sets ε
(mem_infi_sets hε $ by simp only [abs_sub, mem_principal_self])

@[priority 100] -- see Note [lower instance priority]
instance linear_ordered_add_comm_group.topological_add_group : topological_add_group α :=
{ continuous_add :=
begin
refine continuous_iff_continuous_at.2 _,
rintro ⟨a, b⟩,
refine linear_ordered_add_comm_group.tendsto_nhds.2 (λ ε ε0, _),
rcases dense_or_discrete 0 ε with (⟨δ, δ0, δε⟩|⟨h₁, h₂⟩),
{ -- If there exists `δ ∈ (0, ε)`, then we choose `δ`-nhd of `a` and `(ε-δ)`-nhd of `b`
filter_upwards [prod_mem_nhds_sets (eventually_abs_sub_lt a δ0)
(eventually_abs_sub_lt b (sub_pos.2 δε))],
rintros ⟨x, y⟩ ⟨hx : |x - a| < δ, hy : |y - b| < ε - δ⟩,
rw [add_sub_comm],
calc |x - a + (y - b)| ≤ |x - a| + |y - b| : abs_add _ _
... < δ + (ε - δ) : add_lt_add hx hy
... = ε : add_sub_cancel'_right _ _ },
{ -- Otherewise `ε`-nhd of each point `a` is `{a}`
have hε : ∀ {x y}, abs (x - y) < ε → x = y,
{ intros x y h,
simpa [sub_eq_zero] using h₂ _ h },
filter_upwards [prod_mem_nhds_sets (eventually_abs_sub_lt a ε0)
(eventually_abs_sub_lt b ε0)],
rintros ⟨x, y⟩ ⟨hx : |x - a| < ε, hy : |y - b| < ε⟩,
simpa [hε hx, hε hy] }
end,
continuous_neg := continuous_iff_continuous_at.2 $ λ a,
linear_ordered_add_comm_group.tendsto_nhds.2 $ λ ε ε0,
(eventually_abs_sub_lt a ε0).mono $ λ x hx, by rwa [neg_sub_neg, abs_sub] }

@[continuity]
lemma continuous_abs : continuous (abs : α → α) := continuous_id.max continuous_neg

lemma filter.tendsto.abs {f : β → α} {a : α} {l : filter β} (h : tendsto f l (𝓝 a)) :
tendsto (λ x, |f x|) l (𝓝 (|a|)) :=
(continuous_abs.tendsto _).comp h

variables [topological_space β] {f : β → α} {b : β} {a : α} {s : set β}

lemma continuous.abs (h : continuous f) : continuous (λ x, |f x|) := continuous_abs.comp h

lemma continuous_at.abs (h : continuous_at f b) : continuous_at (λ x, |f x|) b := h.abs

lemma continuous_within_at.abs (h : continuous_within_at f s b) :
continuous_within_at (λ x, |f x|) s b := h.abs

lemma continuous_on.abs (h : continuous_on f s) : continuous_on (λ x, |f x|) s :=
λ x hx, (h x hx).abs

lemma tendsto_abs_nhds_within_zero : tendsto (abs : α → α) (𝓝[{0}ᶜ] 0) (𝓝[Ioi 0] 0) :=
(continuous_abs.tendsto' (0 : α) 0 abs_zero).inf $ tendsto_principal_principal.2 $ λ x, abs_pos.2

end linear_ordered_add_comm_group

/-!
Here is a counter-example to a version of the following with `conditionally_complete_lattice α`.
Take `α = [0, 1) → ℝ` with the natural lattice structure, `ι = ℕ`. Put `f n x = -x^n`. Then
Expand Down

0 comments on commit 8545aa6

Please sign in to comment.