decide_lt_zero_foldPlusOneStep

formal source

 163      exact not_lt_of_ge hy0
 164    simp [coeffSign, hx, hy, x]
 165
 166lemma decide_lt_zero_foldPlusOneStep {N : ℕ} (u : GalerkinState N) (i : (modes N) × Fin 2) :
 167    decide ((foldPlusOneStep u) i < 0) = decide (u i < 0) := by
 168  classical
 169  set x : ℝ := u i
 170  have hx1 : (1 : Int) ≤ coeffMag x + 1 := by
 171    have hx0 : (0 : Int) ≤ coeffMag x := (Int.floor_nonneg (a := |x|)).2 (abs_nonneg x)
 172    linarith
 173  have hmpos : 0 < clampI32 (coeffMag x + 1) :=
 174    clampI32_pos_of_ge_one (x := coeffMag x + 1) hx1
 175  by_cases hx : x < 0
 176  ·
 177    have hzInt : (coeffSign x) * clampI32 (coeffMag x + 1) < 0 := by
 178      have hneg : -(clampI32 (coeffMag x + 1)) < 0 := neg_neg_of_pos hmpos
 179      calc
 180        (coeffSign x) * clampI32 (coeffMag x + 1)
 181            = (-1) * clampI32 (coeffMag x + 1) := by simp [coeffSign, hx]
 182        _ = -(clampI32 (coeffMag x + 1)) := by ring
 183        _ < 0 := hneg
 184    have hzReal :
 185        (((coeffSign x) * clampI32 (coeffMag x + 1) : Int) : ℝ) < 0 :=
 186      (cast_lt_zero_iff (z := (coeffSign x) * clampI32 (coeffMag x + 1))).2 hzInt
 187    have hy : (foldPlusOneStep u) i < 0 := by
 188      simpa [foldPlusOneStep, x] using hzReal
 189    simp [x, hx, hy]
 190  ·
 191    have hzInt : (0 : Int) ≤ (coeffSign x) * clampI32 (coeffMag x + 1) := by
 192      have hm0 : (0 : Int) ≤ clampI32 (coeffMag x + 1) := le_of_lt hmpos
 193      simpa [coeffSign, hx] using hm0
 194    have hzReal :
 195        (0 : ℝ) ≤ (((coeffSign x) * clampI32 (coeffMag x + 1) : Int) : ℝ) := by
 196      exact_mod_cast hzInt