Documentation

Mathlib.Algebra.Order.Floor.Defs

Floor and ceil #

We define the natural- and integer-valued floor and ceil functions on linearly ordered rings. We also provide positivity extensions to handle floor and ceil.

Main definitions #

Notations #

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 #

class FloorSemiring (α : Type u_4) [Semiring α] [PartialOrder α] :
Type u_4

A FloorSemiring is an ordered semiring over α with a function floor : α → ℕ satisfying ∀ (n : ℕ) (x : α), n ≤ ⌊x⌋ ↔ (n : α) ≤ x). Note that many lemmas require a LinearOrder. Please see the above TODO.

Instances
    def Nat.floor {α : Type u_2} [Semiring α] [PartialOrder α] [FloorSemiring α] :
    α

    ⌊a⌋₊ is the greatest natural n such that n ≤ a. If a is negative, then ⌊a⌋₊ = 0.

    Equations
      Instances For
        def Nat.ceil {α : Type u_2} [Semiring α] [PartialOrder α] [FloorSemiring α] :
        α

        ⌈a⌉₊ is the least natural n such that a ≤ n

        Equations
          Instances For
            @[simp]
            @[simp]

            ⌊a⌋₊ is the greatest natural n such that n ≤ a. If a is negative, then ⌊a⌋₊ = 0.

            Equations
              Instances For

                ⌈a⌉₊ is the least natural n such that a ≤ n

                Equations
                  Instances For
                    theorem Nat.le_floor_iff {α : Type u_2} [Semiring α] [PartialOrder α] [FloorSemiring α] {a : α} {n : } (ha : 0 a) :
                    n a⌋₊ n a
                    theorem Nat.le_floor {α : Type u_2} [Semiring α] [PartialOrder α] [FloorSemiring α] {a : α} {n : } [IsOrderedRing α] (h : n a) :
                    @[simp]
                    theorem Nat.ceil_le {α : Type u_2} [Semiring α] [PartialOrder α] [FloorSemiring α] {a : α} {n : } :
                    a⌉₊ n a n
                    theorem Nat.lt_ceil {α : Type u_2} [Semiring α] [LinearOrder α] [FloorSemiring α] {a : α} {n : } :
                    n < a⌉₊ n < a
                    @[simp]
                    theorem Nat.ceil_pos {α : Type u_2} [Semiring α] [LinearOrder α] [FloorSemiring α] {a : α} :
                    0 < a⌉₊ 0 < a

                    Floor rings #

                    class FloorRing (α : Type u_4) [Ring α] [LinearOrder α] :
                    Type u_4

                    A FloorRing is a linear ordered ring over α with a function floor : α → ℤ satisfying ∀ (z : ℤ) (a : α), z ≤ floor a ↔ (z : α) ≤ a).

                    Instances
                      def FloorRing.ofFloor (α : Type u_4) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (floor : α) (gc_coe_floor : GaloisConnection Int.cast floor) :

                      A FloorRing constructor from the floor function alone.

                      Equations
                        Instances For
                          def FloorRing.ofCeil (α : Type u_4) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (ceil : α) (gc_ceil_coe : GaloisConnection ceil Int.cast) :

                          A FloorRing constructor from the ceil function alone.

                          Equations
                            Instances For
                              def Int.floor {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] :
                              α

                              Int.floor a is the greatest integer z such that z ≤ a. It is denoted with ⌊a⌋.

                              Equations
                                Instances For
                                  def Int.ceil {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] :
                                  α

                                  Int.ceil a is the smallest integer z such that a ≤ z. It is denoted with ⌈a⌉.

                                  Equations
                                    Instances For
                                      def Int.fract {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] (a : α) :
                                      α

                                      Int.fract a the fractional part of a, is a minus its floor.

                                      Equations
                                        Instances For
                                          @[simp]
                                          @[simp]
                                          @[simp]
                                          theorem Int.fract_int :

                                          Int.floor a is the greatest integer z such that z ≤ a. It is denoted with ⌊a⌋.

                                          Equations
                                            Instances For

                                              Int.ceil a is the smallest integer z such that a ≤ z. It is denoted with ⌈a⌉.

                                              Equations
                                                Instances For

                                                  Floor #

                                                  theorem Int.le_floor {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {z : } {a : α} :
                                                  z a z a
                                                  theorem Int.floor_lt {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {z : } {a : α} :
                                                  a < z a < z
                                                  theorem Int.floor_le {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] (a : α) :
                                                  a a
                                                  theorem Int.floor_nonneg {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {a : α} :
                                                  0 a 0 a
                                                  theorem Int.floor_nonpos {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {a : α} [IsStrictOrderedRing α] (ha : a 0) :

                                                  Ceil #

                                                  theorem Int.ceil_le {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {z : } {a : α} :
                                                  a z a z
                                                  theorem Int.lt_ceil {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {z : } {a : α} :
                                                  z < a z < a
                                                  theorem Int.le_ceil {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] (a : α) :
                                                  a a
                                                  theorem Int.ceil_nonneg {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {a : α} [IsStrictOrderedRing α] (ha : 0 a) :
                                                  @[simp]
                                                  theorem Int.ceil_pos {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {a : α} :
                                                  0 < a 0 < a

                                                  A floor ring as a floor semiring #

                                                  @[instance 100]
                                                  Equations
                                                    theorem Int.floor_toNat {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (a : α) :
                                                    theorem Int.ceil_toNat {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (a : α) :

                                                    Extension for the positivity tactic: Int.floor is nonnegative if its input is.

                                                    Equations
                                                      Instances For

                                                        Extension for the positivity tactic: Nat.ceil is positive if its input is.

                                                        Equations
                                                          Instances For

                                                            Extension for the positivity tactic: Int.ceil is positive/nonnegative if its input is.

                                                            Equations
                                                              Instances For