recidivismCost_at_equilibrium

formal source

  39def recidivismCost (reoffense baseline : ℝ) : ℝ :=
  40  Jcost (reoffense / baseline)
  41
  42theorem recidivismCost_at_equilibrium (r : ℝ) (h : r ≠ 0) :
  43    recidivismCost r r = 0 := by
  44  unfold recidivismCost; rw [div_self h]; exact Jcost_unit0
  45
  46theorem recidivismCost_nonneg (reoffense baseline : ℝ)
  47    (hr : 0 < reoffense) (hb : 0 < baseline) :
  48    0 ≤ recidivismCost reoffense baseline := by
  49  unfold recidivismCost; exact Jcost_nonneg (div_pos hr hb)
  50
  51theorem recidivismCost_reciprocal (reoffense baseline : ℝ)
  52    (hr : 0 < reoffense) (hb : 0 < baseline) :
  53    recidivismCost reoffense baseline = recidivismCost baseline reoffense := by
  54  unfold recidivismCost
  55  have h : Jcost (reoffense / baseline) = Jcost (baseline / reoffense) := by
  56    rw [Jcost_reciprocal (div_pos hr hb)]
  57    congr 1; field_simp [hb.ne', hr.ne']
  58  exact h
  59
  60theorem recidivismCost_phi_step :
  61    Jcost phi = phi - 3 / 2 := by
  62  exact Jcost_phi_val
  63
  64structure RecidivismCert where
  65  cost_at_equilibrium : ∀ r : ℝ, r ≠ 0 → recidivismCost r r = 0
  66  cost_nonneg : ∀ r b : ℝ, 0 < r → 0 < b → 0 ≤ recidivismCost r b
  67  cost_reciprocal : ∀ r b : ℝ, 0 < r → 0 < b →
  68    recidivismCost r b = recidivismCost b r
  69  phi_step : Jcost phi = phi - 3 / 2
  70
  71noncomputable def cert : RecidivismCert where
  72  cost_at_equilibrium := recidivismCost_at_equilibrium