`FinancialRisk`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Economics.FinancialMarketsFromRS on GitHub at line 32.

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

  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.