Simple cauchy sequence fact

Stream: mathlib4

[Alex Meiburg]

I'm looking for a theorem giving me this fact, without chasing the epsilons myself -- I feel sure this "has" to be in Mathlib in some form, but my loogle-fu is failing me :)

theorem real_cauchy_stupid (x : CauSeq ℚ abs) : ∀ ε > 0, ∃ i, ∀ j ≥ i, |x j - Real.mk x| ≤ ε := by
  sorry

[Andrew Yang]

Here's an attempt

theorem real_cauchy_stupid (x : CauSeq ℚ abs) : ∀ ε > 0, ∃ i, ∀ j ≥ i, |x j - Real.mk x| ≤ ε := by
  intro ε hε
  obtain ⟨q, hq, hq'⟩ := exists_rat_btwn hε
  obtain ⟨i, hi⟩ := x.2.cauchy₂ (by simpa using hq)
  simp_rw [abs_sub_comm]
  refine ⟨i, fun j hj ↦ Real.mk_near_of_forall_near ⟨i, fun k hk ↦ ?_⟩⟩
  exact_mod_cast ((Rat.cast_strictMono (hi k hk j hj)).trans hq').le

I'm not familiar with this part of the library but I feel one probably shouldn't use Real.mk but some CauSeq.lim instead.

[Patrick Massot]

Are you really really sure you need this lemma? This is very unlikely.

[Alex Meiburg]

Maybe I don't! So I'm probably using some API in the "wrong" way. If you tell me why needing this is unlikely, maybe I can figure out how to use things in the correct way?

e.g. is using Real.mk a sign of something bad? -- and why is it bad / what should I be trying to do instead?

[Jireh Loreaux]

Alex, why don't you answer a different question: what were you trying to do that you ended up needing this? It sounds like an #xy problem.

[Alex Meiburg]

Well, I've got a cauchy sequence of rationals x, and then I apply a certain element-wise function to that to get a new rational sequence y, and I want to prove that y converges to rexp x

[Kevin Buzzard]

Is this for some constructive exp function?

[Alex Meiburg]

Yeah

[Kevin Buzzard]

So do you actually want concrete bounds on your $i(\epsilon)$?

[Alex Meiburg]

No, just that it converges

[Jireh Loreaux]

I'm confused, you want it to be constructive, but you don't actually want concrete bounds on the convergence rate?

[Yakov Pechersky]

Use docs#Filter.Tendsto of your sequence with atTop and Nhds. So you have, for a sequence u : Nat -> Rat, Tendsto u atTop (Nhds x), and you want to prove that Tendsto (f o u) atTop (Nhds (rexp x)). Where the proof will be something that involves the continuity of f and rexp, looking like Tendsto f (Nhds x) (Nhds (rexp x)), if I understand correctly.

[Alex Meiburg]

Jireh Loreaux said:

I'm confused, you want it to be constructive, but you don't actually want concrete bounds on the convergence rate?

Haha yes, for this purpose: #general > Discussion: ComputableReal

[Alex Meiburg]

I'm just using Andrew Yang's code (since it was handy) but I'm still wondering if there's a "better way" to do the thing.

[Chris Wong]

My uninformed guess is that CauSeq's purpose is to bootstrap real numbers, so you'll have difficulty using it for more than that.