# estimate_tools

**Repository Path**: mingshan/estimate_tools

## Basic Information

- **Project Name**: estimate_tools
- **Description**: No description available
- **Primary Language**: Unknown
- **License**: Not specified
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2025-05-15
- **Last Updated**: 2025-05-15

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# Lean formalization of asymptotic estimates

Will set up the theory of totally ordered real vector spaces, and the ultraproduct construction to correspond this with asymptotic estimates.  Then, develop metaprogramming tactics to prove inequalities in such vector spaces.

- [Web page](https://teorth.github.io/estimate_tools/)
    - [Blueprint](https://teorth.github.io/estimate_tools/blueprint/)
- [Blog post](https://terrytao.wordpress.com/2025/05/01/a-proof-of-concept-tool-to-verify-estimates/)