cauchy subsequences

Stream: new members

[Alex Kontorovich]

Hello, can someone please help me prove this (I assume it's in mathlib? subsequence of abs converging sequence is also convergent)

def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m

def cauchy_sequence (u : ℕ → α) := ∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε

def partial_sum [has_zero α] [has_add α]  (seq: ℕ → α) : ℕ → α
| (nat.zero  ) := 0
| (nat.succ n) := seq n + partial_sum n


lemma subseq_cauchy_is_cauchy (s:ℕ → α)  (nonneg : ∀ n, 0 ≤ s n) (φ : ℕ → ℕ ) (incφ : extraction φ)
    : cauchy_sequence (partial_sum s)
    → cauchy_sequence (partial_sum (s∘φ)) :=
begin
  sorry,
end

[Kevin Buzzard]

This looks like a fun exercise. I'd recommend you use <= not >= in your definition of Cauchy sequence. I doubt it's in mathlib and even if it is it would be in there using some mathlib definition of Cauchy rather than your home-rolled one

[Kevin Buzzard]

Wait -- is this true?

[Kevin Buzzard]

How about 1-1+1/2-1/2+1/3-1/3+...?

[Kevin Buzzard]

Oh I just spotted the positivity condition :-)

[Kevin Buzzard]

I would be tempted to define a function representing the sum from a to b and prove that under the positivity condition the subsequence sum from a to b was at most the original sum from phi a to phi b

[Kevin Buzzard]

Then you're home by monotonicity of phi

[Alex Kontorovich]

Yes, thanks; I was hoping to quote something in mathlib, but if it's not there, it'll be a fun (?) exercise (which I guess I'll get to now)...

Why aren't basic facts about series (as opposed to sequences) in mathlib?...

[Kevin Buzzard]

Formalising it will be a bit annoying. Humans have a very good intuitive picture of a subsequence, and would write things such as a(phi n) + a(phi(n+1))+...+a(phi(m)) <= a(phi n) + a(phi(n) + 1) + ...+a(phi(m)) but this is actually some tedious induction

[Kevin Buzzard]

People have defined exp(x) as an infinite sum so there must be stuff about infinite sums in there somewhere

[Patrick Massot]

docs#cauchy_seq and docs#tendsto_subseq_of_bounded are probably good entry points

[Patrick Massot]

About series, we discussed building a specialized theory for them but it didn't happen yet. However you shouldn't define your own partial_sum. See docs#harmonic_tendsto_at_top for inspiration.

[Patrick Massot]

Returning to your question, maybe I'm blind but it looks like one more little hole in the library:

lemma cauchy_seq.subseq {α : Type*} [uniform_space α]
  {S : ℕ → α} {φ : ℕ → ℕ} (hS : cauchy_seq S) (hφ : strict_mono φ) :
  cauchy_seq (S ∘ φ) :=
begin
  have limφ : tendsto φ at_top at_top := strict_mono_tendsto_at_top hφ,
  have : tendsto (prod.map φ φ) at_top at_top,
  { rw ← prod_at_top_at_top_eq,
    exact limφ.prod_map limφ, },
  rw cauchy_seq_iff_tendsto at *,
  exact hS.comp this,
end

[Patrick Massot]

One last comment about how you were meant to find answers (beyond asking here which is fine). Since this is elementary stuff, you got to https://leanprover-community.github.io/undergrad.html, open "Single Variable Real Analysis" and then "Sequences of real numbers" to see "Cauchy sequences" mentioned. You can then click on that and wander around.

[Kevin Buzzard]

@Patrick Massot this lemma won't answer @Alex Kontorovich 's question, because a subsequence of the sequence doesn't give a subsequence of the partial sums :-/

[Patrick Massot]

Oh, I read too quickly

[Kevin Buzzard]

yeah and me, I accused him of asking us to prove something false :-) It looks like a real bore

[Patrick Massot]

No, it follows easily from what I wrote.

[Patrick Massot]

or maybe not. I'll leave that as an exercise :wink: