Zulip Chat Archive

Stream: maths

Topic: nhds_left and nhds_right


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Anatole Dedecker (Jul 29 2020 at 13:28):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Anatole Dedecker (Jul 29 2020 at 13:35):

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

view this post on Zulip Patrick Massot (Jul 29 2020 at 13:39):

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

view this post on Zulip Anatole Dedecker (Jul 29 2020 at 13:53):

I'll do it then !

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jul 29 2020 at 14:35):

Thank you @Patrick Massot for noticing!

view this post on Zulip Patrick Massot (Jul 29 2020 at 14:42):

#3625

view this post on Zulip 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 ?

view this post on Zulip Patrick Massot (Jul 29 2020 at 19:06):

for consistency with neighborhood we should include the point.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jul 29 2020 at 20:29):

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

view this post on Zulip 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