Zulip Chat Archive

Stream: Is there code for X?

Topic: Equal within s imply same limit within s


view this post on Zulip Anatole Dedecker (Jun 25 2020 at 22:08):

Do we have something like this ?

lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α] {a : α} {l : filter β} {s : set α} (f g : α  β) :
     x  s, f x = g x  tendsto f (nhds_within a s) l  tendsto g (nhds_within a s) l :=
begin
  sorry,
end

view this post on Zulip Patrick Massot (Jun 25 2020 at 22:12):

You need a lemma whose name contains "congr".

view this post on Zulip Patrick Massot (Jun 25 2020 at 22:12):

This is not a riddle, that's all I can say at first sight.

view this post on Zulip Patrick Massot (Jun 25 2020 at 22:12):

Now I'll look at mathlib.

view this post on Zulip Patrick Massot (Jun 25 2020 at 22:13):

Oh, you got parentheses wrong

view this post on Zulip Anatole Dedecker (Jun 25 2020 at 22:14):

Patrick Massot said:

Oh, you got parentheses wrong

Where ?

view this post on Zulip Patrick Massot (Jun 25 2020 at 22:15):

The forall is binding too much.

view this post on Zulip Anatole Dedecker (Jun 25 2020 at 22:15):

Oh yeah

view this post on Zulip Patrick Massot (Jun 25 2020 at 22:16):

There is no point in having all this right of the colon anyway.

view this post on Zulip Anatole Dedecker (Jun 25 2020 at 22:18):

Indeed

view this post on Zulip Patrick Massot (Jun 25 2020 at 22:23):

It seems this lemma doesn't exist yet, but docs#filter.tendsto.congr' does.

view this post on Zulip Patrick Massot (Jun 25 2020 at 22:27):

Do you want the answer or do you want to try to finish using this hint only?

view this post on Zulip Patrick Massot (Jun 25 2020 at 22:27):

The proof I have is 72 characters long.

view this post on Zulip Anatole Dedecker (Jun 25 2020 at 22:31):

My PC just crashed, but yeah I've seen this one and I'm trying to deduce mine

view this post on Zulip Anatole Dedecker (Jun 25 2020 at 22:38):

I have this :

lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α] {a : α} {l : filter β} {s : set α} (f g : α  β)
    (h :  x  s, f x = g x) (hf : tendsto f (nhds_within a s) l) : tendsto g (nhds_within a s) l :=
begin
  intros,
  rw  tendsto_congr',
  exact hf,
  use univ,
  split,
  apply filter.univ_sets,
  use s,
  use (by tauto),
  rw univ_inter,
  intros x hx,
  exact h x hx,
end

view this post on Zulip Anatole Dedecker (Jun 25 2020 at 22:39):

I think I'm going too deep in the definition unfolding

view this post on Zulip Anatole Dedecker (Jun 25 2020 at 22:41):

And the first line is useless, I should have removed it

view this post on Zulip Patrick Massot (Jun 25 2020 at 22:42):

Your proof doesn't work here. Are you using an old mathlib?

view this post on Zulip Patrick Massot (Jun 25 2020 at 22:43):

For the purpose of this conversation, old probably means older than https://github.com/leanprover-community/mathlib/commit/d287d34590761dc6237c7b21d9427580b2d339c4.

view this post on Zulip Anatole Dedecker (Jun 25 2020 at 22:45):

I definitely underestimated update frequency then :sweat_smile:

view this post on Zulip Patrick Massot (Jun 25 2020 at 22:45):

https://leanprover-community.github.io/mathlib_stats.html

view this post on Zulip Anatole Dedecker (Jun 25 2020 at 22:46):

HUGE lockdown peak x)

view this post on Zulip Patrick Massot (Jun 25 2020 at 22:46):

Of course!

view this post on Zulip Anatole Dedecker (Jun 25 2020 at 22:49):

I was in another file with one more open, but it works now :

import analysis.calculus.mean_value

open filter set

lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α] {a : α} {l : filter β} {s : set α} (f g : α  β) :
    ( x  s, f x = g x)  tendsto f (nhds_within a s) l  tendsto g (nhds_within a s) l :=
begin
  intros h hf,
  rw  tendsto_congr',
  exact hf,
  use univ,
  split,
  apply filter.univ_sets,
  use s,
  use (by tauto),
  rw univ_inter,
  intros x hx,
  exact h x hx,
