Simple Limits in Rationals

Stream: new members

[Xavier Généreux]

Hi everyone,

I have been trying to play with filters a little bit and although I can prove some statements about limits and easy topological stuff (say like what is found here), I am finding it a little bit hard to show concrete limits that a student would encounter in an intro to analysis class.

Consider for example:

example : Tendsto (fun n : ℕ ↦ (2 * (n : ℚ) + 1) / (5 * (n : ℚ))) atTop (𝓝 (2 / 5))

I can prove this by rewriting definitions until I pretty much make the filters disappear but I would like to know if people had tips to prove similar statements using the language of filters. Should one use bases in this case? Is there a way to one shot this with filter_upwards ?

As one could prove this using the ε-𝛿 definition of convergence, I would like to be able to prove this using the definition of a filter. (In other words, I am not looking for a proof that decomposes this into known limits by using Tendsto.add for example.

Thanks a lot!
Xavier

[Yakov Pechersky]

I would use docs#Filter.Tendsto.comp, as given by lemmas like docs#Continuous.add and docs#Filter.tendsto_congr. Your function is equal to 2n/5n + 1/5n, so atTop, its the sum of both. Then you can use docs#tendsto_one_div_atTop_nhds_zero_nat, docs#continuous_mul; docs#tendsto_natCast_div_add_atTop. The right lemmas will be easy to use via dot notation.

[Xavier Généreux]

Thank you for your answer.
I wasn't clear so I will edit my message.

[David Loeffler]

I'm puzzled by the formulation of this question. Surely the issue of "using the definition of a filter$ vs. "using $\epsilon$-$\delta$ arguments" is orthogonal to whether or not Tendsto.add is used? The proof of Tendsto.add has nothing to do with $\epsilon$-$\delta$ stuff, it works for limits along any filter.

[Xavier Généreux]

Hello David,
Sorry my formulation is indeed not the best.

The two ways I currently know how to prove this limit is to either show it using the classical undergrad definition of eps and delt or show it by decomposing it into known limits.

[Xavier Généreux]

I am wondering if there is a way to do this by unfolding the definition of tendsto and that doesn't use lemmas like Tendsto.add.

[Yakov Pechersky]

docs#Metric.tendsto_atTop is the translation into eps-delta morally

[Yakov Pechersky]

If that's too cheating, you can use docs#tendsto_atTop_nhds

[Kevin Buzzard]

Xavier, I think your question about whether or not you "use Tendsto.add" is the same as asking "should I prove that addition is continuous (e.g. by using epsilon/2 somewhere, which is the key input) or assume it?" Of course, this is up to you :-)

[Xavier Généreux]

The classical proof I had in mind looked like
$\left|\frac{2n}{5n +1} - \frac{2}{5}\right| = \left|\frac{10n - 10n -2 }{5(5n +1)}\right| = \frac{2}{5(5n +1)} < \frac{1}{5n} < \epsilon$
for all $n > N$ with say $\frac{1}{\epsilon } < N.$ (or something like this.)

[Xavier Généreux]

Yakov Pechersky said:

If that's too cheating, you can use docs#tendsto_atTop_nhds

This pretty much rewrites it using some basis of the filters. This kind of works for me. Thanks Yakov.