# Hansen Econometrics Applications

This repository contains application-level Lean formalizations and expository notes built on top of
[`mostlyharmfuleconometrics/lean-hansen-econometrics`](https://github.com/mostlyharmfuleconometrics/lean-hansen-econometrics).

The base Hansen repository is intended to hold reusable econometrics infrastructure and theorem
formalizations. This repository is for applied examples, paper-specific algebra, and longer
walkthrough documents.

## Contents

- [`applications/Angrist1998.lean`](applications/Angrist1998.lean): finite-sample regression algebra
  behind Angrist-style overlap weights.
- [`applications/angrist_1998_regression_weights.md`](applications/angrist_1998_regression_weights.md):
  detailed walkthrough of the Angrist 1998 regression-weights calculation.
- [`applications/MultipleTreatments.lean`](applications/MultipleTreatments.lean): multiple-treatment
  regression-weight identities for simultaneous and one-at-a-time regression adjustment.
- [`applications/multiple_treatments_regression_weights.md`](applications/multiple_treatments_regression_weights.md):
  detailed walkthrough of the multiple-treatment algebra.

PDF exports of the two notes are committed alongside the Markdown sources.

## Build

```sh
lake update
lake build
```

The package imports Hansen as a Lake dependency from the `main` branch of
`mostlyharmfuleconometrics/lean-hansen-econometrics`.