foldPlusOneStep

formal source

  48  simp [LNALSemantics.voxelStep, foldPlusOneProgram, lStep, -clampI32]
  49
  50/-- The corresponding discrete step on encoded Galerkin coefficients. -/
  51noncomputable def foldPlusOneStep {N : ℕ} (u : GalerkinState N) : GalerkinState N :=
  52  WithLp.toLp 2 (fun i : ((modes N) × Fin 2) =>
  53    let x : ℝ := u i
  54    let m : Int := clampI32 (coeffMag x + 1)
  55    let z : Int := (coeffSign x) * m
  56    (z : ℝ))
  57
  58lemma floor_abs_intCast (z : Int) : Int.floor (|((z : ℝ))|) = |z| := by
  59  have habs : |((z : ℝ))| = ((|z| : Int) : ℝ) := by
  60    simp
  61  rw [habs]
  62  simpa using (Int.floor_intCast (R := ℝ) (z := |z|))
  63
  64lemma cast_lt_zero_iff {z : Int} : ((z : ℝ) < 0) ↔ z < 0 := by
  65  constructor
  66  · intro hz
  67    by_contra h
  68    have : (0 : Int) ≤ z := le_of_not_gt h
  69    have : (0 : ℝ) ≤ (z : ℝ) := by exact_mod_cast this
  70    exact (not_lt_of_ge this) hz
  71  · intro hz
  72    exact_mod_cast hz
  73
  74lemma clampI32_pos_of_ge_one {x : Int} (hx : 1 ≤ x) : 0 < clampI32 x := by
  75  -- From `x ≥ 1`, the negative-saturation branch is impossible; then either we saturate high,
  76  -- or we return `x` itself. In both cases the result is positive.
  77  have hx0 : (0 : Int) ≤ x := le_trans (by decide : (0 : Int) ≤ 1) hx
  78  have hnot : ¬ x ≤ (-i32Bound) := by
  79    have hi : (-i32Bound : Int) < 0 := by
  80      have : (0 : Int) < i32Bound := by decide
  81      linarith