feat: lemmas about rounding dyadics (#10138)

This PR adds lemmas about the `Dyadic.roundUp` and `Dyadic.roundDown`
operations.

src/Init/Data/Dyadic.lean

@@ -8,3 +8,4 @@ prelude
 
 public import Init.Data.Dyadic.Basic
 public import Init.Data.Dyadic.Instances
+public import Init.Data.Dyadic.Round

src/Init/Data/Dyadic/Basic.lean

@@ -399,9 +399,21 @@ theorem ofIntWithPrec_shiftLeft_add {n : Nat} :
       Int.add_comm x.trailingZeros n, ← Int.sub_sub]
 
 /-- The "precision" of a dyadic number, i.e. in `n * 2^(-p)` with `n` odd the precision is `p`. -/
-def precision : Dyadic → Int
-  | .zero => 0
-  | .ofOdd _ p _ => p
+-- TODO: If `WithBot` is upstreamed, replace this with `WithBot Int`.
+def precision : Dyadic → Option Int
+  | .zero => none
+  | .ofOdd _ p _ => some p
+
+theorem precision_ofIntWithPrec_le {i : Int} (h : i ≠ 0) (prec : Int) :
+    (ofIntWithPrec i prec).precision ≤ some prec := by
+  simp [ofIntWithPrec, h, precision]
+  omega
+
+@[simp] theorem precision_zero : (0 : Dyadic).precision = none := rfl
+@[simp] theorem precision_neg {x : Dyadic} : (-x).precision = x.precision :=
+  match x with
+  | .zero => rfl
+  | .ofOdd _ _ _ => rfl
 
 /--
 Convert a rational number `x` to the greatest dyadic number with precision at most `prec`
@@ -441,7 +453,7 @@ def roundDown (x : Dyadic) (prec : Int) : Dyadic :=
     | .ofNat l => .ofIntWithPrec (n >>> l) prec
     | .negSucc _ => x
 
-theorem roundDown_eq_self_of_le {x : Dyadic} {prec : Int} (h : x.precision ≤ prec) :
+theorem roundDown_eq_self_of_le {x : Dyadic} {prec : Int} (h : x.precision ≤ some prec) :
     roundDown x prec = x := by
   rcases x with _ | ⟨n, k, hn⟩
   · rfl
@@ -627,4 +639,21 @@ instance : Std.IsLinearPreorder Dyadic where
 
 instance : Std.IsLinearOrder Dyadic where
 
+/-- `roundUp x prec` is the least dyadic number with precision at most `prec` which is greater than or equal to `x`. -/
+def roundUp (x : Dyadic) (prec : Int) : Dyadic :=
+  match x with
+  | .zero => .zero
+  | .ofOdd n k _ =>
+    match k - prec with
+    | .ofNat l => .ofIntWithPrec (-((-n) >>> l)) prec
+    | .negSucc _ => x
+
+theorem roundUp_eq_neg_roundDown_neg (x : Dyadic) (prec : Int) :
+    x.roundUp prec = -((-x).roundDown prec) := by
+  rcases x with _ | ⟨n, k, hn⟩
+  · rfl
+  · change _ = -(ofOdd ..).roundDown prec
+    rw [roundDown, roundUp]
+    split <;> simp
+
 end Dyadic

src/Init/Data/Dyadic/Round.lean