end

view this post on Zulip Anatole Dedecker (Jun 25 2020 at 22:50):

Well, I think it should at least

view this post on Zulip Patrick Massot (Jun 25 2020 at 23:03):

No, it doesn't work here. Did you update mathlib?

view this post on Zulip Anatole Dedecker (Jun 25 2020 at 23:08):

leanproject up ?

view this post on Zulip Anatole Dedecker (Jun 26 2020 at 11:27):

Well I've just run leanproject up and this definitely compile :

import analysis.calculus.mean_value

open filter set

lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α] {a : α} {l : filter β} {s : set α} (f g : α  β) :
    ( x  s, f x = g x)  tendsto f (nhds_within a s) l  tendsto g (nhds_within a s) l :=
begin
  intros h hf,
  rw  tendsto_congr',
  exact hf,
  use univ,
  split,
  apply filter.univ_sets,
  use s,
  use (by tauto),
  rw univ_inter,
  intros x hx,
  exact h x hx,
end

view this post on Zulip Patrick Massot (Jun 26 2020 at 11:32):

The main trick you're missing in docs#filter.mem_inf_sets_of_right . One could argue this is relying on internal details of nhds_within, and the nhds_within API is lacking.

view this post on Zulip Sebastien Gouezel (Jun 26 2020 at 11:38):

This works for me:

lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α]
  {a : α} {l : filter β} {s : set α} {f g : α  β}
  (h :  x  s, f x = g x) (hf : tendsto f (nhds_within a s) l) : tendsto g (nhds_within a s) l :=
(tendsto_congr' (eventually_eq_iff_exists_mem.2 s, self_mem_nhds_within, h)).1 hf

I am cheating because this won't work for you, as I have somewhere in filter/basic.lean the lemma

lemma eventually_eq_iff_exists_mem {l : filter α} {f g : α  β} :
  (f =[l] g)   s  l,  x  s, f x = g x :=
filter.eventually_iff_exists_mem

view this post on Zulip Patrick Massot (Jun 26 2020 at 11:42):

Spoilers!

view this post on Zulip Anatole Dedecker (Jun 26 2020 at 11:43):

Well even filter.eventually_iff_exists_mem doesn't exist for me, should it ?

view this post on Zulip Sebastien Gouezel (Jun 26 2020 at 11:43):

Not so much because it doesn't work with current mathlib :)

view this post on Zulip Anatole Dedecker (Jun 26 2020 at 11:43):

AH

view this post on Zulip Patrick Massot (Jun 26 2020 at 11:44):

Anatole, do you want to see a short solution that actually work, or do you want to keep trying?

view this post on Zulip Sebastien Gouezel (Jun 26 2020 at 11:44):

No, it doesn't exist either. But it is not hard to prove. It's just to illustrate that having basic API (which is currently missing) helps a lot to prove further statements.

view this post on Zulip Anatole Dedecker (Jun 26 2020 at 11:45):

Patrick Massot said:

Anatole, do you want to see a short solution that actually work, or do you want to keep trying?

I'll take it, I like to learn by imitating x)

view this post on Zulip Patrick Massot (Jun 26 2020 at 11:45):

λ h, tendsto.congr' $ mem_inf_sets_of_right (eventually_principal.mpr h)

view this post on Zulip Anatole Dedecker (Jun 26 2020 at 11:45):

Guess I should train to use term-mode too

view this post on Zulip Patrick Massot (Jun 26 2020 at 11:46):

But again the correct solution is add lots of tiny lemmas that are easy to find.

view this post on Zulip Patrick Massot (Jun 26 2020 at 11:47):

After the third line of your solution, you need to stop and think: there should be a lemma here. Then type extract_goal, do some cleanup, prove and use.

view this post on Zulip Patrick Massot (Jun 26 2020 at 11:49):

@Yury G. Kudryashov there is a serious issue with precedences for the eventually_eq notation.

view this post on Zulip Patrick Massot (Jun 26 2020 at 11:52):

Anatole, the issue is that eventually_eq and eventually_le are very recent and still lack of lot of lemmas. Even eventually and frequently are not so old and still lack lemmas. If you unfold all see to basic filter stuff, involving only membership and lattices operations on filters, then all the lemmas are there. But we need a lot of plumbing.

view this post on Zulip Anatole Dedecker (Jun 26 2020 at 11:56):

Wow tidy is powerful

lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α] {a : α} {l : filter β} {s : set α} (f g : α  β) :
    ( x  s, f x = g x)  tendsto f (nhds_within a s) l  tendsto g (nhds_within a s) l :=
