Floor and ceil #
Summary #
We define the natural- and integer-valued floor and ceil functions on linearly ordered rings.
Main Definitions #
-
FloorSemiring
: An ordered semiring with natural-valued floor and ceil. -
Nat.floor a
: Greatest naturaln
such thatn ≤ a≤ a
. Equal to0
ifa < 0
. -
Nat.ceil a
: Least naturaln
such thata ≤ n≤ n
. -
FloorRing
: A linearly ordered ring with integer-valued floor and ceil. -
Int.floor a
: Greatest integerz
such thatz ≤ a≤ a
. -
Int.ceil a
: Least integerz
such thata ≤ z≤ z
. -
Int.fract a
: Fractional part ofa
, defined asa - floor a
. -
round a
: Nearest integer toa
. It rounds halves towards infinity.
Notations #
⌊a⌋₊₊
isNat.floor a
.⌈a⌉₊₊
isNat.ceil a
.⌊a⌋
isInt.floor a
.⌈a⌉
isInt.ceil a
.
The index ₊₊
in the notations for Nat.floor
and Nat.ceil
is used in analogy to the notation
for nnnorm
.
TODO #
LinearOrderedRing
/LinearOrderedSemiring
can be relaxed to OrderedRing
/OrderedSemiring
in
many lemmas.
Tags #
rounding, floor, ceil
Floor semiring #
FloorSemiring.floor a
computes the greatest naturaln
such that(n : α) ≤ a≤ a
.floor : α → ℕFloorSemiring.ceil a
computes the least naturaln
such thata ≤ (n : α)≤ (n : α)
.ceil : α → ℕFloorSemiring.floor
of a negative element is zero.A natural number
n
is smaller thanFloorSemiring.floor a
iff its coercion toα
is smaller thana
.FloorSemiring.ceil
is the lower adjoint of the coercion↑ : ℕ → α↑ : ℕ → α→ α
.gc_ceil : GaloisConnection ceil Nat.cast
A FloorSemiring
is an ordered semiring over α
with a function
floor : α → ℕ→ ℕ
satisfying ∀ (n : ℕ) (x : α), n ≤ ⌊x⌋ ↔ (n : α) ≤ x)∀ (n : ℕ) (x : α), n ≤ ⌊x⌋ ↔ (n : α) ≤ x)≤ ⌊x⌋ ↔ (n : α) ≤ x)↔ (n : α) ≤ x)≤ x)
.
Note that many lemmas require a LinearOrder
. Please see the above TODO
.
Instances
Equations
- One or more equations did not get rendered due to their size.
⌊a⌋₊₊
is the greatest natural n
such that n ≤ a≤ a
. If a
is negative, then ⌊a⌋₊ = 0₊ = 0
.
Equations
- Nat.floor = FloorSemiring.floor
⌈a⌉₊₊
is the least natural n
such that a ≤ n≤ n
Equations
- Nat.ceil = FloorSemiring.ceil
⌊a⌋₊₊
is the greatest natural n
such that n ≤ a≤ a
. If a
is negative, then ⌊a⌋₊ = 0₊ = 0
.
Equations
- One or more equations did not get rendered due to their size.
⌈a⌉₊₊
is the least natural n
such that a ≤ n≤ n
Equations
- One or more equations did not get rendered due to their size.
Ceil #
Intervals #
Natural division is the floor of field division.
There exists at most one FloorSemiring
structure on a linear ordered semiring.
Floor rings #
FloorRing.floor a
computes the greatest integerz
such that(z : α) ≤ a≤ a
.floor : α → ℤFloorRing.ceil a
computes the least integerz
such thata ≤ (z : α)≤ (z : α)
.ceil : α → ℤFloorRing.ceil
is the upper adjoint of the coercion↑ : ℤ → α↑ : ℤ → α→ α
.gc_coe_floor : GaloisConnection Int.cast floorFloorRing.ceil
is the lower adjoint of the coercion↑ : ℤ → α↑ : ℤ → α→ α
.gc_ceil_coe : GaloisConnection ceil Int.cast
A FloorRing
is a linear ordered ring over α
with a function
floor : α → ℤ→ ℤ
satisfying ∀ (z : ℤ) (a : α), z ≤ floor a ↔ (z : α) ≤ a)∀ (z : ℤ) (a : α), z ≤ floor a ↔ (z : α) ≤ a)≤ floor a ↔ (z : α) ≤ a)↔ (z : α) ≤ a)≤ a)
.
Instances
Equations
- One or more equations did not get rendered due to their size.
A FloorRing
constructor from the floor
function alone.
Equations
- One or more equations did not get rendered due to their size.
A FloorRing
constructor from the ceil
function alone.
Equations
- One or more equations did not get rendered due to their size.
Int.floor a
is the greatest integer z
such that z ≤ a≤ a
. It is denoted with ⌊a⌋
.
Equations
- One or more equations did not get rendered due to their size.
Int.ceil a
is the smallest integer z
such that a ≤ z≤ z
. It is denoted with ⌈a⌉
.
Equations
- One or more equations did not get rendered due to their size.
Floor #
Fractional part #
Ceil #
Intervals #
Round #
A floor ring as a floor semiring #
Equations
- One or more equations did not get rendered due to their size.
There exists at most one FloorRing
structure on a given linear ordered ring.