## Stream: maths

### Topic: nhds_left and nhds_right

#### Patrick Massot (Jul 29 2020 at 13:15):

I haven't followed very closely Anatole's recent efforts, but it seems that limits from the left and from the right are more painful than they should be. I wonder we should rather base things on something like the following code. There I restricted to real numbers, but we could be more general by replace x + epsilon by y > x.

import topology.instances.real
noncomputable theory

open set filter
open_locale topological_space filter

section preliminaries
variables {α ι ι' : Type*}

variables {l l' : filter α} {p : ι → Prop} {s : ι → set α} {t : set α} {i : ι}
{p' : ι' → Prop} {s' : ι' → set α} {i' : ι'}

lemma filter.has_basis.sup (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
(l ⊔ l').has_basis (λ i : ι × ι', p i.1 ∧ p' i.2) (λ i, s i.1 ∪ s' i.2) :=
⟨begin
rintros t,
rw [mem_sup_sets, hl.mem_iff, hl'.mem_iff],
split,
{ rintros ⟨⟨i, pi, hi⟩, ⟨i', pi', hi'⟩⟩,
use [(i, i'), pi, pi'],
finish },
{ rintros ⟨⟨i, i'⟩, ⟨⟨pi, pi'⟩, h⟩⟩,
split,
{ use [i, pi],
finish },
{ use [i', pi'],
finish } }
end⟩

lemma filter.has_basis.ext (hl : l.has_basis p s) (hl' : l'.has_basis p' s')
(h : ∀ i, p i → ∃ i', p' i' ∧ s' i' ⊆ s i)
(h' : ∀ i', p' i' → ∃ i, p i ∧ s i ⊆ s' i') : l = l' :=
begin
apply le_antisymm,
{ rw hl.le_basis_iff hl',
simpa using h' },
{ rw hl'.le_basis_iff hl,
simpa using h },
end

@[nolint ge_or_gt] -- see Note [nolint_ge]
lemma filter.has_basis_binfi_principal' {α β : Type*} {s : β → set α} {p : β → Prop}
(h : ∀ i, p i → ∀ j, p j → ∃ k (h : p k), s k ⊆ s i ∧ s k ⊆ s j)
(ne : ∃ i, p i) :
(⨅ i (h : p i), 𝓟 (s i)).has_basis p s :=
filter.has_basis_binfi_principal h ne

end preliminaries

def nhds_left (x : ℝ) := ⨅ ε > 0, 𝓟 $Ioc (x - ε) x def nhds_right (x : ℝ) := ⨅ ε > 0, 𝓟$ Ico x (x + ε)

localized "notation 𝓝ₗ := nhds_left" in topological_space
localized "notation 𝓝ᵣ := nhds_right" in topological_space

lemma real.has_basis_nhds_left (x : ℝ) : (𝓝ₗ x).has_basis (λ ε : ℝ, 0 < ε) (λ ε, Ioc (x - ε) x) :=
begin
apply filter.has_basis_binfi_principal' _ ⟨(1 : ℝ), zero_lt_one⟩,
intros ε ε_pos η η_pos,
have := min_le_left ε η,
have := min_le_right ε η,
refine ⟨min ε η, lt_min ε_pos η_pos, _, _⟩ ;
apply Ioc_subset_Ioc ; linarith
end

lemma real.has_basis_nhds_right (x : ℝ) : (𝓝ᵣ x).has_basis (λ ε : ℝ, 0 < ε) (λ ε, Ico x (x + ε)) :=
begin
apply filter.has_basis_binfi_principal' _ ⟨(1 : ℝ), zero_lt_one⟩,
intros ε ε_pos η η_pos,
have := min_le_left ε η,
have := min_le_right ε η,
refine ⟨min ε η, lt_min ε_pos η_pos, _, _⟩ ;
apply Ico_subset_Ico ; linarith
end

lemma real.has_basis_nhds (x : ℝ) : (𝓝 x).has_basis (λ ε : ℝ, 0 < ε) (λ ε, Ioo (x - ε) (x + ε)) :=
begin
convert metric.nhds_basis_ball,
ext r,
rw real.ball_eq_Ioo
end

lemma nhds_left_sup_nhds_right (x : ℝ) : 𝓝ₗ x ⊔ 𝓝ᵣ x = 𝓝 x :=
begin
apply (x.has_basis_nhds_left.sup x.has_basis_nhds_right).ext x.has_basis_nhds,
{ rintros ⟨ε, η⟩ ⟨ε_pos, η_pos⟩,
use [min ε η, lt_min ε_pos η_pos],
have := min_le_left ε η,
have := min_le_right ε η,
dsimp only,
rw Ioc_union_Ico_eq_Ioo ; try { linarith },
apply Ioo_subset_Ioo ; linarith },
{ intros ε ε_pos,
use [(ε, ε), ε_pos, ε_pos],
dsimp only,
rw Ioc_union_Ico_eq_Ioo ; linarith }
end

lemma tendsto_nhds_iff_left_right {α : Type*} {F : filter α} {x : ℝ} {f : ℝ → α} :
tendsto f (𝓝 x) F ↔ tendsto f (𝓝ₗ x) F ∧ tendsto f (𝓝ᵣ x) F :=
begin
rw ← nhds_left_sup_nhds_right,
exact tendsto_sup
end


@Anatole Dedecker @Sebastien Gouezel @Yury G. Kudryashov

#### Sebastien Gouezel (Jul 29 2020 at 13:20):

I'd rather define nhds_left and nhds_right in terms of nhds_within (Ioi _) as there is already a lot of supporting API, and prove the charaterization in terms of principal as a theorem, but otherwise it looks like a very good idea.

#### Anatole Dedecker (Jul 29 2020 at 13:27):

I agree with Sebastien, because continuous_on is defined in term of nhds_within, so defining nhds_right and nhds_left differently would imply another layer of translation, which means lots of new lemmas to make. Note that I recently PR-ed lemmas that allow to turn any left/right neighborhood to their "canonical" Ioi/Ici/Iio/Iic form, which makes things a lot easier already

#### Patrick Massot (Jul 29 2020 at 13:29):

Yes, the above code was written after having a very superficial look at this PR. My hope was that my definitions could be a convenient "canonical definition", but I wouldn't be surprised to be wrong.

#### Patrick Massot (Jul 29 2020 at 13:31):

Anatole, are you interested in taking care of the above code? Otherwise I'll at least PR the preliminaries.

#### Anatole Dedecker (Jul 29 2020 at 13:35):

Well, it may be faster if you do it :sweat_smile: but as you want !

#### Patrick Massot (Jul 29 2020 at 13:39):

There is no hurry at all. I don't need any of this.

#### Anatole Dedecker (Jul 29 2020 at 13:53):

I'll do it then !

#### Patrick Massot (Jul 29 2020 at 14:24):

Maybe I should PR the general stuff to make sure it doesn't get lost, and then you can think about left and right neighborhoods.

#### Yury G. Kudryashov (Jul 29 2020 at 14:35):

When I was adding tfae to topology/algebra/ordered, we had no filter.has_basis. I guess proofs can be simplified by using has_basis API.

#### Yury G. Kudryashov (Jul 29 2020 at 14:35):

Thank you @Patrick Massot for noticing!

#3625

#### Anatole Dedecker (Jul 29 2020 at 19:02):

Do you think nhds_right a should be defined as nhds_within (Ioi a) or nhds_within (Ici a) ? e.g do we want tendsto (λ x : ℝ, 1/x) (nhds_right 0) at_top to be true ?

#### Patrick Massot (Jul 29 2020 at 19:06):

for consistency with neighborhood we should include the point.

#### Yury G. Kudryashov (Jul 29 2020 at 20:28):

We can have notation both for nhds_within (Ioi a) a and nhds_within (Ici a) a. Both are useful.

#### Yury G. Kudryashov (Jul 29 2020 at 20:29):

I think that we don't use defs, notation would work.

#### Yury G. Kudryashov (Jul 29 2020 at 20:29):

This way lemmas about nhds_within will work without unfolding.

Last updated: May 18 2021 at 07:19 UTC