Economics
Economics modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
Economics.BehavioralEconomicsFromRS |
3 | 0 | 1 | 46 | — |
Economics.BusinessCycleFromPhiLadder |
2 | 0 | 2 | 48 | — |
Economics.BusinessCyclePeriodFromGap45 |
9 | 0 | 4 | 140 | — |
Economics.CounterCyclicalPolicyFromGap45 |
3 | 0 | 4 | 68 | — |
Economics.CounterCyclicalPolicyFromJCost |
0 | 0 | 1 | 32 | — |
Economics.FinancialCrisisRegimesFromJCost |
1 | 0 | 1 | 35 | — |
Economics.FinancialMarketsFromRS |
3 | 0 | 1 | 52 | — |
Economics.GameTheoryFromRS |
3 | 0 | 1 | 48 | — |
Economics.HealthEconomicsFromRS |
3 | 0 | 1 | 51 | — |
Economics.InequalityCeilingFromSigma |
3 | 0 | 2 | 65 | — |
Economics.InequalityFromSigmaBudget |
0 | 0 | 1 | 35 | — |
Economics.InnovationDiffusionFromPhiLadder |
2 | 0 | 2 | 48 | — |
Economics.LaborEconomicsFromRS |
3 | 0 | 1 | 45 | — |
Economics.LorenzCurveFromSigmaBudget |
6 | 0 | 5 | 98 | — |
Economics.MarketMicrostructureFromJCost |
1 | 0 | 1 | 33 | — |
Economics.MonetaryPolicyToolsFromConfigDim |
1 | 0 | 1 | 33 | — |
Economics.NashEquilibriumTypesFromConfigDim |
1 | 0 | 1 | 36 | — |
Economics.SupplyChainFromRS |
2 | 0 | 1 | 39 | — |
Economics.TaxOptimizationFromJCost |
1 | 0 | 1 | 39 | — |
Economics.WealthDistributionFromSigma |
3 | 0 | 2 | 57 | — |