/MATH40002-lean

Analysis I in Lean

Primary LanguageLean

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)