Stream: Is there code for X?

Topic: Equal within s imply same limit within s

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


Patrick Massot (Jun 25 2020 at 22:12):

You need a lemma whose name contains "congr".

Patrick Massot (Jun 25 2020 at 22:12):

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

Patrick Massot (Jun 25 2020 at 22:12):

Now I'll look at mathlib.

Patrick Massot (Jun 25 2020 at 22:13):

Oh, you got parentheses wrong

Anatole Dedecker (Jun 25 2020 at 22:14):

Patrick Massot said:

Oh, you got parentheses wrong

Where ?

Patrick Massot (Jun 25 2020 at 22:15):

The forall is binding too much.

Oh yeah

Patrick Massot (Jun 25 2020 at 22:16):

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

Indeed

Patrick Massot (Jun 25 2020 at 22:23):

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

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?

Patrick Massot (Jun 25 2020 at 22:27):

The proof I have is 72 characters long.

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

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


Anatole Dedecker (Jun 25 2020 at 22:39):

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

Anatole Dedecker (Jun 25 2020 at 22:41):

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

Patrick Massot (Jun 25 2020 at 22:42):

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

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.

Anatole Dedecker (Jun 25 2020 at 22:45):

I definitely underestimated update frequency then :sweat_smile:

Patrick Massot (Jun 25 2020 at 22:45):

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

Anatole Dedecker (Jun 25 2020 at 22:46):

HUGE lockdown peak x)

Of course!

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


Anatole Dedecker (Jun 25 2020 at 22:50):

Well, I think it should at least

Patrick Massot (Jun 25 2020 at 23:03):

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

Anatole Dedecker (Jun 25 2020 at 23:08):

leanproject up ?

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


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.

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


Spoilers!

Anatole Dedecker (Jun 26 2020 at 11:43):

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

Sebastien Gouezel (Jun 26 2020 at 11:43):

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

AH

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?

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.

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)

λ h, tendsto.congr' $mem_inf_sets_of_right (eventually_principal.mpr h) Anatole Dedecker (Jun 26 2020 at 11:45): Guess I should train to use term-mode too Patrick Massot (Jun 26 2020 at 11:46): But again the correct solution is add lots of tiny lemmas that are easy to find. 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. Patrick Massot (Jun 26 2020 at 11:49): @Yury G. Kudryashov there is a serious issue with precedences for the eventually_eq notation. 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. 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  Anatole Dedecker (Jun 26 2020 at 11:56): But I don't think that's what you were hoping me to do Johan Commelin (Jun 26 2020 at 11:57): tidy? will tell you how it proved it 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  Anatole Dedecker (Jun 26 2020 at 11:58): x) 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. 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  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: 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  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. 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? 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. Patrick Massot (Jun 26 2020 at 12:34): And I know I saw other examples yesterday. 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. 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 ... 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


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.

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


Patrick Massot (Jun 27 2020 at 20:04):

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

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.

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?

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