SomeProofs

A collection of formal proofs, derivations, and mathematical constructions in economic theory, checked in Lean 4.

This repository exists partly as a working notebook and partly as an attempt to think more rigorously about systems, abstraction, and structure.

Build

lake build

Repository

SomeProofs.lean
SomeProofsTest.lean
SomeProofs/
|- ConsumerTheory/
|  `- Basic.lean
|- ProducerTheory/
|  `- Basic.lean
|- GameTheory/
|  `- Basic.lean
|- GeneralEquilibrium/
|  `- Basic.lean
|- DynamicProg/
|  `- Basic.lean
|- Mathematics/
|  |- Infrastructure.lean
|  |- FixedPoint.lean
|  `- Convexity.lean
|- Econometrics/
|  |- LinearModels.lean
|  `- Asymptotics.lean
`- Utils/
   |- Notations.lean
   |- Tactics.lean
   `- Utils.lean
SomeProofsTest/
`- BudgetCompactness.lean

Proved Theorems

SomeProofs/Mathematics/Infrastructure.lean

• budget_set_compact — For strictly positive prices $p \in \mathbb{R}^n$ and $w \ge 0$, the set ${x \ge 0 \mid p \cdot x \le w} \subset \mathbb{R}^n$ is compact. Proved by embedding in a product of compact intervals. (Mas-Colell, Whinston, & Green, 1995, Proposition 2.D.1)
• utility_maximum_attained — A continuous function on a non-empty compact set attains its maximum. Wrapper around IsCompact.exists_isMaxOn. (Mas-Colell et al., 1995, Theorem M.C.1)

SomeProofs/Mathematics/FixedPoint.lean

