Mathlib.Algebra.Order.Floor.Defs

FloorSemiring structure

(α) [Semiring α] [PartialOrder α]

Full source

/-- 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`. -/
class FloorSemiring (α) [Semiring α] [PartialOrder α] where
  /-- `FloorSemiring.floor a` computes the greatest natural `n` such that `(n : α) ≤ a`. -/
  floor : α → ℕ
  /-- `FloorSemiring.ceil a` computes the least natural `n` such that `a ≤ (n : α)`. -/
  ceil : α → ℕ
  /-- `FloorSemiring.floor` of a negative element is zero. -/
  floor_of_neg {a : α} (ha : a < 0) : floor a = 0
  /-- A natural number `n` is smaller than `FloorSemiring.floor a` iff its coercion to `α` is
  smaller than `a`. -/
  gc_floor {a : α} {n : ℕ} (ha : 0 ≤ a) : n ≤ floor a ↔ (n : α) ≤ a
  /-- `FloorSemiring.ceil` is the lower adjoint of the coercion `↑ : ℕ → α`. -/
  gc_ceil : GaloisConnection ceil (↑)

Floor Semiring

Informal description

A `FloorSemiring` is an ordered semiring `α` equipped with a floor function `floor : α → ℕ` satisfying the property that for any natural number `n` and any element `x` of `α`, the inequality `n ≤ floor x` holds if and only if the inequality `(n : α) ≤ x` holds in `α`. This structure provides a way to generalize the notion of floor from natural numbers to more general ordered semirings.

instFloorSemiringNat instance

: FloorSemiring ℕ

Full source

instance : FloorSemiring ℕ where
  floor := id
  ceil := id
  floor_of_neg ha := (Nat.not_lt_zero _ ha).elim
  gc_floor _ := by
    rw [Nat.cast_id, id_def]
  gc_ceil n a := by
    rw [Nat.cast_id, id_def]

Natural Numbers as a Floor Semiring

Informal description

The natural numbers $\mathbb{N}$ form a floor semiring, where the floor and ceil functions are the identity functions.

Nat.floor definition

: α → ℕ

Full source

/-- `⌊a⌋₊` is the greatest natural `n` such that `n ≤ a`. If `a` is negative, then `⌊a⌋₊ = 0`. -/
def floor : α → ℕ :=
  FloorSemiring.floor

Natural floor function

Informal description

For an element $a$ in a floor semiring $\alpha$, $\lfloor a \rfloor_\mathbb{N}$ is the greatest natural number $n$ such that $n \leq a$. If $a$ is negative, then $\lfloor a \rfloor_\mathbb{N} = 0$.

Nat.ceil definition

: α → ℕ

Full source

/-- `⌈a⌉₊` is the least natural `n` such that `a ≤ n` -/
def ceil : α → ℕ :=
  FloorSemiring.ceil

Natural ceil function

Informal description

For an element $a$ in a floor semiring $\alpha$, $\lceil a \rceil_\mathbb{N}$ is the smallest natural number $n$ such that $a \leq n$.

Nat.floor_nat theorem

: (Nat.floor : ℕ → ℕ) = id

Full source

@[simp]
theorem floor_nat : (Nat.floor : ℕ → ℕ) = id :=
  rfl

Natural Floor Function is Identity on Natural Numbers

Informal description

The natural-valued floor function $\lfloor \cdot \rfloor_\mathbb{N}$ on natural numbers is the identity function, i.e., $\lfloor n \rfloor_\mathbb{N} = n$ for all $n \in \mathbb{N}$.

Nat.ceil_nat theorem

: (Nat.ceil : ℕ → ℕ) = id

Full source

@[simp]
theorem ceil_nat : (Nat.ceil : ℕ → ℕ) = id :=
  rfl

Natural Ceil Function is Identity on Natural Numbers

Informal description

The natural-valued ceil function $\lceil \cdot \rceil_\mathbb{N}$ on natural numbers is the identity function, i.e., $\lceil n \rceil_\mathbb{N} = n$ for all $n \in \mathbb{N}$.

Nat.term⌊_⌋₊ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
notation "⌊" a "⌋₊" => Nat.floor a

Natural floor notation

Informal description

The notation `⌊a⌋₊` represents the natural-valued floor function applied to `a`, which gives the greatest natural number `n` such that `n ≤ a`. If `a` is negative, it returns `0`.

Nat.term⌈_⌉₊ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
notation "⌈" a "⌉₊" => Nat.ceil a

Natural ceiling notation

Informal description

The notation `⌈a⌉₊` represents the least natural number `n` such that `a ≤ n`, where `a` is an element of a linearly ordered semiring. This is the natural number ceiling function.

Nat.le_floor_iff theorem

(ha : 0 ≤ a) : n ≤ ⌊a⌋₊ ↔ (n : α) ≤ a

Full source

theorem le_floor_iff (ha : 0 ≤ a) : n ≤ ⌊a⌋₊ ↔ (n : α) ≤ a :=
  FloorSemiring.gc_floor ha

Natural Floor Comparison Criterion

Informal description

For an element $a$ in a floor semiring $\alpha$ with $0 \leq a$, and for any natural number $n$, we have $n \leq \lfloor a \rfloor_\mathbb{N}$ if and only if $n \leq a$ (where $n$ is considered as an element of $\alpha$ via the canonical embedding).

Nat.le_floor theorem

[IsOrderedRing α] (h : (n : α) ≤ a) : n ≤ ⌊a⌋₊

Full source

theorem le_floor [IsOrderedRing α] (h : (n : α) ≤ a) : n ≤ ⌊a⌋₊ :=
  (le_floor_iff <| n.cast_nonneg.trans h).2 h

Natural Floor Lower Bound Property

Informal description

For any element $a$ in a floor semiring $\alpha$ and any natural number $n$, if $n \leq a$ (where $n$ is considered as an element of $\alpha$ via the canonical embedding), then $n \leq \lfloor a \rfloor_\mathbb{N}$.

Nat.gc_ceil_coe theorem

: GaloisConnection (ceil : α → ℕ) (↑)

Full source

theorem gc_ceil_coe : GaloisConnection (ceil : α → ℕ) (↑) :=
  FloorSemiring.gc_ceil

Galois Connection Between Natural Ceil and Canonical Embedding

Informal description

For any element $a$ in a floor semiring $\alpha$, the natural ceil function $\lceil a \rceil_\mathbb{N}$ and the canonical embedding of natural numbers into $\alpha$ form a Galois connection. That is, for any natural number $n$, we have $\lceil a \rceil_\mathbb{N} \leq n$ if and only if $a \leq n$ (where $n$ is considered as an element of $\alpha$ via the canonical embedding).

Nat.ceil_le theorem

: ⌈a⌉₊ ≤ n ↔ a ≤ n

Full source

@[simp]
theorem ceil_le : ⌈a⌉₊⌈a⌉₊ ≤ n ↔ a ≤ n :=
  gc_ceil_coe _ _

Natural Ceil Upper Bound Property: $\lceil a \rceil_\mathbb{N} \leq n \leftrightarrow a \leq n$

Informal description

For any element $a$ in a floor semiring $\alpha$ and any natural number $n$, the inequality $\lceil a \rceil_\mathbb{N} \leq n$ holds if and only if $a \leq n$ (where $n$ is considered as an element of $\alpha$ via the canonical embedding).

Nat.lt_ceil theorem

: n < ⌈a⌉₊ ↔ (n : α) < a

Full source

theorem lt_ceil : n < ⌈a⌉₊ ↔ (n : α) < a :=
  lt_iff_lt_of_le_iff_le ceil_le

Natural Ceil Lower Bound Property: $n < \lceil a \rceil_\mathbb{N} \leftrightarrow n < a$

Informal description

For any element $a$ in a floor semiring $\alpha$ and any natural number $n$, the inequality $n < \lceil a \rceil_\mathbb{N}$ holds if and only if $n < a$ (where $n$ is considered as an element of $\alpha$ via the canonical embedding).

Nat.ceil_pos theorem

: 0 < ⌈a⌉₊ ↔ 0 < a

Full source

@[simp]
theorem ceil_pos : 0 < ⌈a⌉₊ ↔ 0 < a := by rw [lt_ceil, cast_zero]

Positivity of Natural Ceil: $0 < \lceil a \rceil_\mathbb{N} \leftrightarrow 0 < a$

Informal description

For any element $a$ in a floor semiring $\alpha$, the ceil of $a$ is positive if and only if $a$ is positive, i.e., $0 < \lceil a \rceil_\mathbb{N} \leftrightarrow 0 < a$.

FloorRing structure

(α) [Ring α] [LinearOrder α]

Full source

/-- A `FloorRing` is a linear ordered ring over `α` with a function
`floor : α → ℤ` satisfying `∀ (z : ℤ) (a : α), z ≤ floor a ↔ (z : α) ≤ a)`.
-/
class FloorRing (α) [Ring α] [LinearOrder α] where
  /-- `FloorRing.floor a` computes the greatest integer `z` such that `(z : α) ≤ a`. -/
  floor : α → ℤ
  /-- `FloorRing.ceil a` computes the least integer `z` such that `a ≤ (z : α)`. -/
  ceil : α → ℤ
  /-- `FloorRing.ceil` is the upper adjoint of the coercion `↑ : ℤ → α`. -/
  gc_coe_floor : GaloisConnection (↑) floor
  /-- `FloorRing.ceil` is the lower adjoint of the coercion `↑ : ℤ → α`. -/
  gc_ceil_coe : GaloisConnection ceil (↑)

Linearly Ordered Ring with Floor Function

Informal description

A `FloorRing` is a linearly ordered ring $\alpha$ equipped with a floor function $\lfloor \cdot \rfloor : \alpha \to \mathbb{Z}$ satisfying the Galois connection property: for all integers $z$ and elements $a \in \alpha$, $z \leq \lfloor a \rfloor$ if and only if $z \leq a$ (where $z$ is coerced to $\alpha$).

instFloorRingInt instance

: FloorRing ℤ

Full source

instance : FloorRing ℤ where
  floor := id
  ceil := id
  gc_coe_floor a b := by
    rw [Int.cast_id, id_def]
  gc_ceil_coe a b := by
    rw [Int.cast_id, id_def]

The Floor Ring Structure on Integers

Informal description

The integers $\mathbb{Z}$ form a linearly ordered ring with the canonical floor function $\lfloor \cdot \rfloor : \mathbb{Z} \to \mathbb{Z}$ given by the identity map.

FloorRing.ofFloor definition

 (α) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (floor : α → ℤ) (gc_coe_floor : GaloisConnection (↑) floor) :
  FloorRing α

Full source

/-- A `FloorRing` constructor from the `floor` function alone. -/
def FloorRing.ofFloor (α) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (floor : α → ℤ)
    (gc_coe_floor : GaloisConnection (↑) floor) : FloorRing α :=
  { floor
    ceil := fun a => -floor (-a)
    gc_coe_floor
    gc_ceil_coe := fun a z => by rw [neg_le, ← gc_coe_floor, Int.cast_neg, neg_le_neg_iff] }

Construction of a Floor Ring from a Floor Function with Galois Connection

Informal description

Given a linearly ordered ring $\alpha$ with a strict order, and a function $\lfloor \cdot \rfloor : \alpha \to \mathbb{Z}$ satisfying the Galois connection property (i.e., for all integers $z$ and elements $a \in \alpha$, $z \leq \lfloor a \rfloor$ if and only if $z \leq a$), this constructs a `FloorRing` structure on $\alpha$ where the ceiling function is defined as $\lceil a \rceil = -\lfloor -a \rfloor$.

FloorRing.ofCeil definition

 (α) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (ceil : α → ℤ) (gc_ceil_coe : GaloisConnection ceil (↑)) :
  FloorRing α

Full source

/-- A `FloorRing` constructor from the `ceil` function alone. -/
def FloorRing.ofCeil (α) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (ceil : α → ℤ)
    (gc_ceil_coe : GaloisConnection ceil (↑)) : FloorRing α :=
  { floor := fun a => -ceil (-a)
    ceil
    gc_coe_floor := fun a z => by rw [le_neg, gc_ceil_coe, Int.cast_neg, neg_le_neg_iff]
    gc_ceil_coe }

Construction of a Floor Ring from a Ceiling Function with Galois Connection

Informal description

Given a linearly ordered ring $\alpha$ with a strict order, and a function $\lceil \cdot \rceil : \alpha \to \mathbb{Z}$ satisfying the Galois connection property (i.e., for all elements $a \in \alpha$ and integers $z$, $\lceil a \rceil \leq z$ if and only if $a \leq z$), this constructs a `FloorRing` structure on $\alpha$ where the floor function is defined as $\lfloor a \rfloor = -\lceil -a \rceil$.

Int.floor definition

: α → ℤ

Full source

/-- `Int.floor a` is the greatest integer `z` such that `z ≤ a`. It is denoted with `⌊a⌋`. -/
def floor : α → ℤ :=
  FloorRing.floor

Floor function

Informal description

For an element $a$ in a linearly ordered ring $\alpha$, the floor function $\lfloor a \rfloor$ returns the greatest integer $z$ such that $z \leq a$.

Int.ceil definition

: α → ℤ

Full source

/-- `Int.ceil a` is the smallest integer `z` such that `a ≤ z`. It is denoted with `⌈a⌉`. -/
def ceil : α → ℤ :=
  FloorRing.ceil

Ceiling function

Informal description

For an element $a$ in a linearly ordered ring $\alpha$, the ceiling function $\lceil a \rceil$ returns the smallest integer $z$ such that $a \leq z$.

Int.fract definition

(a : α) : α

Full source

/-- `Int.fract a` the fractional part of `a`, is `a` minus its floor. -/
def fract (a : α) : α :=
  a - floor a

Fractional part of an element in a linearly ordered ring

Informal description

For an element $a$ in a linearly ordered ring $\alpha$, the fractional part $\text{fract}(a)$ is defined as $a - \lfloor a \rfloor$, where $\lfloor a \rfloor$ is the floor of $a$.

Int.floor_int theorem

: (Int.floor : ℤ → ℤ) = id

Full source

@[simp]
theorem floor_int : (Int.floor : ℤ → ℤ) = id :=
  rfl

Floor Function as Identity on Integers

Informal description

The floor function on the integers $\mathbb{Z}$ is the identity function, i.e., for any integer $z \in \mathbb{Z}$, we have $\lfloor z \rfloor = z$.

Int.ceil_int theorem

: (Int.ceil : ℤ → ℤ) = id

Full source

@[simp]
theorem ceil_int : (Int.ceil : ℤ → ℤ) = id :=
  rfl

Ceiling Function as Identity on Integers

Informal description

The ceiling function on the integers $\mathbb{Z}$ is the identity function, i.e., for any integer $z \in \mathbb{Z}$, we have $\lceil z \rceil = z$.

Int.fract_int theorem

: (Int.fract : ℤ → ℤ) = 0

Full source

@[simp]
theorem fract_int : (Int.fract : ℤ → ℤ) = 0 :=
  funext fun x => by simp [fract]

Fractional Part Vanishes on Integers

Informal description

The fractional part function on the integers $\mathbb{Z}$ is identically zero, i.e., for any integer $z \in \mathbb{Z}$, we have $\text{fract}(z) = 0$.

Int.term⌊_⌋ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
notation "⌊" a "⌋" => Int.floor a

Floor function notation

Informal description

The notation `⌊a⌋` represents the floor function applied to `a`, which returns the greatest integer less than or equal to `a`.

Int.term⌈_⌉ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
notation "⌈" a "⌉" => Int.ceil a

Ceiling notation

Informal description

The notation `⌈a⌉` represents the ceiling function applied to `a`, which is the least integer greater than or equal to `a`.

Int.floorRing_floor_eq theorem

: @FloorRing.floor = @Int.floor

Full source

@[simp]
theorem floorRing_floor_eq : @FloorRing.floor = @Int.floor :=
  rfl

Equality of Floor Functions in a Floor Ring

Informal description

In a linearly ordered ring $\alpha$ with a floor function, the floor function defined in the `FloorRing` structure coincides with the integer-valued floor function $\lfloor \cdot \rfloor : \alpha \to \mathbb{Z}$.

Int.floorRing_ceil_eq theorem

: @FloorRing.ceil = @Int.ceil

Full source

@[simp]
theorem floorRing_ceil_eq : @FloorRing.ceil = @Int.ceil :=
  rfl

Equality of Ceiling Functions in a Floor Ring

Informal description

In a linearly ordered ring $\alpha$ with a floor function, the ceiling function defined in the `FloorRing` structure coincides with the integer-valued ceiling function $\lceil \cdot \rceil : \alpha \to \mathbb{Z}$.

Int.gc_coe_floor theorem

: GaloisConnection ((↑) : ℤ → α) floor

Full source

theorem gc_coe_floor : GaloisConnection ((↑) : ℤ → α) floor :=
  FloorRing.gc_coe_floor

Galois Connection Between Integer Embedding and Floor Function

Informal description

The canonical embedding from the integers $\mathbb{Z}$ to a linearly ordered ring $\alpha$ and the floor function $\lfloor \cdot \rfloor : \alpha \to \mathbb{Z}$ form a Galois connection. That is, for any integer $z \in \mathbb{Z}$ and any element $a \in \alpha$, we have $z \leq \lfloor a \rfloor$ if and only if $(z : \alpha) \leq a$.

Int.le_floor theorem

: z ≤ ⌊a⌋ ↔ (z : α) ≤ a

Full source

theorem le_floor : z ≤ ⌊a⌋ ↔ (z : α) ≤ a :=
  (gc_coe_floor z a).symm

Galois Connection Property of Floor Function: $z \leq \lfloor a \rfloor \leftrightarrow (z : \alpha) \leq a$

Informal description

For any integer $z$ and any element $a$ in a linearly ordered ring $\alpha$, the inequality $z \leq \lfloor a \rfloor$ holds if and only if the canonical embedding of $z$ into $\alpha$ satisfies $(z : \alpha) \leq a$.

Int.floor_lt theorem

: ⌊a⌋ < z ↔ a < z

Full source

theorem floor_lt : ⌊a⌋⌊a⌋ < z ↔ a < z :=
  lt_iff_lt_of_le_iff_le le_floor

Floor Strict Inequality: $\lfloor a \rfloor < z \leftrightarrow a < z$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$ and any integer $z$, the floor of $a$ is strictly less than $z$ if and only if $a$ is strictly less than $z$ (where $z$ is viewed in $\alpha$ via the canonical embedding). In other words, $\lfloor a \rfloor < z \leftrightarrow a < z$.

Int.floor_le theorem

(a : α) : (⌊a⌋ : α) ≤ a

Full source

@[bound]
theorem floor_le (a : α) : (⌊a⌋ : α) ≤ a :=
  gc_coe_floor.l_u_le a

Floor Function Lower Bound: $\lfloor a \rfloor \leq a$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the floor of $a$ (denoted $\lfloor a \rfloor$) satisfies $\lfloor a \rfloor \leq a$ when viewed as an element of $\alpha$ via the canonical embedding $\mathbb{Z} \to \alpha$.

Int.floor_nonneg theorem

: 0 ≤ ⌊a⌋ ↔ 0 ≤ a

Full source

theorem floor_nonneg : 0 ≤ ⌊a⌋ ↔ 0 ≤ a := by rw [le_floor, Int.cast_zero]

Non-negativity of Floor Function: $0 \leq \lfloor a \rfloor \leftrightarrow 0 \leq a$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the floor of $a$ is non-negative if and only if $a$ itself is non-negative, i.e., $0 \leq \lfloor a \rfloor \leftrightarrow 0 \leq a$.

Int.floor_nonpos theorem

[IsStrictOrderedRing α] (ha : a ≤ 0) : ⌊a⌋ ≤ 0

Full source

@[bound]
theorem floor_nonpos [IsStrictOrderedRing α] (ha : a ≤ 0) : ⌊a⌋ ≤ 0 := by
  rw [← @cast_le α, Int.cast_zero]
  exact (floor_le a).trans ha

Floor of Nonpositive Element is Nonpositive

Informal description

For any element $a$ in a strictly ordered ring $\alpha$ such that $a \leq 0$, the floor of $a$ satisfies $\lfloor a \rfloor \leq 0$.

Int.gc_ceil_coe theorem

: GaloisConnection ceil ((↑) : ℤ → α)

Full source

theorem gc_ceil_coe : GaloisConnection ceil ((↑) : ℤ → α) :=
  FloorRing.gc_ceil_coe

Galois Connection Between Ceiling Function and Integer Embedding

Informal description

The ceiling function $\lceil \cdot \rceil$ and the canonical embedding of integers into a linearly ordered ring $\alpha$ form a Galois connection. That is, for any integer $z$ and any element $a \in \alpha$, we have $\lceil a \rceil \leq z$ if and only if $a \leq z$ (where $z$ is viewed as an element of $\alpha$ via the embedding).

Int.ceil_le theorem

: ⌈a⌉ ≤ z ↔ a ≤ z

Full source

theorem ceil_le : ⌈a⌉⌈a⌉ ≤ z ↔ a ≤ z :=
  gc_ceil_coe a z

Ceiling Comparison: $\lceil a \rceil \leq z \leftrightarrow a \leq z$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$ and any integer $z$, the ceiling of $a$ is less than or equal to $z$ if and only if $a$ is less than or equal to $z$ (where $z$ is viewed as an element of $\alpha$ via the canonical embedding).

Int.lt_ceil theorem

: z < ⌈a⌉ ↔ (z : α) < a

Full source

theorem lt_ceil : z < ⌈a⌉ ↔ (z : α) < a :=
  lt_iff_lt_of_le_iff_le ceil_le

Strict Inequality Characterization of Ceiling Function: $z < \lceil a \rceil \leftrightarrow (z : \alpha) < a$

Informal description

For any integer $z$ and any element $a$ in a linearly ordered ring $\alpha$, the integer $z$ is strictly less than the ceiling of $a$ if and only if the canonical embedding of $z$ into $\alpha$ is strictly less than $a$. In other words, $z < \lceil a \rceil \leftrightarrow (z : \alpha) < a$.

Int.le_ceil theorem

(a : α) : a ≤ ⌈a⌉

Full source

@[bound]
theorem le_ceil (a : α) : a ≤ ⌈a⌉ :=
  gc_ceil_coe.le_u_l a

Element is Less Than or Equal to its Ceiling

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the ceiling of $a$ is greater than or equal to $a$, i.e., $a \leq \lceil a \rceil$.

Int.ceil_nonneg theorem

[IsStrictOrderedRing α] (ha : 0 ≤ a) : 0 ≤ ⌈a⌉

Full source

@[bound]
theorem ceil_nonneg [IsStrictOrderedRing α] (ha : 0 ≤ a) : 0 ≤ ⌈a⌉ := mod_cast ha.trans (le_ceil a)

Nonnegativity of Ceiling for Nonnegative Elements

Informal description

For any element $a$ in a strictly ordered ring $\alpha$, if $0 \leq a$, then the ceiling of $a$ is nonnegative, i.e., $0 \leq \lceil a \rceil$.

Int.ceil_pos theorem

: 0 < ⌈a⌉ ↔ 0 < a

Full source

@[simp]
theorem ceil_pos : 0 < ⌈a⌉ ↔ 0 < a := by rw [lt_ceil, cast_zero]

Positivity of Ceiling: $0 < \lceil a \rceil \leftrightarrow 0 < a$

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the ceiling of $a$ is positive if and only if $a$ is positive, i.e., $0 < \lceil a \rceil \leftrightarrow 0 < a$.

FloorRing.toFloorSemiring instance

: FloorSemiring α

Full source

instance (priority := 100) FloorRing.toFloorSemiring : FloorSemiring α where
  floor a := ⌊a⌋.toNat
  ceil a := ⌈a⌉.toNat
  floor_of_neg {_} ha := Int.toNat_of_nonpos (Int.floor_nonpos ha.le)
  gc_floor {a n} ha := by rw [Int.le_toNat (Int.floor_nonneg.2 ha), Int.le_floor, Int.cast_natCast]
  gc_ceil a n := by rw [Int.toNat_le, Int.ceil_le, Int.cast_natCast]

Linearly Ordered Ring as a Floor Semiring

Informal description

Every linearly ordered ring $\alpha$ with a floor function is also a floor semiring. This means that the floor function on $\alpha$ can be naturally restricted to a floor function taking values in the natural numbers, where for any $a \in \alpha$, $\lfloor a \rfloor_\mathbb{N}$ is the greatest natural number $n$ such that $n \leq a$.

Int.floor_toNat theorem

(a : α) : ⌊a⌋.toNat = ⌊a⌋₊

Full source

theorem Int.floor_toNat (a : α) : ⌊a⌋.toNat = ⌊a⌋₊ :=
  rfl

Equivalence of Integer Floor and Natural Floor via `toNat`

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the natural number obtained by applying the `toNat` function to the floor $\lfloor a \rfloor$ is equal to the natural floor $\lfloor a \rfloor_\mathbb{N}$ of $a$. In other words, $\text{toNat}(\lfloor a \rfloor) = \lfloor a \rfloor_\mathbb{N}$.

Int.ceil_toNat theorem

(a : α) : ⌈a⌉.toNat = ⌈a⌉₊

Full source

theorem Int.ceil_toNat (a : α) : ⌈a⌉.toNat = ⌈a⌉₊ :=
  rfl

Equivalence of Integer Ceiling and Natural Ceiling via `toNat`

Informal description

For any element $a$ in a linearly ordered ring $\alpha$, the natural number obtained by applying the `toNat` function to the ceiling $\lceil a \rceil$ is equal to the natural ceiling $\lceil a \rceil_\mathbb{N}$ of $a$. In other words, $\text{toNat}(\lceil a \rceil) = \lceil a \rceil_\mathbb{N}$.

Nat.floor_int theorem

: (Nat.floor : ℤ → ℕ) = Int.toNat

Full source

@[simp]
theorem Nat.floor_int : (Nat.floor : ℤ → ℕ) = Int.toNat :=
  rfl

Natural Floor on Integers Equals Canonical Natural Conversion

Informal description

The natural floor function $\lfloor \cdot \rfloor_\mathbb{N}$ restricted to the integers $\mathbb{Z}$ coincides with the canonical function mapping integers to natural numbers, i.e., $\lfloor z \rfloor_\mathbb{N} = \text{toNat}(z)$ for all $z \in \mathbb{Z}$.

Nat.ceil_int theorem

: (Nat.ceil : ℤ → ℕ) = Int.toNat

Full source

@[simp]
theorem Nat.ceil_int : (Nat.ceil : ℤ → ℕ) = Int.toNat :=
  rfl

Natural Ceil on Integers Equals Canonical Natural Conversion

Informal description

The natural ceil function $\lceil \cdot \rceil_\mathbb{N}$ restricted to the integers $\mathbb{Z}$ coincides with the canonical function mapping integers to natural numbers, i.e., $\lceil z \rceil_\mathbb{N} = \text{toNat}(z)$ for all $z \in \mathbb{Z}$.

Mathlib.Meta.Positivity.evalIntFloor definition

: PositivityExt

Full source

/-- Extension for the `positivity` tactic: `Int.floor` is nonnegative if its input is. -/
@[positivity ⌊_⌋]
def evalIntFloor : PositivityExt where eval {u α} _zα _pα e := do
  match u, α, e with
  | 0, ~q(ℤ), ~q(@Int.floor $α' $ir $io $j $a) =>
    match ← core q(inferInstance) q(inferInstance) a with
    | .positive pa =>
        assertInstancesCommute
        pure (.nonnegative q(int_floor_nonneg_of_pos (α := $α') $pa))
    | .nonnegative pa =>
        assertInstancesCommute
        pure (.nonnegative q(int_floor_nonneg (α := $α') $pa))
    | _ => pure .none
  | _, _, _ => throwError "failed to match on Int.floor application"

Positivity extension for integer floor function

Informal description

The `positivity` tactic extension for `Int.floor`, which proves that the floor of an integer is nonnegative if its input is nonnegative.

Mathlib.Meta.Positivity.evalNatCeil definition

: PositivityExt

Full source

/-- Extension for the `positivity` tactic: `Nat.ceil` is positive if its input is. -/
@[positivity ⌈_⌉₊]
def evalNatCeil : PositivityExt where eval {u α} _zα _pα e := do
  match u, α, e with
  | 0, ~q(ℕ), ~q(@Nat.ceil $α' $ir $io $j $a) =>
    let _i ← synthInstanceQ q(LinearOrder $α')
    let _i ← synthInstanceQ q(IsStrictOrderedRing $α')
    assertInstancesCommute
    match ← core q(inferInstance) q(inferInstance) a with
    | .positive pa =>
      assertInstancesCommute
      pure (.positive q(nat_ceil_pos (α := $α') $pa))
    | _ => pure .none
  | _, _, _ => throwError "failed to match on Nat.ceil application"

Positivity of natural ceiling function

Informal description

The positivity tactic extension for `Nat.ceil` proves that the ceiling of a positive element in a linearly ordered semiring is positive. Specifically, for any element `a` in a linearly ordered semiring `α`, if `a` is positive, then `⌈a⌉₊` (the natural ceiling of `a`) is also positive.

Mathlib.Meta.Positivity.evalIntCeil definition

: PositivityExt

Full source

/-- Extension for the `positivity` tactic: `Int.ceil` is positive/nonnegative if its input is. -/
@[positivity ⌈_⌉]
def evalIntCeil : PositivityExt where eval {u α} _zα _pα e := do
  match u, α, e with
  | 0, ~q(ℤ), ~q(@Int.ceil $α' $ir $io $j $a) =>
    match ← core q(inferInstance) q(inferInstance) a with
    | .positive pa =>
        assertInstancesCommute
        pure (.positive q(int_ceil_pos (α := $α') $pa))
    | .nonnegative pa =>
        let _i ← synthInstanceQ q(IsStrictOrderedRing $α')
        assertInstancesCommute
        pure (.nonnegative q(Int.ceil_nonneg (α := $α') $pa))
    | _ => pure .none
  | _, _, _ => throwError "failed to match on Int.ceil application"

Positivity extension for integer ceiling function

Informal description

The `evalIntCeil` function is a positivity tactic extension that determines if the ceiling of an integer is positive or nonnegative based on the input value. Specifically: - If the input `a` is positive, then `⌈a⌉` is positive. - If the input `a` is nonnegative, then `⌈a⌉` is nonnegative.

Mathlib.Algebra.Order.Floor.Defs

Main definitions

Notations

TODO

Tags