8d9d23b5bb
This PR adds the inverse of a dyadic rational, at a given precision, and characterising lemmas. Also cleans up various parts of the `Int.DivMod` and `Rat` APIs, and proves some characterising lemmas about `Rat.toDyadic`. --------- Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
80 lines
2.6 KiB
Text
80 lines
2.6 KiB
Text
/-
|
|
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
|
|
import Init.Data.Dyadic.Basic
|
|
import Init.Data.Dyadic.Round
|
|
import Init.Grind.Ordered.Ring
|
|
|
|
/-!
|
|
# Inversion for dyadic numbers
|
|
-/
|
|
|
|
namespace Dyadic
|
|
|
|
/--
|
|
Inverts a dyadic number at a given (maximum) precision.
|
|
Returns the greatest dyadic number with precision at most `prec` which is less than or equal to `1/x`.
|
|
For `x = 0`, returns `0`.
|
|
-/
|
|
def invAtPrec (x : Dyadic) (prec : Int) : Dyadic :=
|
|
match x with
|
|
| .zero => .zero
|
|
| _ => x.toRat.inv.toDyadic prec
|
|
|
|
/-- For a positive dyadic `x`, `invAtPrec x prec * x ≤ 1`. -/
|
|
theorem invAtPrec_mul_le_one {x : Dyadic} (hx : 0 < x) (prec : Int) :
|
|
invAtPrec x prec * x ≤ 1 := by
|
|
rw [le_iff_toRat]
|
|
rw [toRat_mul]
|
|
rw [show (1 : Dyadic).toRat = (1 : Rat) from rfl]
|
|
unfold invAtPrec
|
|
cases x with
|
|
| zero =>
|
|
exfalso
|
|
contradiction
|
|
| ofOdd n k hn =>
|
|
simp only
|
|
have h_le : ((ofOdd n k hn).toRat.inv.toDyadic prec).toRat ≤ (ofOdd n k hn).toRat.inv := Rat.toRat_toDyadic_le
|
|
have h_pos : 0 ≤ (ofOdd n k hn).toRat := by
|
|
rw [lt_iff_toRat, toRat_zero] at hx
|
|
exact Rat.le_of_lt hx
|
|
calc ((ofOdd n k hn).toRat.inv.toDyadic prec).toRat * (ofOdd n k hn).toRat
|
|
≤ (ofOdd n k hn).toRat.inv * (ofOdd n k hn).toRat := Rat.mul_le_mul_of_nonneg_right h_le h_pos
|
|
_ = 1 := by
|
|
apply Rat.inv_mul_cancel
|
|
rw [lt_iff_toRat, toRat_zero] at hx
|
|
exact Rat.ne_of_gt hx
|
|
|
|
/-- For a positive dyadic `x`, `1 < (invAtPrec x prec + 2^(-prec)) * x`. -/
|
|
theorem one_lt_invAtPrec_add_inc_mul {x : Dyadic} (hx : 0 < x) (prec : Int) :
|
|
1 < (invAtPrec x prec + ofIntWithPrec 1 prec) * x := by
|
|
rw [lt_iff_toRat]
|
|
rw [toRat_mul]
|
|
rw [show (1 : Dyadic).toRat = (1 : Rat) from rfl]
|
|
unfold invAtPrec
|
|
cases x with
|
|
| zero =>
|
|
exfalso
|
|
contradiction
|
|
| ofOdd n k hn =>
|
|
simp only
|
|
have h_le : (ofOdd n k hn).toRat.inv < ((ofOdd n k hn).toRat.inv.toDyadic prec + ofIntWithPrec 1 prec).toRat :=
|
|
Rat.lt_toRat_toDyadic_add
|
|
have h_pos : 0 < (ofOdd n k hn).toRat := by
|
|
rwa [lt_iff_toRat, toRat_zero] at hx
|
|
calc
|
|
1 = (ofOdd n k hn).toRat.inv * (ofOdd n k hn).toRat := by
|
|
symm
|
|
apply Rat.inv_mul_cancel
|
|
rw [lt_iff_toRat, toRat_zero] at hx
|
|
exact Rat.ne_of_gt hx
|
|
_ < ((ofOdd n k hn).toRat.inv.toDyadic prec + ofIntWithPrec 1 prec).toRat * (ofOdd n k hn).toRat :=
|
|
Rat.mul_lt_mul_of_pos_right h_le h_pos
|
|
|
|
-- TODO: `invAtPrec` is the unique dyadic with the given precision satisfying the two inequalities above.
|
|
|
|
end Dyadic
|