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.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

norm_num extension for Nat.floor

theorem Mathlib.Meta.NormNum.IsNat.natFloor {R : Type u_3} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorSemiring R] (r : R) (m : ℕ) : IsNat r m → IsNat ⌊r⌋₊ m

theorem Mathlib.Meta.NormNum.IsInt.natFloor {R : Type u_3} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorSemiring R] (r : R) (m : ℕ) : IsInt r (Int.negOfNat m) → IsNat ⌊r⌋₊ 0

theorem Mathlib.Meta.NormNum.IsNNRat.natFloor {R : Type u_3} [Semifield R] [LinearOrder R] [IsStrictOrderedRing R] [FloorSemiring R] (r : R) (n d : ℕ) (h : IsNNRat r n d) (res : ℕ) (hres : n / d = res) : IsNat ⌊r⌋₊ res

theorem Mathlib.Meta.NormNum.IsRat.natFloor {R : Type u_3} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [FloorSemiring R] (r : R) (n d : ℕ) (h : IsRat r (Int.negOfNat n) d) : IsNat ⌊r⌋₊ 0

def Mathlib.Meta.NormNum.evalNatFloor : NormNumExt

norm_num extension for Nat.floor