Lemmas on Nat.floor and Nat.ceil for semifields

This file contains basic results on the natural-valued floor and ceiling functions.

Tags

rounding, floor, ceil

theorem Nat.floor_div_natCast {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (a : K) (n : ℕ) : ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n

theorem Nat.cast_mul_floor_div_cancel {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {n : ℕ} (hn : n ≠ 0) (a : K) : ⌊↑n * a⌋₊ / n = ⌊a⌋₊

theorem Nat.mul_cast_floor_div_cancel {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {n : ℕ} (hn : n ≠ 0) (a : K) : ⌊a * ↑n⌋₊ / n = ⌊a⌋₊

@[deprecated Nat.floor_div_natCast (since := "2025-04-01")]

theorem Nat.floor_div_nat {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (a : K) (n : ℕ) : ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n

Alias of Nat.floor_div_natCast.

theorem Nat.floor_div_ofNat {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (a : K) (n : ℕ) [n.AtLeastTwo] : ⌊a / OfNat.ofNat n⌋₊ = ⌊a⌋₊ / OfNat.ofNat n

theorem Nat.floor_div_eq_div {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] (m n : ℕ) : ⌊↑m / ↑n⌋₊ = m / n

Natural division is the floor of field division.

theorem Nat.mul_lt_floor {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {a b : K} (hb₀ : 0 < b) (hb : b < 1) (hba : ↑⌈b / (1 - b)⌉₊ ≤ a) : b * a < ↑⌊a⌋₊

theorem Nat.ceil_lt_mul {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {a b : K} (hb : 1 < b) (hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a) : ↑⌈a⌉₊ < b * a

theorem Nat.ceil_le_mul {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {a b : K} (hb : 1 < b) (hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ a) : ↑⌈a⌉₊ ≤ b * a

theorem Nat.div_two_lt_floor {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {a : K} (ha : 1 ≤ a) : a / 2 < ↑⌊a⌋₊

theorem Nat.ceil_lt_two_mul {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {a : K} (ha : 2⁻¹ < a) : ↑⌈a⌉₊ < 2 * a

theorem Nat.ceil_le_two_mul {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K] {a : K} (ha : 2⁻¹ ≤ a) : ↑⌈a⌉₊ ≤ 2 * a