nhds_left and nhds_right

Stream: maths

[Patrick Massot]

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]

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]

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

[Anatole Dedecker]

See https://github.com/leanprover-community/mathlib/pull/3516

[Patrick Massot]

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]

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

[Anatole Dedecker]

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

[Patrick Massot]

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

[Anatole Dedecker]

I'll do it then !

[Patrick Massot]

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]

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]

Thank you @Patrick Massot for noticing!

[Patrick Massot]

#3625

[Anatole Dedecker]

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]

for consistency with neighborhood we should include the point.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

This way lemmas about nhds_within will work without unfolding.