Equal within s imply same limit within s

Stream: Is there code for X?

[Anatole Dedecker]

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]

You need a lemma whose name contains "congr".

[Patrick Massot]

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

[Patrick Massot]

Now I'll look at mathlib.

[Patrick Massot]

Oh, you got parentheses wrong

[Anatole Dedecker]

Patrick Massot said:

Oh, you got parentheses wrong

Where ?

[Patrick Massot]

The forall is binding too much.

[Anatole Dedecker]

Oh yeah

[Patrick Massot]

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

[Anatole Dedecker]

Indeed

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

The proof I have is 72 characters long.

[Anatole Dedecker]

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

[Anatole Dedecker]

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]

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

[Anatole Dedecker]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Anatole Dedecker]

I definitely underestimated update frequency then :sweat_smile:

[Patrick Massot]

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

[Anatole Dedecker]

HUGE lockdown peak x)

[Patrick Massot]

Of course!

[Anatole Dedecker]

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]

Well, I think it should at least

[Patrick Massot]

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

[Anatole Dedecker]

leanproject up ?

[Anatole Dedecker]

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]

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]

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

[Patrick Massot]

Spoilers!

[Anatole Dedecker]

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

[Sebastien Gouezel]

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

[Anatole Dedecker]

AH

[Patrick Massot]

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

[Sebastien Gouezel]

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]

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)

[Patrick Massot]

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

[Anatole Dedecker]

Guess I should train to use term-mode too

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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]

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]

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

[Johan Commelin]

tidy? will tell you how it proved it

[Anatole Dedecker]

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]

x)

[Patrick Massot]

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]

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]

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

[Sebastien Gouezel]

For readability, you can use

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

[Patrick Massot]

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]

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]

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]

And I know I saw other examples yesterday.

[Yury G. Kudryashov]

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

works in this case.

[Kevin Buzzard]

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]

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]

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]

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]

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

[Patrick Massot]

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]

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]

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