Real Analysis Exercises

Introduction

This page contains exercises in Real Analysis, focusing on sequences and series. Each exercise includes a pre-loaded Lean template to help you formalize your solutions.

Recall that a sequence \(\{a_n\}\) is simply a function, \(a : \mathbb N \to \mathbb R\). We say that it \(\operatorname{convergesTo}\) \(L : \mathbb R\) if for all epsilon ... and it \(\operatorname{converges}\) if such an \(L\) exists.

Exercise 1: Convergence and Absolute Value

Exercise 1.1: Prove that convergence of \(\{s_n\}\) implies convergence of \(\{|s_n|\}\). Is the converse true?

Exercise 2: Limit Calculation

Exercise 2.1: Calculate \(\lim_{n \to \infty} (\sqrt{n^2 + n} - n)\).

Exercise 3: Recursive Sequences

Exercise 3.1: If \(s_1 = \sqrt{2}\), and \(s_{n+1} = \sqrt{2 + \sqrt{s_n}}\) for \(n = 1, 2, 3, \ldots\), prove that \(\{s_n\}\) converges, and that \(s_n < 2\) for \(n = 1, 2, 3, \ldots\)