lemma
proved
tactic proof
coeffMag_foldPlusOneStep
show as:
view Lean formalization →
formal statement (Lean)
94lemma coeffMag_foldPlusOneStep {N : ℕ} (u : GalerkinState N) (i : (modes N) × Fin 2) :
95 coeffMag ((foldPlusOneStep u) i) = clampI32 (coeffMag (u i) + 1) := by
proof body
Tactic-mode proof.
96 classical
97 set x : ℝ := u i
98 have hx1 : (1 : Int) ≤ coeffMag x + 1 := by
99 have hx0 : (0 : Int) ≤ coeffMag x := (Int.floor_nonneg (a := |x|)).2 (abs_nonneg x)
100 linarith
101 -- Let `m` be the (positive) clamped magnitude and `z` the signed integer we encode as a real.
102 set m : Int := clampI32 (coeffMag x + 1)
103 set z : Int := coeffSign x * m
104 have hmpos : 0 < m := by
105 simpa [m] using (clampI32_pos_of_ge_one (x := coeffMag x + 1) hx1)
106 have hm0 : 0 ≤ m := le_of_lt hmpos
107 -- Expand `coeffMag` and reduce to a floor/abs fact on an integer cast.
108 -- `foldPlusOneStep u i` is literally `(z : ℝ)`.
109 have hcore :
110 coeffMag ((foldPlusOneStep u) i) = Int.floor (|((z : ℝ))|) := by
111 simp [coeffMag, foldPlusOneStep, x, m, z, -clampI32]
112 -- Now compute the floor of the abs cast and simplify `|z|`.
113 calc
114 coeffMag ((foldPlusOneStep u) i)
115 = Int.floor (|((z : ℝ))|) := hcore
116 _ = |z| := floor_abs_intCast z
117 _ = m := by
118 by_cases hx : x < 0
119 · have hz : z = -m := by simp [z, coeffSign, hx]
120 rw [hz]
121 -- `| -m | = |m| = m` since `m ≥ 0`.
122 simp [abs_of_nonneg hm0]
123 · have hz : z = m := by simp [z, coeffSign, hx]
124 rw [hz]
125 simp [abs_of_nonneg hm0]
126