begin
  intros h hf,
  rw  tendsto_congr',
  exact hf,
  apply mem_inf_sets_of_right,
  tidy,
end

view this post on Zulip Anatole Dedecker (Jun 26 2020 at 11:56):

But I don't think that's what you were hoping me to do

view this post on Zulip Johan Commelin (Jun 26 2020 at 11:57):

tidy? will tell you how it proved it

view this post on Zulip Anatole Dedecker (Jun 26 2020 at 11:58):

lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α] {a : α} {l : filter β} {s : set α} (f g : α  β) :
    ( x  s, f x = g x)  tendsto f (nhds_within a s) l  tendsto g (nhds_within a s) l :=
begin
  intros h hf,
  rw  tendsto_congr',
  exact hf,
  apply mem_inf_sets_of_right,
  assumption,
end

view this post on Zulip Anatole Dedecker (Jun 26 2020 at 11:58):

x)

view this post on Zulip Patrick Massot (Jun 26 2020 at 12:11):

Here is your plumbing exercise:

import topology.continuous_on

open_locale filter topological_space
open filter set

variables {α β : Type*} [topological_space α] {a : α} {s : set α} {f g : α  β}

lemma eventually_eq_nhds_within_iff  :
  (f =[nhds_within a s] g)   x in 𝓝 a, x  s  f x = g x :=
sorry

lemma eventually_eq_nhds_within_of_eq_on (h : eq_on f g s) : f =[nhds_within a s] g :=
sorry

lemma tendsto_nhds_within_congr {l : filter β} (hfg :  x  s, f x = g x)
  (hf : tendsto f (nhds_within a s) l) : tendsto g (nhds_within a s) l :=
sorry

Make sure you understand the choices of binders. The second and third proofs should be one line long terms. The first one will probably be longer, which means it should probably be split further.

view this post on Zulip Anatole Dedecker (Jun 26 2020 at 12:16):

Hey, I got shorter than you :grinning_face_with_smiling_eyes:

lemma tendsto_nhds_within_of_tendsto_nhds_within_of_eq_within {α β : Type} [topological_space α] {a : α} {l : filter β} {s : set α} (f g : α  β) :
    ( x  s, f x = g x)  tendsto f (nhds_within a s) l  tendsto g (nhds_within a s) l :=
