`AssetClass`

definition

show as: view math explainer →

module: IndisputableMonolith.Economics.FinancialMarketsFromRS
domain: Economics
line: 26 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Economics.FinancialMarketsFromRS on GitHub at line 26.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  23namespace IndisputableMonolith.Economics.FinancialMarketsFromRS
  24open Cost
  25
  26inductive AssetClass where
  27  | equities | bonds | commodities | currencies | realEstate
  28  deriving DecidableEq, Repr, BEq, Fintype
  29
  30theorem assetClassCount : Fintype.card AssetClass = 5 := by decide
  31
  32inductive FinancialRisk where
  33  | market | credit | liquidity | operational | systemic
  34  deriving DecidableEq, Repr, BEq, Fintype
  35
  36theorem financialRiskCount : Fintype.card FinancialRisk = 5 := by decide
  37
  38/-- Market equilibrium: J = 0. -/
  39theorem market_equilibrium : Jcost 1 = 0 := Jcost_unit0
  40
  41structure FinancialMarketsCert where
  42  five_classes : Fintype.card AssetClass = 5
  43  five_risks : Fintype.card FinancialRisk = 5
  44  equilibrium : Jcost 1 = 0
  45
  46def financialMarketsCert : FinancialMarketsCert where
  47  five_classes := assetClassCount
  48  five_risks := financialRiskCount
  49  equilibrium := market_equilibrium
  50
  51end IndisputableMonolith.Economics.FinancialMarketsFromRS

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.