disease_cost

formal source

  40def RecognitionDeficit : Prop := ∀ r : ℝ, 0 < r → r ≠ 1 → 0 < Jcost r
  41
  42theorem turbulent_cost : TurbulentCost := fun r hr hne => Jcost_pos_of_ne_one r hr hne
  43theorem disease_cost : DiseaseCost := fun r hr hne => Jcost_pos_of_ne_one r hr hne
  44theorem off_target_cost : OffTargetCost := fun r hr hne => Jcost_pos_of_ne_one r hr hne
  45theorem off_equilibrium_game_cost : OffEquilibriumGameCost :=
  46  fun r hr hne => Jcost_pos_of_ne_one r hr hne
  47theorem market_arbitrage_gap : MarketArbitrageGap :=
  48  fun r hr hne => Jcost_pos_of_ne_one r hr hne
  49theorem biased_reasoning_cost : BiasedReasoningCost :=
  50  fun r hr hne => Jcost_pos_of_ne_one r hr hne
  51theorem recognition_deficit : RecognitionDeficit :=
  52  fun r hr hne => Jcost_pos_of_ne_one r hr hne
  53
  54/-! ## Universality: all seven are definitionally the same proposition. -/
  55
  56theorem all_seven_are_one :
  57    TurbulentCost = DiseaseCost ∧
  58    DiseaseCost = OffTargetCost ∧
  59    OffTargetCost = OffEquilibriumGameCost ∧
  60    OffEquilibriumGameCost = MarketArbitrageGap ∧
  61    MarketArbitrageGap = BiasedReasoningCost ∧
  62    BiasedReasoningCost = RecognitionDeficit :=
  63  ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩
  64
  65/-- J-cost is symmetric around r = 1: J(r) = J(r⁻¹). -/
  66theorem symmetry_at_equilibrium (r : ℝ) (hr : 0 < r) : Jcost r = Jcost r⁻¹ :=
  67  Jcost_symm hr
  68
  69/-- The minimum of J on (0, ∞) is at r = 1, value 0. -/
  70theorem minimum_at_one : ∀ r : ℝ, 0 < r → Jcost 1 ≤ Jcost r := by
  71  intro r hr
  72  rw [Jcost_unit0]
  73  rcases eq_or_ne r 1 with heq | hne