behavioralFindingCount

formal source

  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