Missing exercise 5.1.2

Stream: Analysis I

[Rado Kirov]

The exercise in fourth edition states:

If a^∞_n=1 and b^∞_n=1 are bounded sequences, show that (an + bn)^∞_n=1, ... are also bounded.

I am going to add it, but since we slightly generalize Sequences to start at any whole number n_0, but sure which form would be better

theorem Sequence.isBounded_of_add {a b:Sequence} (ha: a.IsBounded) (hb: b.IsBounded) :
    (Sequence.mk' 1 (fun n ↦ a n + b n)).IsBounded := by sorry

or maybe something like

theorem Sequence.isBounded_of_add {a b:Sequence} (ha: a.IsBounded) (hb: b.IsBounded) :
    (Sequence.mk' (min a.n₀ b.n₀) (fun n ↦ a n + b n)).IsBounded

or even

theorem Sequence.isBounded_of_add {a b:Sequence} (ha: a.IsBounded) (hb: b.IsBounded)
  (ha: a.n₀ = 1) (hb: b.n₀ = 1) :
    (Sequence.mk' 1 (fun n ↦ a n + b n)).IsBounded := by sorry

i think they are all true and provable, but the first one is probably a bit annoying, because one has to adjust for these finite parts where we might be adding zero.

[Terence Tao]

Thanks for the catch! (I had been using an older edition of the book as reference which did not have that exercise.) In general I've adjusted sequences in the companion to start from 0 by default rather than from 1, so something like

theorem Sequence.isBounded_of_add {a b:ℕ → ℚ} (ha: (a:Sequence).IsBounded) (hb: (b:Sequence).IsBounded) :
    (a+b:Sequence).IsBounded := by sorry

should work.

[Rado Kirov]

I see, explicitly build Sequence from functions from N, which sets n0 = 0, makes sense. Will send a PR shortly

[Li Xuanji]

Maybe it should be named IsBounded.add? My understanding is _of is only used for hypotheses

[Rado Kirov]

Yeah I changed it in the PR