tendsto equivalent to is bounded

Stream: Is there code for X?

[Ella Yu]

Hi! Is there a theorem in mathlib similar to the following? Or can anyone give me a hint on how to prove this please?

theorem tendsto_equiv_has_bound (seq: ℕ → ℝ):
tendsto seq at_top (𝓝 1) → (∃ x: ℕ, ∀ c_1 < 1, ∀ c_2 > 1, c_1 ≤ seq x ∧ seq x ≤ c_2):=sorry

Thanks a lot!

[Anatole Dedecker]

The key lemma here is docs#nhds_basis_Ioo, and you can probably find closer matches later in the same file

[Anatole Dedecker]

You can also probably get there using docs#nhds_left_sup_nhds_right

[Anatole Dedecker]

I’m not at my computer atm, but if you are still struggling I can make a proof in a few hours

[Anatole Dedecker]

And search more efficiently too

[Anatole Dedecker]

Oh and I assumed you were familiar with filters, if that is not the case then tell me and I’ll provide more details

[Ella Yu]

Sorry, I just saw that. I'm not quite familiar with filters and nhds, if you can help me to explain a little bit more that will be awesome! Thanks a lot!

[Kevin Buzzard]

Right now your theorem doesn't look true? Although I said this about something on this forum yesterday and I was wrong, so take this with a pinch of salt. Doesn't your theorem say "if the sequence tends to 1 then there's an element s (:= seq x) of the sequence with the property that for all c1<1 and for all c2 > 1, we have c1<=s and s<=c2"? It seems to me that you need to swap the forall and exists for this to be true?

[Anatole Dedecker]

Oh right definitely, I fixed the statement in my head while reading it :sweat_smile:

[Ella Yu]

Right I see,

theorem tendsto_equiv_has_bound (seq: ℕ → ℝ):
tendsto seq at_top (𝓝 1) → (∀ c_1 < 1, ∀ c_2 > 1, ∃ x: ℕ, c_1 ≤ seq x ∧ seq x ≤ c_2):=sorry

so it should be something like this? Thank you so much!

[Kevin Buzzard]

And a low-level proof would be: take c_1 < 1 and c_2 > 1, then show that the closed interval Icc c_1 c_2 is an element of the 𝓝 1 filter, so by this tendsto hypothesis its preimage under the map seq will be a subset of nat in the at_top filter so in particular it will be nonempty, so choose an element x and this element will work. Anatole is suggesting a way of getting there more quickly.

[Anatole Dedecker]

I was also thinking about the following statement, matching the topic title :

import topology.metric_space.basic

open filter
open_locale topological_space

example (seq : ℕ → ℝ) :
  tendsto seq at_top (𝓝 1) ↔ ∀ l < 1, ∀ u > 1, ∃ N, ∀ n ≥ N, l < seq n ∧ seq n < u :=
sorry

[Anatole Dedecker]

But indeed for your statement you don't need filter bases, so let's start with this

[Junyan Xu]

import topology.metric_space.basic
open_locale topological_space
open filter
theorem tendsto_equiv_has_bound (seq : ℕ → ℝ) (h : tendsto seq at_top (𝓝 1)) :
  ∀ c_1 < 1, ∀ c_2 > 1, ∃ x : ℕ, c_1 ≤ seq x ∧ seq x ≤ c_2 :=
λ c1 h1 c2 h2, let ⟨x, hx⟩ := mem_at_top_sets.1 (tendsto_def.1 h _ $ Icc_mem_nhds h1 h2) in ⟨x, hx x rfl.le⟩

or with tactics:

theorem tendsto_equiv_has_bound (seq : ℕ → ℝ) (h : tendsto seq at_top (𝓝 1)) :
  ∀ c_1 < 1, ∀ c_2 > 1, ∃ x : ℕ, c_1 ≤ seq x ∧ seq x ≤ c_2 :=
λ c1 h1 c2 h2, begin
  rw tendsto_def at h,
  specialize h _ (Icc_mem_nhds h1 h2),
  obtain ⟨x, hx⟩ := mem_at_top_sets.1 h,
  use x, apply hx, exact le_rfl,
end

[Anatole Dedecker]

For this one, the right proof is the one proposed by Kevin (I don't think bases buy you anything in that case), but we can reformulate it a bit so that it seems more natural. You should think of the fact that Icc c_1 c_2 is in 𝓝 1 (this is docs#Icc_mem_nhds) as a way of expressing the fact that "when x apporaches 1, we eventually have x ∈ Icc c_1 c_2" (see the definition of docs#filter.eventually). Then , since we have tendsto seq at_top (𝓝 1), we can use docs#filter.tendsto.eventually to deduce that "when n approaches infinity, we eventually have seq n ∈ Icc c_1 c_2. Finally, since at_top : filter ℕ is a nontrivial filter, you can use docs#filter.eventually.exists to finish your proof

[Anatole Dedecker]

Junyan Xu said:

import topology.metric_space.basic
open_locale topological_space
open filter
theorem tendsto_equiv_has_bound (seq : ℕ → ℝ) (h : tendsto seq at_top (𝓝 1)) :
  ∀ c_1 < 1, ∀ c_2 > 1, ∃ x : ℕ, c_1 ≤ seq x ∧ seq x ≤ c_2 :=
λ c1 h1 c2 h2, let ⟨x, hx⟩ := mem_at_top_sets.1 (tendsto_def.1 h _ $ Icc_mem_nhds h1 h2) in ⟨x, hx x rfl.le⟩

Hmmm you shouldn't have to use mem_at_top_sets here, only the fact that at_top is nontrivial

[Anatole Dedecker]

My proof would be something like :

import topology.metric_space.basic

open filter
open_locale topological_space

theorem tendsto_equiv_has_bound (seq : ℕ → ℝ) (h : tendsto seq at_top (𝓝 1)) :
  ∀ c_1 < 1, ∀ c_2 > 1, ∃ x : ℕ, c_1 ≤ seq x ∧ seq x ≤ c_2 :=
λ c_1 h_1 c_2 h_2, (h.eventually (Icc_mem_nhds h_1 h_2)).exists

[Anatole Dedecker]

And notice there is nothing special about at_top here, it would work the same for any nontrivial filter :

theorem tendsto_equiv_has_bound' {ι : Type*} {l : filter ι} [l.ne_bot] (seq : ι → ℝ)
  (h : tendsto seq l (𝓝 1)) :
  ∀ c_1 < 1, ∀ c_2 > 1, ∃ x : ι, c_1 ≤ seq x ∧ seq x ≤ c_2 :=
λ c_1 h_1 c_2 h_2, (h.eventually (Icc_mem_nhds h_1 h_2)).exists

[Anatole Dedecker]

(One could also generalize the target using docs#order_closed_topology, but that's less crucial)

[Ella Yu]

Thanks for all of your answers, I'm thinking about how can we prove the opposite direction.

theorem tendsto_equiv_has_bound (seq : ℕ → ℝ)  :
  ∀ c_1 < 1, ∀ c_2 > 1, ∃ x : ℕ, c_1 ≤ seq x ∧ seq x ≤ c_2  →  tendsto seq at_top (𝓝 1):=sorry

[Anatole Dedecker]

This one is not true, you need the statement that I posted above

[Anatole Dedecker]

You need to ask that all terms of the sequence are close to 1 after a certain point

[Anatole Dedecker]

Anatole Dedecker said:

I was also thinking about the following statement, matching the topic title :

import topology.metric_space.basic

open filter
open_locale topological_space

example (seq : ℕ → ℝ) :
  tendsto seq at_top (𝓝 1) ↔ ∀ l < 1, ∀ u > 1, ∃ N, ∀ n ≥ N, l < seq n ∧ seq n < u :=
sorry

This statement

[Ella Yu]

I see, so if I wish to prove this equivalence statement, I need to consider ∃ N, ∀ n ≥ N,.

[Anatole Dedecker]

Yes

[Anatole Dedecker]

To prove the equivalence, the best is really to use filter bases, namely docs#filter.has_basis.tendsto, docs#at_top_basis and docs#nhds_basis_Ioo

[Anatole Dedecker]

And then you have to do a bit of cleaning to get to exactly the form you want

[Anatole Dedecker]

This would be something like this :

import topology.metric_space.basic

open filter
open_locale topological_space

example (seq : ℕ → ℝ) :
  tendsto seq at_top (𝓝 1) ↔ ∀ l < 1, ∀ u > 1, ∃ N, ∀ n ≥ N, l < seq n ∧ seq n < u :=
begin
  rw [at_top_basis.tendsto_iff (nhds_basis_Ioo (1 : ℝ))],
  simp only [set.mem_Ici, set.mem_Ioo, exists_true_left, and_imp, prod.forall, gt_iff_lt,
    ge_iff_le],
  exact forall_congr (λ _, forall_swap),
  apply_instance
end

[Anatole Dedecker]

Note that this is specific to at_top (although it would work for at_top over other types than ℕ of course)

[Anatole Dedecker]

All the mathematical content is in the first line of the proof, the rest is just messing around to make things match

[Ella Yu]

Thank you so much!!! I'm trying to prove the prime number theorem with my groupmates, but I'm not familiar with lean, this is super helpful!

[Junyan Xu]

Seems this can be generalized to an iff version of docs#tendsto_order_unbounded?

[Anatole Dedecker]

Junyan Xu said:

Seems this can be generalized to an iff version of docs#tendsto_order_unbounded?

Oh I didn't know about this lemma. But indeed it should be an iff, and then we should use this one

[Anatole Dedecker]

Oh we have docs#tendsto_order

[Anatole Dedecker]

Oh right, in general you need to split the two foralls because, if a is a minimum, one of the conditions is a forall on an empty set

[Kevin Buzzard]

@Ella Yu that's an awesome goal! Are you going to make a roadmap like people tend to do for larger projects? See Bloom-Mehta for a recent example (click on "blueprint").

[Anatole Dedecker]

Ella Yu said:

Thank you so much!!! I'm trying to prove the prime number theorem with my groupmates, but I'm not familiar with lean, this is super helpful!

No problem, I'm a filter fanboy so I love answering to these questions x) I should also say that if filters are too much of a problem we have docs#metric.tendsto_at_top. But you'll should at least use filters in the statements to be able to use all the API

[Ella Yu]

Kevin Buzzard said:

Ella Yu that's an awesome goal! Are you going to make a roadmap like people tend to do for larger projects? See Bloom-Mehta for a recent example (click on "blueprint").

This looks good! I'll talk about this with my groupmates tomorrow to see how to make it a larger project: )

[Ella Yu]

Anatole Dedecker said:

Ella Yu said:

Thank you so much!!! I'm trying to prove the prime number theorem with my groupmates, but I'm not familiar with lean, this is super helpful!

No problem, I'm a filter fanboy so I love answering to these questions x) I should also say that if filters are too much of a problem we have docs#metric.tendsto_at_top. But you'll should at least use filters in the statements to be able to use all the API

Great! I'll check the docs#metric.tendsto_at_top page :D