analysis

Tech stack & purpose

This repository contains formalizations of textbooks on analysis into Lean, a proof assistant language. The main project formalizes "Analysis I," covering foundational mathematics from the natural numbers through limits of sequences, while a companion "Analysis/MeasureTheory" subdirectory formalizes "An Introduction to Measure Theory," addressing topics like Lebesgue measure, integration, and abstract measure spaces. The formalizations are authored by Terence Tao and designed to closely parallel the original textbooks while demonstrating Lean's features; they gradually transition from textbook-specific definitions to Mathlib (Lean's standard mathematics library) definitions as the material progresses, serving as both faithful companions to the texts and introductions to relevant portions of Mathlib.

Community & reference links

• The natural number game
• broader list
• Lean tactics cheat sheet
• List of Mathlib tactics
• LeanCopilot
• Duper
• Common Lean pitfalls
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source
• Lean source

Languages

Contributors (top 30 of 52)

• 
  teorth547 commits · 4,345 followers
• 
  teorth455 commits · 4,345 followers
• 
  Zephyr Fan195 commits · 16 followers
• 
  Taksh Kothari165 commits · 18 followers
• 
  Li Xuanji71 commits · 209 followers
• 
  dan62 commits · 91,233 followers
• 
  Rado Kirov59 commits · 194 followers
• 
  dan39 commits · 91,233 followers
• 
  Pim Otte31 commits · 33 followers
• 
  David Thrane Christiansen18 commits · 585 followers
• 
  Lorenzo Castelli16 commits · 24 followers
• 
  kvanvels11 commits · 1 followers
• 
  euprunin10 commits · 0 followers
• 
  Kim Morrison10 commits · 552 followers
• laurakim12157 commits
• Andrii Kurdiumov5 commits
• Hanson Char4 commits
• 
  Shaunticlair4 commits · 13 followers
• AW-AlanWu3 commits
• Brandon3 commits
• 
  Zhi Kai Pong3 commits · 4 followers
• Georg Pichler3 commits
• 
  Eric Wieser3 commits · 532 followers
• Emanuel Rietveld3 commits
• CharredLee3 commits
• 
  Justin Asher3 commits · 37 followers
• Luni-42 commits
• 数学主义2 commits
• Soham Patil2 commits
• Xiaoyun2 commits