Mathlib.Data.Rat.Floor

Rat.floor_def' theorem

(a : ℚ) : a.floor = a.num / a.den

Full source

protected theorem floor_def' (a : ℚ) : a.floor = a.num / a.den := by
  rw [Rat.floor]
  split
  · next h => simp [h]
  · next => rfl

Floor of Rational Number as Integer Division of Numerator by Denominator

Informal description

For any rational number $a$, the floor of $a$ is equal to the integer division of its numerator by its denominator, i.e., $\lfloor a \rfloor = \text{num}(a) / \text{den}(a)$.

Rat.le_floor theorem

{z : ℤ} : ∀ {r : ℚ}, z ≤ Rat.floor r ↔ (z : ℚ) ≤ r

Full source

protected theorem le_floor {z : ℤ} : ∀ {r : ℚ}, z ≤ Rat.floor r ↔ (z : ℚ) ≤ r
  | ⟨n, d, h, c⟩ => by
    simp only [Rat.floor_def']
    rw [mk'_eq_divInt]
    have h' := Int.ofNat_lt.2 (Nat.pos_of_ne_zero h)
    conv =>
      rhs
      rw [intCast_eq_divInt, Rat.divInt_le_divInt zero_lt_one h', mul_one]
    exact Int.le_ediv_iff_mul_le h'

Integer-Rational Floor Inequality: $z \leq \lfloor r \rfloor \leftrightarrow z \leq r$

Informal description

For any integer $z$ and rational number $r$, we have $z \leq \lfloor r \rfloor$ if and only if $z \leq r$ (where $z$ is viewed as a rational number via the canonical embedding).

Rat.instFloorRing instance

: FloorRing ℚ

Full source

instance : FloorRing ℚ :=
  (FloorRing.ofFloor ℚ Rat.floor) fun _ _ => Rat.le_floor.symm

Floor Ring Structure on Rational Numbers

Informal description

The rational numbers $\mathbb{Q}$ form a `FloorRing`, meaning they are equipped with a floor function $\lfloor \cdot \rfloor : \mathbb{Q} \to \mathbb{Z}$ that satisfies the standard properties of a floor function.

Rat.floor_def theorem

{q : ℚ} : ⌊q⌋ = q.num / q.den

Full source

protected theorem floor_def {q : ℚ} : ⌊q⌋ = q.num / q.den := Rat.floor_def' q

Floor of Rational Number as Integer Division of Numerator by Denominator

Informal description

For any rational number $q$, the floor of $q$ is equal to the integer division of its numerator by its denominator, i.e., $\lfloor q \rfloor = \text{num}(q) / \text{den}(q)$.

Rat.ceil_def theorem

(q : ℚ) : ⌈q⌉ = -(-q.num / ↑q.den)

Full source

protected theorem ceil_def (q : ℚ) : ⌈q⌉ = -(-q.num / ↑q.den) := by
  change -⌊-q⌋ = _
  rw [Rat.floor_def, num_neg_eq_neg_num, den_neg_eq_den]

Ceiling of Rational Number via Integer Division

Informal description

For any rational number $q$, the ceiling of $q$ is equal to the negation of the integer division of the negation of its numerator by its denominator, i.e., $\lceil q \rceil = -\left\lfloor \frac{-\text{num}(q)}{\text{den}(q)} \right\rfloor$.

Rat.floor_intCast_div_natCast theorem

(n : ℤ) (d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋ = n / (↑d : ℤ)

Full source

@[norm_cast]
theorem floor_intCast_div_natCast (n : ℤ) (d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋ = n / (↑d : ℤ) := by
  rw [Rat.floor_def]
  obtain rfl | hd := eq_zero_or_pos (a := d)
  · simp
  set q := (n : ℚ) / d with q_eq
  obtain ⟨c, n_eq_c_mul_num, d_eq_c_mul_denom⟩ : ∃ c, n = c * q.num ∧ (d : ℤ) = c * q.den := by
    rw [q_eq]
    exact mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den n d (mod_cast hd.ne')
  rw [n_eq_c_mul_num, d_eq_c_mul_denom]
  refine (Int.mul_ediv_mul_of_pos _ _ <| pos_of_mul_pos_left ?_ <| Int.natCast_nonneg q.den).symm
  rwa [← d_eq_c_mul_denom, Int.natCast_pos]

Floor of Integer Divided by Natural Number Equals Integer Division

Informal description

For any integer $n$ and natural number $d$, the floor of the rational number $\frac{n}{d}$ is equal to the integer division of $n$ by $d$ (viewed as an integer), i.e., $\left\lfloor \frac{n}{d} \right\rfloor = n / d$.

Rat.ceil_intCast_div_natCast theorem

(n : ℤ) (d : ℕ) : ⌈(↑n / ↑d : ℚ)⌉ = -((-n) / (↑d : ℤ))

Full source

@[norm_cast]
theorem ceil_intCast_div_natCast (n : ℤ) (d : ℕ) : ⌈(↑n / ↑d : ℚ)⌉ = -((-n) / (↑d : ℤ)) := by
  conv_lhs => rw [← neg_neg ⌈_⌉, ← floor_neg]
  rw [← neg_div, ← Int.cast_neg, floor_intCast_div_natCast]

Ceiling of Integer Divided by Natural Number Equals Negated Floor of Negative Division

Informal description

For any integer $n$ and natural number $d$, the ceiling of the rational number $\frac{n}{d}$ is equal to the negation of the integer division of $-n$ by $d$ (viewed as an integer), i.e., $\left\lceil \frac{n}{d} \right\rceil = -\left\lfloor \frac{-n}{d} \right\rfloor$.

Rat.floor_natCast_div_natCast theorem

(n d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋ = n / d

Full source

@[norm_cast]
theorem floor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋ = n / d :=
  floor_intCast_div_natCast n d

Floor of Natural Division Equals Natural Division: $\left\lfloor \frac{n}{d} \right\rfloor = n / d$

Informal description

For any natural numbers $n$ and $d$, the floor of the rational number $\frac{n}{d}$ is equal to the natural number division of $n$ by $d$, i.e., $\left\lfloor \frac{n}{d} \right\rfloor = n / d$.

Rat.ceil_natCast_div_natCast theorem

(n d : ℕ) : ⌈(↑n / ↑d : ℚ)⌉ = -((-n) / d)

Full source

@[norm_cast]
theorem ceil_natCast_div_natCast (n d : ℕ) : ⌈(↑n / ↑d : ℚ)⌉ = -((-n) / d) :=
  ceil_intCast_div_natCast n d

Ceiling of Natural Division Equals Negated Floor of Negative Division: $\left\lceil \frac{n}{d} \right\rceil = -\left\lfloor \frac{-n}{d} \right\rfloor$

Informal description

For any natural numbers $n$ and $d$, the ceiling of the rational number $\frac{n}{d}$ is equal to the negation of the integer division of $-n$ by $d$, i.e., $\left\lceil \frac{n}{d} \right\rceil = -\left\lfloor \frac{-n}{d} \right\rfloor$.

Rat.natFloor_natCast_div_natCast theorem

(n d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋₊ = n / d

Full source

@[norm_cast]
theorem natFloor_natCast_div_natCast (n d : ℕ) : ⌊(↑n / ↑d : ℚ)⌋₊ = n / d := by
  rw [← Int.ofNat_inj, Int.natCast_floor_eq_floor (by positivity)]
  push_cast
  exact floor_intCast_div_natCast n d

Natural Floor of Rational Division Equals Natural Division: $\lfloor \frac{n}{d} \rfloor_\mathbb{N} = n / d$

Informal description

For any natural numbers $n$ and $d$, the floor of the rational number $\frac{n}{d}$ (as a natural number) equals the natural number division of $n$ by $d$, i.e., $\lfloor \frac{n}{d} \rfloor_\mathbb{N} = n / d$.

Rat.floor_cast theorem

(x : ℚ) : ⌊(x : α)⌋ = ⌊x⌋

Full source

@[simp, norm_cast]
theorem floor_cast (x : ℚ) : ⌊(x : α)⌋ = ⌊x⌋ :=
  floor_eq_iff.2 (mod_cast floor_eq_iff.1 (Eq.refl ⌊x⌋))

Floor Function Commutes with Casting of Rational Numbers

Informal description

For any rational number $x \in \mathbb{Q}$ and any type $\alpha$ with a floor ring structure, the floor of the cast of $x$ to $\alpha$ is equal to the floor of $x$ in $\mathbb{Q}$, i.e., $\lfloor x \rfloor_\alpha = \lfloor x \rfloor_\mathbb{Q}$.

Rat.ceil_cast theorem

(x : ℚ) : ⌈(x : α)⌉ = ⌈x⌉

Full source

@[simp, norm_cast]
theorem ceil_cast (x : ℚ) : ⌈(x : α)⌉ = ⌈x⌉ := by
  rw [← neg_inj, ← floor_neg, ← floor_neg, ← Rat.cast_neg, Rat.floor_cast]

Ceiling Function Commutes with Casting of Rational Numbers

Informal description

For any rational number $x \in \mathbb{Q}$ and any type $\alpha$ with a floor ring structure, the ceiling of the cast of $x$ to $\alpha$ is equal to the ceiling of $x$ in $\mathbb{Q}$, i.e., $\lceil x \rceil_\alpha = \lceil x \rceil_\mathbb{Q}$.

Rat.round_cast theorem

(x : ℚ) : round (x : α) = round x

Full source

@[simp, norm_cast]
theorem round_cast (x : ℚ) : round (x : α) = round x := by
  have : ((x + 1 / 2 : ℚ) : α) = x + 1 / 2 := by simp
  rw [round_eq, round_eq, ← this, floor_cast]

Rounding Commutes with Casting of Rational Numbers

Informal description

For any rational number $x \in \mathbb{Q}$ and any type $\alpha$ with a floor ring structure, the rounding of the cast of $x$ to $\alpha$ is equal to the rounding of $x$ in $\mathbb{Q}$, i.e., $\operatorname{round}(x : \alpha) = \operatorname{round}(x)$.

Rat.cast_fract theorem

(x : ℚ) : (↑(fract x) : α) = fract (x : α)

Full source

@[simp, norm_cast]
theorem cast_fract (x : ℚ) : (↑(fract x) : α) = fract (x : α) := by
  simp only [fract, cast_sub, cast_intCast, floor_cast]

Fractional Part Preservation under Rational Number Casting: $\overline{\operatorname{fract}(x)} = \operatorname{fract}(\overline{x})$

Informal description

For any rational number $x$ and any type $\alpha$ with a floor ring structure, the fractional part of $x$ when cast to $\alpha$ equals the fractional part of the cast of $x$ to $\alpha$, i.e., $\overline{\operatorname{fract}(x)} = \operatorname{fract}(\overline{x})$, where $\overline{\cdot}$ denotes the canonical map and $\operatorname{fract}(x) = x - \lfloor x \rfloor$.

Rat.isNat_intFloor theorem

{R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (m : ℕ) : IsNat r m → IsNat ⌊r⌋ m

Full source

theorem isNat_intFloor {R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R]
    (r : R) (m : ℕ) :
    IsNat r m → IsNat ⌊r⌋ m := by rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

Floor of Natural-Valued Element in a Floor Ring

Informal description

Let $R$ be a ring with a linear order and a strict ordered ring structure, and equipped with a floor ring structure. For any element $r \in R$ and natural number $m \in \mathbb{N}$, if $r$ is equal to the image of $m$ under the canonical map from $\mathbb{N}$ to $R$, then the floor of $r$ is also equal to the image of $m$ under this canonical map, i.e., $\lfloor r \rfloor = m$.

Rat.isInt_intFloor theorem

{R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (m : ℤ) : IsInt r m → IsInt ⌊r⌋ m

Full source

theorem isInt_intFloor {R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R]
    (r : R) (m : ℤ) :
    IsInt r m → IsInt ⌊r⌋ m := by rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

Floor of Integer-Valued Element in a Floor Ring

Informal description

Let $R$ be a ring with a linear order and a strict ordered ring structure, and equipped with a floor ring structure. For any element $r \in R$ and integer $m \in \mathbb{Z}$, if $r$ is equal to the image of $m$ under the canonical map from $\mathbb{Z}$ to $R$, then the floor of $r$ is also equal to the image of $m$ under this canonical map, i.e., $\lfloor r \rfloor = m$.

Rat.isInt_intFloor_ofIsRat theorem

(r : α) (n : ℤ) (d : ℕ) : IsRat r n d → IsInt ⌊r⌋ (n / d)

Full source

theorem isInt_intFloor_ofIsRat (r : α) (n : ℤ) (d : ℕ) :
    IsRat r n d → IsInt ⌊r⌋ (n / d) := by
  rintro ⟨inv, rfl⟩
  constructor
  simp only [invOf_eq_inv, ← div_eq_mul_inv, Int.cast_id]
  rw [← floor_intCast_div_natCast n d, ← floor_cast (α := α), Rat.cast_div,
    cast_intCast, cast_natCast]

Floor of Rational-Valued Element Equals Integer Division

Informal description

For any element $r$ in a ring $\alpha$ and integers $n \in \mathbb{Z}$, $d \in \mathbb{N}$, if $r$ is equal to the rational number $n/d$ (i.e., $\text{IsRat}\, r\, n\, d$ holds), then the floor of $r$ is equal to the integer division of $n$ by $d$ (i.e., $\lfloor r \rfloor = n / d$).

Rat.evalIntFloor definition

: NormNumExt

Full source

/-- `norm_num` extension for `Int.floor` -/
@[norm_num ⌊_⌋]
def evalIntFloor : NormNumExt where eval {u αZ} e := do
  match u, αZ, e with
  | 0, ~q(ℤ), ~q(@Int.floor $α $instR $instO $instF $x) =>
    match ← derive x with
    | .isBool .. => failure
    | .isNat _ _ pb => do
      let _i ← synthInstanceQ q(IsStrictOrderedRing $α)
      assertInstancesCommute
      return .isNat q(inferInstance) _ q(isNat_intFloor $x _ $pb)
    | .isNegNat _ _ pb => do
      let _i ← synthInstanceQ q(IsStrictOrderedRing $α)
      assertInstancesCommute
      -- floor always keeps naturals negative, so we can shortcut `.isInt`
      return .isNegNat q(inferInstance) _ q(isInt_intFloor _ _ $pb)
    | .isRat _ q n d h => do
      let _i ← synthInstanceQ q(Field $α)
      let _i ← synthInstanceQ q(IsStrictOrderedRing $α)
      assertInstancesCommute
      have z : Q(ℤ) := mkRawIntLit ⌊q⌋
      letI : $z =Q $n / $d := ⟨⟩
      return .isInt q(inferInstance) z ⌊q⌋ q(isInt_intFloor_ofIsRat _ $n $d $h)
  | _, _, _ => failure

`norm_num` extension for rational floor function

Informal description

The `norm_num` extension for evaluating the floor function on rational numbers. Given an expression of the form `⌊x⌋` where `x` is a rational number, this extension normalizes it to an integer by: - If `x` is a natural number, returning that number directly - If `x` is a negative integer, returning its negation - If `x` is a rational number `n/d`, returning the integer division `n/d` The evaluation preserves the mathematical properties of the floor function while avoiding unnecessary typeclass searches.

Rat.isNat_intCeil theorem

{R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (m : ℕ) : IsNat r m → IsNat ⌈r⌉ m

Full source

theorem isNat_intCeil {R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R]
    (r : R) (m : ℕ) :
    IsNat r m → IsNat ⌈r⌉ m := by rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

Ceiling of Natural Number in Rationals is Itself

Informal description

For any ring $R$ with a linear order, strict ordered ring structure, and floor ring structure, if a rational number $r$ is equal to a natural number $m$ (i.e., $r = m$), then the ceiling of $r$ is also equal to $m$ (i.e., $\lceil r \rceil = m$).

Rat.isInt_intCeil theorem

{R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R] (r : R) (m : ℤ) : IsInt r m → IsInt ⌈r⌉ m

Full source

theorem isInt_intCeil {R} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorRing R]
    (r : R) (m : ℤ) :
    IsInt r m → IsInt ⌈r⌉ m := by rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

Ceiling of Integer-Valued Element in Ordered Ring

Informal description

Let $R$ be a ring equipped with a linear order, strict ordered ring structure, and floor ring structure. For any element $r \in R$ and integer $m \in \mathbb{Z}$, if $r$ is equal to $m$ (i.e., $r = m$), then the ceiling of $r$ is also equal to $m$ (i.e., $\lceil r \rceil = m$).

Rat.isInt_intCeil_ofIsRat theorem

(r : α) (n : ℤ) (d : ℕ) : IsRat r n d → IsInt ⌈r⌉ (-(-n / d))

Full source

theorem isInt_intCeil_ofIsRat (r : α) (n : ℤ) (d : ℕ) :
    IsRat r n d → IsInt ⌈r⌉ (-(-n / d)) := by
  rintro ⟨inv, rfl⟩
  constructor
  simp only [invOf_eq_inv, ← div_eq_mul_inv, Int.cast_id]
  rw [← ceil_intCast_div_natCast n d, ← ceil_cast (α := α), Rat.cast_div,
    cast_intCast, cast_natCast]

Ceiling of Rational Representation in Ring Equals Negated Floor of Negative Division

Informal description

For any element $r$ in a ring $\alpha$ and integers $n \in \mathbb{Z}$, $d \in \mathbb{N}$, if $r$ is equal to the rational number $\frac{n}{d}$ (i.e., $\text{IsRat}\, r\, n\, d$ holds), then the ceiling of $r$ is equal to the integer $-\left\lfloor \frac{-n}{d} \right\rfloor$ (i.e., $\text{IsInt}\, \lceil r \rceil\, (-\left\lfloor \frac{-n}{d} \right\rfloor)$ holds).

Rat.evalIntCeil definition

: NormNumExt

Full source

/-- `norm_num` extension for `Int.ceil` -/
@[norm_num ⌈_⌉]
def evalIntCeil : NormNumExt where eval {u αZ} e := do
  match u, αZ, e with
  | 0, ~q(ℤ), ~q(@Int.ceil $α $instR $instO $instF $x) =>
    match ← derive x with
    | .isBool .. => failure
    | .isNat _ _ pb => do
      let _i ← synthInstanceQ q(IsStrictOrderedRing $α)
      assertInstancesCommute
      return .isNat q(inferInstance) _ q(isNat_intCeil $x _ $pb)
    | .isNegNat _ _ pb => do
      let _i ← synthInstanceQ q(IsStrictOrderedRing $α)
      assertInstancesCommute
      -- ceil always keeps naturals negative, so we can shortcut `.isInt`
      return .isNegNat q(inferInstance) _ q(isInt_intCeil _ _ $pb)
    | .isRat _ q n d h => do
      let _i ← synthInstanceQ q(Field $α)
      let _i ← synthInstanceQ q(IsStrictOrderedRing $α)
      assertInstancesCommute
      have z : Q(ℤ) := mkRawIntLit ⌈q⌉
      letI : $z =Q (-(-$n / $d)) := ⟨⟩
      return .isInt q(inferInstance) z ⌈q⌉ q(isInt_intCeil_ofIsRat _ $n $d $h)
  | _, _, _ => failure

Ceiling function normalization for rational numbers

Informal description

The `norm_num` extension for evaluating the ceiling function on rational numbers. Given an expression of the form `Int.ceil x` where `x` is a rational number, this extension normalizes the expression by: - If `x` is a natural number, returning the same natural number. - If `x` is a negative integer, returning the same negative integer. - If `x` is a rational number `n/d`, returning the integer `-(-n / d)` (which is equivalent to the ceiling of `n/d`).

Int.mod_nat_eq_sub_mul_floor_rat_div theorem

{n : ℤ} {d : ℕ} : n % d = n - d * ⌊(n : ℚ) / d⌋

Full source

theorem Int.mod_nat_eq_sub_mul_floor_rat_div {n : ℤ} {d : ℕ} : n % d = n - d * ⌊(n : ℚ) / d⌋ := by
  rw [eq_sub_of_add_eq <| Int.emod_add_ediv n d, Rat.floor_intCast_div_natCast]

Modulo as Difference with Floor Division: $n \bmod d = n - d \lfloor n/d \rfloor$

Informal description

For any integer $n$ and natural number $d$, the modulo operation $n \bmod d$ equals $n$ minus $d$ times the floor of the rational division $\frac{n}{d}$, i.e., \[ n \bmod d = n - d \left\lfloor \frac{n}{d} \right\rfloor. \]

Nat.coprime_sub_mul_floor_rat_div_of_coprime theorem

{n d : ℕ} (n_coprime_d : n.Coprime d) : ((n : ℤ) - d * ⌊(n : ℚ) / d⌋).natAbs.Coprime d

Full source

theorem Nat.coprime_sub_mul_floor_rat_div_of_coprime {n d : ℕ} (n_coprime_d : n.Coprime d) :
    ((n : ℤ) - d * ⌊(n : ℚ) / d⌋).natAbs.Coprime d := by
  have : (n : ℤ) % d = n - d * ⌊(n : ℚ) / d⌋ := Int.mod_nat_eq_sub_mul_floor_rat_div
  rw [← this]
  have : d.Coprime n := n_coprime_d.symm
  rwa [Nat.Coprime, Nat.gcd_rec] at this

Coprimality Preservation Under Floor Division: $\gcd(n, d) = 1 \implies \gcd(|n - d \lfloor n/d \rfloor|, d) = 1$

Informal description

For any natural numbers $n$ and $d$ such that $n$ and $d$ are coprime, the natural number obtained as the absolute value of $n - d \lfloor \frac{n}{d} \rfloor$ is also coprime with $d$. In other words, if $\gcd(n, d) = 1$, then $\gcd(|n - d \lfloor \frac{n}{d} \rfloor|, d) = 1$.

Rat.num_lt_succ_floor_mul_den theorem

(q : ℚ) : q.num < (⌊q⌋ + 1) * q.den

Full source

theorem num_lt_succ_floor_mul_den (q : ℚ) : q.num < (⌊q⌋ + 1) * q.den := by
  suffices (q.num : ℚ) < (⌊q⌋ + 1) * q.den from mod_cast this
  suffices (q.num : ℚ) < (q - fract q + 1) * q.den by
    have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q
    rwa [this]
  suffices (q.num : ℚ) < q.num + (1 - fract q) * q.den by
    have : (q - fract q + 1) * q.den = q.num + (1 - fract q) * q.den := by
      calc
        (q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
        _ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
        _ = q.num + (1 - fract q) * q.den := by simp
    rwa [this]
  suffices 0 < (1 - fract q) * q.den by
    rw [← sub_lt_iff_lt_add']
    simpa
  have : 0 < 1 - fract q := by
    have : fract q < 1 := fract_lt_one q
    have : 0 + fract q < 1 := by simp [this]
    rwa [lt_sub_iff_add_lt]
  exact mul_pos this (by exact mod_cast q.pos)

Numerator Bound via Floor and Denominator: $\text{num}(q) < (\lfloor q \rfloor + 1) \cdot \text{den}(q)$

Informal description

For any rational number $q$, the numerator of $q$ is strictly less than the product of the denominator of $q$ and the successor of the floor of $q$, i.e., \[ \text{num}(q) < (\lfloor q \rfloor + 1) \cdot \text{den}(q). \]

Rat.fract_inv_num_lt_num_of_pos theorem

{q : ℚ} (q_pos : 0 < q) : (fract q⁻¹).num < q.num

Full source

theorem fract_inv_num_lt_num_of_pos {q : ℚ} (q_pos : 0 < q) : (fract q⁻¹).num < q.num := by
  -- we know that the numerator must be positive
  have q_num_pos : 0 < q.num := Rat.num_pos.mpr q_pos
  -- we will work with the absolute value of the numerator, which is equal to the numerator
  have q_num_abs_eq_q_num : (q.num.natAbs : ℤ) = q.num := Int.natAbs_of_nonneg q_num_pos.le
  set q_inv : ℚ := q.den / q.num with q_inv_def
  have q_inv_eq : q⁻¹ = q_inv := by rw [q_inv_def, inv_def', divInt_eq_div, Int.cast_natCast]
  suffices (q_inv - ⌊q_inv⌋).num < q.num by rwa [q_inv_eq]
  suffices ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num < q.num by
    field_simp [q_inv, this, ne_of_gt q_num_pos]
  suffices (q.den : ℤ) - q.num * ⌊q_inv⌋ < q.num by
    -- use that `q.num` and `q.den` are coprime to show that the numerator stays unreduced
    have : ((q.den - q.num * ⌊q_inv⌋ : ℚ) / q.num).num = q.den - q.num * ⌊q_inv⌋ := by
      suffices ((q.den : ℤ) - q.num * ⌊q_inv⌋).natAbs.Coprime q.num.natAbs from
        mod_cast Rat.num_div_eq_of_coprime q_num_pos this
      have tmp := Nat.coprime_sub_mul_floor_rat_div_of_coprime q.reduced.symm
      simpa only [Nat.cast_natAbs, abs_of_nonneg q_num_pos.le] using tmp
    rwa [this]
  -- to show the claim, start with the following inequality
  have q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * q⁻¹.den < q⁻¹.den := by
    have : q⁻¹.num < (⌊q⁻¹⌋ + 1) * q⁻¹.den := Rat.num_lt_succ_floor_mul_den q⁻¹
    have : q⁻¹.num < ⌊q⁻¹⌋ * q⁻¹.den + q⁻¹.den := by rwa [right_distrib, one_mul] at this
    rwa [← sub_lt_iff_lt_add'] at this
  -- use that `q.num` and `q.den` are coprime to show that q_inv is the unreduced reciprocal
  -- of `q`
  have : q_inv.num = q.den ∧ q_inv.den = q.num.natAbs := by
    have coprime_q_denom_q_num : q.den.Coprime q.num.natAbs := q.reduced.symm
    have : Int.natAbs q.den = q.den := by simp
    rw [← this] at coprime_q_denom_q_num
    rw [q_inv_def]
    constructor
    · exact mod_cast Rat.num_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
    · suffices (((q.den : ℚ) / q.num).den : ℤ) = q.num.natAbs by exact mod_cast this
      rw [q_num_abs_eq_q_num]
      exact mod_cast Rat.den_div_eq_of_coprime q_num_pos coprime_q_denom_q_num
  rwa [q_inv_eq, this.left, this.right, q_num_abs_eq_q_num, mul_comm] at q_inv_num_denom_ineq

Numerator Comparison for Fractional Part of Reciprocal: $\text{num}(\text{fract}(q^{-1})) < \text{num}(q)$ when $q > 0$

Informal description

For any positive rational number $q$, the numerator of the fractional part of its reciprocal is strictly less than the numerator of $q$, i.e., $\text{num}(\text{fract}(q^{-1})) < \text{num}(q)$.

Mathlib.Data.Rat.Floor

Summary

Tags