minimum_at_one

formal source

  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
  74  · rw [heq, Jcost_unit0]
  75  · exact le_of_lt (Jcost_pos_of_ne_one r hr hne)
  76
  77structure JPositivityUniversalityCert where
  78  turbulent : TurbulentCost
  79  disease : DiseaseCost
  80  off_target : OffTargetCost
  81  off_game : OffEquilibriumGameCost
  82  arbitrage : MarketArbitrageGap
  83  biased : BiasedReasoningCost
  84  deficit : RecognitionDeficit
  85  all_same : TurbulentCost = DiseaseCost ∧
  86             DiseaseCost = OffTargetCost ∧
  87             OffTargetCost = OffEquilibriumGameCost ∧
  88             OffEquilibriumGameCost = MarketArbitrageGap ∧
  89             MarketArbitrageGap = BiasedReasoningCost ∧
  90             BiasedReasoningCost = RecognitionDeficit
  91  minimum_at_1 : ∀ r : ℝ, 0 < r → Jcost 1 ≤ Jcost r
  92  symmetry : ∀ r : ℝ, 0 < r → Jcost r = Jcost r⁻¹
  93
  94def jPositivityUniversalityCert : JPositivityUniversalityCert where
  95  turbulent := turbulent_cost
  96  disease := disease_cost
  97  off_target := off_target_cost
  98  off_game := off_equilibrium_game_cost
  99  arbitrage := market_arbitrage_gap
 100  biased := biased_reasoning_cost