@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+public import Init.Data.Dyadic.Basic
+import all Init.Data.Dyadic.Instances
+import Init.Data.Int.Bitwise.Lemmas
+import Init.Grind.Ordered.Rat
+import Init.Grind.Ordered.Field
+
+namespace Dyadic
+
+/-!
+Theorems about `roundUp` and `roundDown`.
+-/
+
+public section
+
+theorem roundDown_le {x : Dyadic} {prec : Int} : roundDown x prec ≤ x :=
+  match x with
+  | .zero => Dyadic.le_refl _
+  | .ofOdd n k _ => by
+    unfold roundDown
+    dsimp
+    match h : k - prec with
+    | .ofNat l =>
+      dsimp
+      rw [ofOdd_eq_ofIntWithPrec, le_iff_toRat]
+      replace h : k = Int.ofNat l + prec := by omega
+      subst h
+      simp only [toRat_ofIntWithPrec_eq_mul_two_pow]
+      rw [Int.neg_add, Rat.zpow_add (by decide), ← Rat.mul_assoc]
+      refine Lean.Grind.OrderedRing.mul_le_mul_of_nonneg_right ?_ (Rat.zpow_nonneg (by decide))
+      rw [Int.shiftRight_eq_div_pow]
+      rw [← Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_pos_right (c := 2^(Int.ofNat l)) (Rat.zpow_pos (by decide))]
+      simp only [Int.natCast_pow, Int.cast_ofNat_Int, Int.ofNat_eq_coe]
+      rw [Rat.mul_assoc, ← Rat.zpow_add (by decide), Int.add_left_neg, Rat.zpow_zero, Rat.mul_one]
+      have : (2 : Rat) ^ (l : Int) = (2 ^ l : Int) := by
+        rw [Rat.zpow_natCast, Rat.intCast_pow, Rat.intCast_ofNat]
+      rw [this, ← Rat.intCast_mul, Rat.intCast_le_intCast]
+      exact Int.ediv_mul_le n (Int.pow_ne_zero (by decide))
+    | .negSucc _ =>
+      apply Dyadic.le_refl
+
+theorem precision_roundDown {x : Dyadic} {prec : Int} : (roundDown x prec).precision ≤ some prec := by
+  unfold roundDown
+  match x with
+  | zero => simp [precision]
+  | ofOdd n k hn =>
+    dsimp
+    split
+    · rename_i n' h
+      by_cases h' : n >>> n' = 0
+      · simp [h']
+      · exact precision_ofIntWithPrec_le h' _
+    · simp [precision]
+      omega
+
+-- This theorem would characterize `roundDown` in terms of the order and `precision`.
+-- theorem le_roundDown {x y : Dyadic} {prec : Int} (h : y.precision ≤ some prec) (h' : y ≤ x) :
+--     y ≤ x.roundDown prec := sorry
+
+theorem le_roundUp {x : Dyadic} {prec : Int} : x ≤ roundUp x prec := by
+  rw [roundUp_eq_neg_roundDown_neg, Lean.Grind.OrderedAdd.le_neg_iff]
+  apply roundDown_le
+
+theorem precision_roundUp {x : Dyadic} {prec : Int} : (roundUp x prec).precision ≤ some prec := by
+  rw [roundUp_eq_neg_roundDown_neg, precision_neg]
+  exact precision_roundDown
+
+-- This theorem would characterize `roundUp` in terms of the order and `precision`.
+-- theorem roundUp_le {x y : Dyadic} {prec : Int} (h : y.precision ≤ some prec) (h' : x ≤ y) :
+--    x.roundUp prec ≤ y := sorry

src/Init/Data/Rat/Lemmas.lean

@@ -773,12 +773,33 @@ protected theorem pow_pos {a : Rat} {n : Nat} (h : 0 < a) : 0 < a ^ n := by
   | zero => simp +decide
   | succ k ih => rw [Rat.pow_succ]; exact Rat.mul_pos ih h
 
+protected theorem pow_nonneg {a : Rat} {n : Nat} (h : 0 ≤ a) : 0 ≤ a ^ n := by
+  by_cases h' : a = 0
+  · simp [h']
+    match n with
+    | 0 => simp; rfl
+    | n + 1 => simp [Rat.pow_succ]; apply Rat.le_refl
+  · exact Rat.le_of_lt (Rat.pow_pos (Rat.lt_of_le_of_ne h (Ne.symm h')))
+
 protected theorem zpow_pos {a : Rat} {n : Int} (h : 0 < a) : 0 < a ^ n := by
   cases n
   · simp [Rat.zpow_natCast, Rat.pow_pos h]
   · simp only [Int.negSucc_eq, Rat.zpow_neg, Rat.inv_pos, ← Int.natCast_add_one,
       Rat.zpow_natCast, Rat.pow_pos h]
 
+protected theorem zpow_nonneg {a : Rat} {n : Int} (h : 0 ≤ a) : 0 ≤ a ^ n := by
+  by_cases h' : a = 0
+  · simp [h']
+    match n with
+    | (0 : Nat) => simp; rfl
+    | (n + 1 : Nat) =>
+      rw [Rat.zpow_natCast, Rat.pow_succ, Rat.mul_zero]
+      rfl
+    | -(n + 1 : Nat) =>
+      rw [Rat.zpow_neg, Rat.zpow_natCast, Rat.pow_succ, Rat.mul_zero, Rat.inv_zero]
+      rfl
+  · exact Rat.le_of_lt (Rat.zpow_pos (Rat.lt_of_le_of_ne h (Ne.symm h')))
+
 protected theorem div_lt_iff {a b c : Rat} (hb : 0 < b) : a / b < c ↔ a < c * b := by
   rw [← Rat.mul_lt_mul_right hb, Rat.div_mul_cancel (Rat.ne_of_gt hb)]