• standardSimplex — Definition of the standard $n$-simplex $\Delta^n = {x \in \mathbb{R}^{n+1} \mid x \ge 0,\ \sum x_i = 1}$ with proofs of non-emptiness and convexity.
• brouwer_fixed_point_interval — Any continuous $f: [0,1] \to [0,1]$ has a fixed point. Proved by applying the intermediate value theorem to $g(x) = f(x) - x$. (Mas-Colell et al., 1995, Appendix M.I)
• brouwer_fixed_point_simplex — Brouwer fixed point theorem for the standard $n$-simplex. (Stated — full proof via Sperner's lemma pending.)
• brouwer_fixed_point_bridge — Brouwer fixed point theorem for any non-empty compact convex $C \subset \mathbb{R}^n$. (Stated.)
• kakutani_fixed_point_bridge — Fixed point theorem for convex-valued, upper hemicontinuous correspondences on compact convex sets. (Stated.)

SomeProofs/Mathematics/Convexity.lean

• envelope_theorem — For a parameterised optimisation problem $V(\theta) = \max_x f(x, \theta)$, the total derivative equals the partial derivative at the optimum: $V'(\theta) = \partial f / \partial \theta, (x^*(\theta), \theta)$. (Stated.) (Mas-Colell et al., 1995, Appendix M.L)
• kkt_sufficiency — For a concave objective on convex constraints, any point satisfying the KKT first-order conditions is a global maximiser. Signature uses ConcaveOn/ConvexOn from mathlib. (Stated.) (Mas-Colell et al., 1995, Appendix M.K)

SomeProofs/ConsumerTheory/Basic.lean

• PreferenceRelation — Typeclass providing weak, strict, and indiff binary relations over a type $\alpha$. (Mas-Colell et al., 1995, Chapter 1.B)
• preference_complete — $\forall x, y,; x \succcurlyeq y \lor y \succcurlyeq x$. (Mas-Colell et al., 1995, Definition 1.B.1)
• preference_transitive — $\forall x, y, z,; (x \succcurlyeq y \land y \succcurlyeq z) \Rightarrow x \succcurlyeq z$. (Mas-Colell et al., 1995, Definition 1.B.1)
• preference_continuous — For every $y$, the sets ${x \mid x \succcurlyeq y}$ and ${x \mid y \succcurlyeq x}$ are closed. (Mas-Colell et al., 1995, Definition 3.C.1)
• local_non_satiation — For every $x \in X$ and neighbourhood $U$ of $x$, there exists $y \in U \cap X$ with $y \succ x$. (Mas-Colell et al., 1995, Definition 3.B.3)
• preference_convex — If $x \succcurlyeq z$ and $y \succcurlyeq z$, then $t x + (1-t) y \succcurlyeq z$ for all $t \in [0,1]$. Equivalently, upper contour sets are convex. (Mas-Colell et al., 1995, Definition 3.B.4)
• preference_monotone — $y \le x$ (component-wise) $\Rightarrow x \succcurlyeq y$. (Mas-Colell et al., 1995, Definition 3.B.2)
• preference_strictly_monotone — $y \le x$ and $x \ne y$ $\Rightarrow x \succ y$.
• UtilityRepresentation — Structure bundling a continuous $u: X \to \mathbb{R}$ with $u(x) \ge u(y) \iff x \succcurlyeq y$. (Mas-Colell et al., 1995, Section 3.C)
• commodity_space — The set $\mathbb{R}^n_+$ of non-negative consumption vectors.
• BudgetSet — Structure bundling prices $p \in \mathbb{R}^n_{++}$ and wealth $w \ge 0$ with proofs of positivity. (Mas-Colell et al., 1995, Definition 2.D.1)
• budget_set — $B(p,w) = {x \ge 0 \mid p \cdot x \le w}$.
• compact_budget_set — $B(p,w)$ is compact. Wrapper around budget_set_compact.
• budget_set_nonempty — $0 \in B(p,w)$.
• marshallian_demand — $x(p,w) = {x \in B(p,w) \mid x \succcurlyeq y \text{ for all } y \in B(p,w)}$. (Mas-Colell et al., 1995, Definition 2.D.1)
• marshallian_demand_nonempty — If preferences have a continuous utility representation, Marshallian demand is non-empty. (Mas-Colell et al., 1995, Proposition 3.D.1)
• walras_law — Under local non-satiation, $p \cdot x = w$ for any $x \in x(p,w)$. (Mas-Colell et al., 1995, Proposition 3.D.2)
• budget_set_homogeneous — $B(\lambda p, \lambda w) = B(p,w)$ for any $\lambda > 0$.
• demand_homogeneous_degree_zero — $x(\lambda p, \lambda w) = x(p,w)$ for any $\lambda > 0$. (Mas-Colell et al., 1995, Definition 2.D.2)
• indirect_utility — $v(p,w) = \max{u(x) \mid x \in B(p,w)}$. (Mas-Colell et al., 1995, Definition 3.D.1)

SomeProofs/ProducerTheory/Basic.lean

• ProductionSet — A closed set $Y \subset \mathbb{R}^n$ of feasible net-output vectors. (Mas-Colell et al., 1995, Chapter 5.B)
• profit_function — $\pi(p) = \sup{, p \cdot y \mid y \in Y ,}$. (Mas-Colell et al., 1995, Definition 5.C.1)
• supply_correspondence — $y(p) = {, y \in Y \mid p \cdot y \ge p \cdot y' \text{ for all } y' \in Y ,}$. (Mas-Colell et al., 1995, Definition 5.C.1)
• hotellings_lemma — The derivative of the profit function recovers net supplies. (Stated.) (Mas-Colell et al., 1995, Lemma 5.C.1)
• law_of_supply — If $y$ maximises profit at $p$ and $y'$ at $p'$, then $(p' - p) \cdot (y' - y) \ge 0$. Proved by expanding the product and using the profit-maximisation inequalities. (Mas-Colell et al., 1995, Proposition 5.C.1)

SomeProofs/GeneralEquilibrium/Basic.lean

• ExchangeEconomy — Structure with $m$ agents, each with an endowment vector in $\mathbb{R}^n_+$. (Mas-Colell et al., 1995, Chapter 15.B)
• WalrasianEquilibrium — Structure: prices $p \gg 0$ and allocation ${x_a}$ such that each agent's bundle is affordable and markets clear $\sum_a x_a = \sum_a e_a$. (Mas-Colell et al., 1995, Definition 15.B.1)
• first_welfare_theorem — Every Walrasian equilibrium is Pareto efficient under local non-satiation. (Stated.) (Mas-Colell et al., 1995, Theorem 16.C.1)
• second_welfare_theorem — Every Pareto optimum can be decentralised as a Walrasian equilibrium with transfers. (Stated.) (Mas-Colell et al., 1995, Theorem 16.D.1)
• arrow_debreu_existence — A Walrasian equilibrium exists under standard assumptions. (Stated.) (Mas-Colell et al., 1995, Chapter 17.C)

SomeProofs/GameTheory/Basic.lean

• StrategicGame — $n$ players, each with strategy set $S_i \subseteq \mathbb{R}^m$ and payoff $u_i: \prod_j S_j \to \mathbb{R}$. (Mas-Colell et al., 1995, Chapter 7.D)
• nash_existence_finite — Every finite strategic-form game has at least one Nash equilibrium in mixed strategies. (Stated — requires Kakutani fixed point.) (Mas-Colell et al., 1995, Proposition 8.D.1)

SomeProofs/DynamicProg/Basic.lean

• DynamicProgram — Structure bundling state space $S$, action space $A$, transition $g: S \times A \to S$, and payoff $r: S \times A \to \mathbb{R}$. (Ljungqvist & Sargent, 2004, Chapter 3)
• bellman_contraction — The Bellman operator $T v(s) = \max_a{ r(s,a) + \beta v(g(s,a)) }$ is a contraction mapping under Blackwell's conditions. (Stated.) (Stokey, Lucas, & Prescott, 1989, Theorem 4.2)
• principle_of_optimality — The fixed point of the Bellman operator equals the supremum of the sequence problem. (Stated.) (Stokey, Lucas, & Prescott, 1989, Theorem 4.3)

SomeProofs/Econometrics/LinearModels.lean

• LinearRegression — Structure: $y = X\beta + \varepsilon$ with $n$ observations and $k$ regressors. (Greene, 2012, Chapter 2)
• gauss_markov — Under the Gauss-Markov assumptions, the OLS estimator is the best linear unbiased estimator (BLUE). (Stated.) (Greene, 2012, Theorem 2.3)
• frisch_waugh_lovell — The coefficients from a partitioned regression can be obtained by partialling out the other regressors. (Stated.) (Greene, 2012, Theorem 2.5)

SomeProofs/Econometrics/Asymptotics.lean

• ols_consistency — Under standard exogeneity assumptions, OLS converges in probability to $\beta$. (Stated.) (Greene, 2012, Chapter 4; Hayashi, 2000, Chapter 2)

Utils

| Notations.lean | x ≽ y (weak pref.), x ≻ y (strict pref.), x ∼ y (indifference) | | Tactics.lean | econ_simp (simp attribute), solve_budget (budget constraints), solve_foc (first-order conditions) |

Tests

| BudgetCompactness.lean | Verifies that with $p = (2, 3)$ and $w = 12$, ${x \ge 0 \mid 2x_0 + 3x_1 \le 12}$ is compact and non-empty. |

Theorems Awaiting Proof

Stated as theorem signatures with trivial bodies. Each requires a standard proof.

Theorem	Prerequisite
brouwer_fixed_point_simplex (n ≥ 2)	Sperner's lemma
kakutani_fixed_point_bridge	Brouwer + approximation
kkt_sufficiency	Convex analysis, subgradient calculus
envelope_theorem	Calculus in normed spaces
first_welfare_theorem	LNS + Walrasian equilibrium
second_welfare_theorem	Separating hyperplane theorem
arrow_debreu_existence	Kakutani + excess demand
nash_existence_finite	Kakutani + best-reply correspondence
bellman_contraction	Blackwell's sufficient conditions
gauss_markov	Linear algebra, expectation calculus
ols_consistency	Laws of large numbers

References

1. Border, K. C. (1985). Fixed point theorems with applications to economics and game theory. Cambridge University Press.
2. Boyd, S., & Vandenberghe, L. (2004). Convex optimization. Cambridge University Press.
3. Greene, W. H. (2012). Econometric analysis (7th ed.). Pearson.
4. Hayashi, F. (2000). Econometrics. Princeton University Press.
5. Ljungqvist, L., & Sargent, T. J. (2004). Recursive macroeconomic theory (2nd ed.). MIT Press.
6. Mas-Colell, A., Whinston, M. D., & Green, J. R. (1995). Microeconomic theory. Oxford University Press.
7. Stokey, N. L., Lucas, R. E., & Prescott, E. C. (1989). Recursive methods in economic dynamics. Harvard University Press.