MATH40002 – Analysis I

Some Analysis I related stuff in Lean.

• src/lemmas.lean contains lemmas related to real numbers.
• src/seq_def.lean contains definitions related to real sequences.
  • Boundedness
  • Limits and convergence
  • Monotonicity
  • Cauchy sequences
  • Subsequences
• src/seq.lean contains examples and propositions.
  • Uniqueness of limits
  • Algebra of limits
  • Monotone convergence theorem
  • Order limit theorem
  • Squeeze theorem
  • Cauchy if and only if convergent
  • Bolzano-Weierstrass theorem
  • Some particular limits (x ^ n, 1 / n ^ k, etc.)
• src/series_def.lean contains definitions related to real series.
  • Partial sums
  • Convergence of series
  • Absolute convergence
• src/series.lean contains examples and propositions.
  • Limit test
  • Comparison tests
  • Alternating series test (WIP)
  • Ratio test (WIP)
  • Root test (WIP)
  • Some particular series (x ^ n, 1 / n, 1 / n ^ 2 etc.)
  • Power series (WIP)
• src/continuity_def.lean contains definitions related to continuity.
  • Limits
  • Continuity
• src/continuity.lean contains examples and propositions
  • Continuous iff sequentially continuous
  • Intermediate Value Theorem (WIP)