foldPlusOneProgram

formal source

  38-/
  39
  40/-- A nontrivial LNAL program: increment `nuPhi` by `+1` at every instruction pointer. -/
  41@[simp] def foldPlusOneProgram : LProgram :=
  42  fun _ => LInstr.fold 1
  43
  44/-- One-voxel semantics for `foldPlusOneProgram`: increment `nuPhi` by `+1` (clamped); leave `aux5` unchanged. -/
  45lemma voxelStep_foldPlusOneProgram (v : LNALVoxel) :
  46    voxelStep foldPlusOneProgram v = ({ v.1 with nuPhi := clampI32 (v.1.nuPhi + 1) }, v.2) := by
  47  rcases v with ⟨r6, a5⟩
  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