pith. machine review for the scientific record. sign in
theorem proved tactic proof

recidivismRate_decay

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  32theorem recidivismRate_decay (k : ℕ) :
  33    recidivismRateAtYear (k + 1) < recidivismRateAtYear k := by

proof body

Tactic-mode proof.

  34  unfold recidivismRateAtYear
  35  have hphi_ne := phi_ne_zero
  36  have hpos : 0 < phi ^ (-(k : ℤ)) := zpow_pos phi_pos _
  37  rw [show ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 from by push_cast; ring]
  38  rw [show -((k : ℤ) + 1) = -(k : ℤ) + (-1 : ℤ) from by ring]
  39  rw [zpow_add₀ hphi_ne]
  40  have hphi_inv_lt1 : phi ^ (-1 : ℤ) < 1 := by
  41    simp [zpow_neg, inv_lt_one_of_one_lt₀ one_lt_phi]
  42  calc phi ^ (-(k : ℤ)) * phi ^ (-1 : ℤ)
  43      < phi ^ (-(k : ℤ)) * 1 := by
  44        apply mul_lt_mul_of_pos_left hphi_inv_lt1 hpos
  45    _ = phi ^ (-(k : ℤ)) := mul_one _
  46

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.