`BehavioralFinding`

definition

show as: view math explainer →

module: IndisputableMonolith.Economics.BehavioralEconomicsFromRS
domain: Economics
line: 22 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Economics.BehavioralEconomicsFromRS on GitHub at line 22.

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

  19namespace IndisputableMonolith.Economics.BehavioralEconomicsFromRS
  20open Cost
  21
  22inductive BehavioralFinding where
  23  | lossAversion | anchoring | hyperbolicDiscounting | herding | overconfidence
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem behavioralFindingCount : Fintype.card BehavioralFinding = 5 := by decide
  27
  28/-- Rational agent: J = 0. -/
  29theorem rational_agent : Jcost 1 = 0 := Jcost_unit0
  30
  31/-- Biased agent: J > 0. -/
  32theorem biased_agent {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  33    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  34
  35structure BehavioralEconomicsCert where
  36  five_findings : Fintype.card BehavioralFinding = 5
  37  rational : Jcost 1 = 0
  38  biased : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  39
  40def behavioralEconomicsCert : BehavioralEconomicsCert where
  41  five_findings := behavioralFindingCount
  42  rational := rational_agent
  43  biased := biased_agent
  44
  45end IndisputableMonolith.Economics.BehavioralEconomicsFromRS

papers checked against this theorem

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