λ h, (tendsto_congr' (mem_inf_sets_of_right (by exact h))).1

view this post on Zulip Anatole Dedecker (Jun 26 2020 at 12:16):

Now it is not entirely clear why by exact h can't be replaced by h here :thinking:

view this post on Zulip Sebastien Gouezel (Jun 26 2020 at 12:21):

For readability, you can use

λ h, (tendsto_congr' $ mem_inf_sets_of_right $ by exact h).1

view this post on Zulip Patrick Massot (Jun 26 2020 at 12:21):

The fact that by exact is needed shows Lean elaboration has trouble. You're not being nice to Lean, it has to unfold many definition in the right order to get there. This is why you need plumbing.

view this post on Zulip Yury G. Kudryashov (Jun 26 2020 at 12:33):

Patrick Massot said:

Yury G. Kudryashov there is a serious issue with precedences for the eventually_eq notation.

What exactly do you mean? #mwe?

view this post on Zulip Patrick Massot (Jun 26 2020 at 12:34):

https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Equal.20within.20s.20imply.20same.20limit.20within.20s/near/202081600 is autonomous. The first statement needs unexpected parentheses.

view this post on Zulip Patrick Massot (Jun 26 2020 at 12:34):

And I know I saw other examples yesterday.

view this post on Zulip Yury G. Kudryashov (Jun 26 2020 at 13:05):

notation f ` =[`:50 l:50 `] `:0 g:50 := filter.eventually_eq l f g

works in this case.

view this post on Zulip Kevin Buzzard (Jun 26 2020 at 13:46):

Anatole Dedecker said:

Guess I should train to use term-mode too

If you concentrate on proving and tactic mode then you will slowly realise which proofs have "content" (e.g. they use high-powered tactics) and which proofs are literally just "intro, apply, cases, exact" which are really just ways to make a function piece by piece. For these "basic" proofs it's a good exercise to turn it into term mode (because you learn some weird tricks sometimes). After a while you can write hybrid proofs, where the intro/apply stuff is in term mode, and the occasional high-powered tactic like rw is just done by briefly dropping into tactic mode with by rw ...

view this post on Zulip Anatole Dedecker (Jun 27 2020 at 14:42):

I've been busy IRL since yesterday afternoon, but here is the plumbing @Patrick Massot . I could shorten the first, especially if I finally start to learn rcases :sweat_smile: but I'll work on this later, cause my parents are exploiting me right now x)

import topology.continuous_on
import tactic.tidy

open_locale filter topological_space
open filter set

variables {α β : Type*} [topological_space α] {a : α} {s : set α} {f g : α  β}

lemma eventually_eq_nhds_within_iff  :
  (f =[nhds_within a s] g)   x in 𝓝 a, x  s  f x = g x :=
begin
  unfold eventually_eq,
  rw eventually_iff,
  rw eventually_iff,
  rw mem_nhds_within,
  rw mem_nhds_sets_iff,
  split,
  { intros h,
    cases h with u hu,
    cases hu with hu hau,
    cases hau with hau hus,
    use u,
    split,
    intros x hx hxs,
    apply hus,
    exact and.intro hx hxs,
    exact and.intro hu hau, },
  { intros h,
    cases h with t ht,
    cases ht with htsub ht,
    cases ht with ht hta,
    use t,
    split,
    exact ht,
    split,
    exact hta,
    intros x hx,
    cases hx with hxt hxs,
    exact htsub hxt hxs }
end

lemma eventually_eq_nhds_within_of_eq_on (h : eq_on f g s) : f =[nhds_within a s] g :=
mem_inf_sets_of_right h

lemma tendsto_nhds_within_congr {l : filter β} (hfg :  x  s, f x = g x)
  (hf : tendsto f (nhds_within a s) l) : tendsto g (nhds_within a s) l :=
(tendsto_congr' $ eventually_eq_nhds_within_of_eq_on hfg).1 hf

view this post on Zulip Patrick Massot (Jun 27 2020 at 20:03):

Indeed you need to learn about rintros/rcases. But actually you are not using any tactic here. After the rewrite, everything you wrote has completely straightforward translation to term mode. You can also group your rw in one tactic invocation.

view this post on Zulip Patrick Massot (Jun 27 2020 at 20:04):

lemma eventually_eq_nhds_within_iff  :
  (f =[nhds_within a s] g)   x in 𝓝 a, x  s  f x = g x :=
begin
  rw [eventually_eq, eventually_iff, eventually_iff, mem_nhds_within, mem_nhds_sets_iff],
  exact ⟨λ u, hu, hau, hus, u, λ x hx hxs, hus hx, hxs, hu, hau⟩⟩,
         λ t, htsub, ht, hta, t, ht, hta, λ x hxt, hxs, htsub hxt hxs⟩⟩
end

view this post on Zulip Patrick Massot (Jun 27 2020 at 20:04):

This is exactly your proof, but without wasting too much space.

view this post on Zulip Patrick Massot (Jun 27 2020 at 20:07):

Note also:

  • nobody is interested in seeing this proof since the statement is obvious. mathlib style in this case is to compress the proof.
  • actually you don't loose any information. You can still move your cursor and see the tactic state. Note that the tactic state is update when you move your cursor from left to right in the rw line but also in the exact line.
  • you still miss intermediate lemmas that could be useful.

view this post on Zulip Patrick Massot (Jun 27 2020 at 20:13):

Elaborating on the third point: don't you find it weird that you had to use the definition of neighborhoods in this proof? Don't you feel the lemma should be more general than that?

view this post on Zulip Patrick Massot (Jun 27 2020 at 20:14):

import topology.continuous_on

open_locale filter topological_space
open filter

variables {α β : Type*}  {a : α} {s : set α} {f g : α  β}

lemma eventually_eq_inf_principal_iff  {F : filter α} :
  (f =[F  𝓟 s] g)   x in F, x  s  f x = g x :=
by simp [eventually_eq, eventually_iff, mem_inf_principal]

lemma eventually_eq_nhds_within_iff [topological_space α] :
  (f =[nhds_within a s] g)   x in 𝓝 a, x  s  f x = g x :=
eventually_eq_inf_principal_iff

Last updated: May 16 2021 at 05:21 UTC