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

complexDemand_ge

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)

 171theorem complexDemand_ge {L : ℝ} (hL : 0 < L) (Z : ℤ) :
 172    maintenanceDemand L ≤ complexDemand L Z := by

proof body

Tactic-mode proof.

 173  unfold complexDemand
 174  have hd := maintenanceDemand_nonneg hL
 175  have hfac : 1 ≤ 1 + ↑|Z| * k_R := by
 176    have : 0 ≤ ↑|Z| * k_R := mul_nonneg (by exact_mod_cast abs_nonneg Z) (le_of_lt k_R_pos)
 177    linarith
 178  calc maintenanceDemand L
 179      = maintenanceDemand L * 1 := (mul_one _).symm
 180    _ ≤ maintenanceDemand L * (1 + ↑|Z| * k_R) := by
 181        apply mul_le_mul_of_nonneg_left hfac hd
 182
 183/-- Higher Z-complexity strictly increases demand (when J > 0). -/

depends on (12)

Lean names referenced from this declaration's body.