coeffSign_foldPlusOneStep

proof body

Tactic-mode proof.

 129  classical
 130  set x : ℝ := u i
 131  have hx1 : (1 : Int) ≤ coeffMag x + 1 := by
 132    have hx0 : (0 : Int) ≤ coeffMag x := (Int.floor_nonneg (a := |x|)).2 (abs_nonneg x)
 133    linarith
 134  have hmpos : 0 < clampI32 (coeffMag x + 1) :=
 135    clampI32_pos_of_ge_one (x := coeffMag x + 1) hx1
 136  by_cases hx : x < 0
 137  ·
 138    -- `x < 0` ⇒ `coeffSign x = -1`, and the step coefficient is negative (since the magnitude is positive).
 139    have hzInt : (coeffSign x) * clampI32 (coeffMag x + 1) < 0 := by
 140      have hneg : -(clampI32 (coeffMag x + 1)) < 0 := neg_neg_of_pos hmpos
 141      calc
 142        (coeffSign x) * clampI32 (coeffMag x + 1)
 143            = (-1) * clampI32 (coeffMag x + 1) := by simp [coeffSign, hx]
 144        _ = -(clampI32 (coeffMag x + 1)) := by ring
 145        _ < 0 := hneg
 146    have hzReal :
 147        (((coeffSign x) * clampI32 (coeffMag x + 1) : Int) : ℝ) < 0 :=
 148      (cast_lt_zero_iff (z := (coeffSign x) * clampI32 (coeffMag x + 1))).2 hzInt
 149    have hy : (foldPlusOneStep u) i < 0 := by
 150      simpa [foldPlusOneStep, x] using hzReal
 151    simp [coeffSign, hx, hy, x]
 152  ·
 153    -- `¬ x < 0` ⇒ `coeffSign x = 1`, and the step coefficient is nonnegative.
 154    have hzInt : (0 : Int) ≤ (coeffSign x) * clampI32 (coeffMag x + 1) := by
 155      have hm0 : (0 : Int) ≤ clampI32 (coeffMag x + 1) := le_of_lt hmpos
 156      simpa [coeffSign, hx] using hm0
 157    have hzReal :
 158        (0 : ℝ) ≤ (((coeffSign x) * clampI32 (coeffMag x + 1) : Int) : ℝ) := by
 159      exact_mod_cast hzInt
 160    have hy : ¬ (foldPlusOneStep u) i < 0 := by
 161      have hy0 : (0 : ℝ) ≤ (foldPlusOneStep u) i := by
 162        simpa [foldPlusOneStep, x] using hzReal
 163      exact not_lt_of_ge hy0
 164    simp [coeffSign, hx, hy, x]
 165