Extended floor and ceil #

This file defines the extended floor and ceil functions ENat.floor, ENat.ceil : ℝ≥0∞ → ℕ∞.

Main declarations #

ENat.floor r: Greatest extended natural n such that n ≤ r.
ENat.ceil r: Least extended natural n such that r ≤ n.

Notation #

⌊r⌋ₑ is ENat.floor r.
⌈r⌉ₑ is ENat.ceil r.

The index ₑ is used in analogy to the notation for enorm.

TODO #

The day Mathlib acquires ENNRat, it would be good to generalise this file to an EFloorSemiring typeclass.

Tags #

efloor, eceil

source

noncomputable def ENat.floor :

ENNReal → ℕ∞

⌊r⌋ₑ is the greatest extended natural n such that n ≤ r.

Equations

⌊none ⌋ₑ = ⊤
⌊some r⌋ₑ = ↑⌊r⌋₊

Instances For

source

noncomputable def ENat.ceil :

ENNReal → ℕ∞

⌈r⌉ₑ is the least extended natural n such that r ≤ n

Equations

⌈none ⌉ₑ = ⊤
⌈some r⌉ₑ = ↑⌈r⌉₊

Instances For

source

def ENat.«term⌊_⌋ₑ» :

Lean.ParserDescr

⌊r⌋ₑ is the greatest extended natural n such that n ≤ r.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def ENat.«term⌈_⌉ₑ» :

Lean.ParserDescr

⌈r⌉ₑ is the least extended natural n such that r ≤ n

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem ENat.floor_top :

⌊⊤⌋ₑ = ⊤

source

@[simp]

theorem ENat.ceil_top :

⌈⊤⌉ₑ = ⊤

source

@[simp]

theorem ENat.floor_coe (r : NNReal) :

⌊↑r⌋ₑ = ↑⌊r⌋₊

source

@[simp]

theorem ENat.ceil_coe (r : NNReal) :

⌈↑r⌉ₑ = ↑⌈r⌉₊

source

@[simp]

theorem ENat.floor_eq_top {r : ENNReal} :

⌊r⌋ₑ = ⊤ ↔ r = ⊤

source

@[simp]

theorem ENat.ceil_eq_top {r : ENNReal} :

⌈r⌉ₑ = ⊤ ↔ r = ⊤

source

theorem ENat.floor_lt_top {r : ENNReal} :

⌊r⌋ₑ < ⊤ ↔ r < ⊤

source

@[simp]

theorem ENat.ceil_lt_top {r : ENNReal} :

⌈r⌉ₑ < ⊤ ↔ r < ⊤

source

@[simp]

theorem ENat.le_floor {r : ENNReal} {n : ℕ∞} :

n ≤ ⌊r⌋ₑ ↔ ↑n ≤ r

source

@[simp]

theorem ENat.ceil_le {r : ENNReal} {n : ℕ∞} :

⌈r⌉ₑ ≤ n ↔ r ≤ ↑n

source

@[simp]

theorem ENat.floor_lt {r : ENNReal} {n : ℕ∞} :

⌊r⌋ₑ < n ↔ r < ↑n

source

@[simp]

theorem ENat.lt_ceil {r : ENNReal} {n : ℕ∞} :

n < ⌈r⌉ₑ ↔ ↑n < r

source

theorem ENat.gc_toENNReal_floor :

GaloisConnection toENNReal floor

source

theorem ENat.gc_ceil_toENNReal :

GaloisConnection ceil toENNReal

source

theorem ENat.floor_le_self {r : ENNReal} :

↑⌊r⌋ₑ ≤ r

source

theorem ENat.le_ceil_self {r : ENNReal} :

r ≤ ↑⌈r⌉ₑ

source

@[simp]

theorem ENat.floor_le {r : ENNReal} {n : ℕ∞} (hn : n ≠ ⊤) :

⌊r⌋ₑ ≤ n ↔ r < ↑n + 1

source

@[simp]

theorem ENat.le_ceil {r : ENNReal} {n : ℕ∞} (hn₀ : n ≠ 0) (hn : n ≠ ⊤) :

n ≤ ⌈r⌉ₑ ↔ ↑n - 1 < r

source

@[simp]

theorem ENat.lt_floor {r : ENNReal} {n : ℕ∞} (hn : n ≠ ⊤) :

n < ⌊r⌋ₑ ↔ ↑n + 1 ≤ r

source

@[simp]

theorem ENat.ceil_lt {r : ENNReal} {n : ℕ∞} (hn₀ : n ≠ 0) (hn : n ≠ ⊤) :

⌈r⌉ₑ < n ↔ r ≤ ↑n - 1

source

theorem ENat.floor_mono :

Monotone floor

source

theorem ENat.ceil_mono :

Monotone ceil

source

theorem ENat.floor_le_floor {r s : ENNReal} (hrs : r ≤ s) :

⌊r⌋ₑ ≤ ⌊s⌋ₑ

source

theorem ENat.ceil_le_ceil {r s : ENNReal} (hrs : r ≤ s) :

⌈r⌉ₑ ≤ ⌈s⌉ₑ

source

@[simp]

theorem ENat.floor_natCast (n : ℕ∞) :

⌊↑n⌋ₑ = n

source

@[simp]

theorem ENat.ceil_natCast (n : ℕ∞) :

⌈↑n⌉ₑ = n

source

@[simp]

theorem ENat.floor_zero :

⌊0⌋ₑ = 0

source

@[simp]

theorem ENat.ceil_zero :

⌈0⌉ₑ = 0

source

@[simp]

theorem ENat.floor_one :

⌊1⌋ₑ = 1

source

@[simp]

theorem ENat.ceil_one :

⌈1⌉ₑ = 1

source

@[simp]

theorem ENat.floor_ofNat (n : ℕ) [n.AtLeastTwo] :

⌊OfNat.ofNat n⌋ₑ = OfNat.ofNat n

source

@[simp]

theorem ENat.ceil_ofNat (n : ℕ) [n.AtLeastTwo] :

⌈OfNat.ofNat n⌉ₑ = OfNat.ofNat n

source

theorem ENat.floor_pos {r : ENNReal} :

0 < ⌊r⌋ₑ ↔ 1 ≤ r

source

theorem ENat.ceil_pos {r : ENNReal} :

0 < ⌈r⌉ₑ ↔ 0 < r

source

@[simp]

theorem ENat.floor_eq_zero {r : ENNReal} :

⌊r⌋ₑ = 0 ↔ r < 1

source

@[simp]

theorem ENat.ceil_eq_zero {r : ENNReal} :

⌈r⌉ₑ = 0 ↔ r = 0

source

theorem ENat.floor_le_ceil {r : ENNReal} :

⌊r⌋ₑ ≤ ⌈r⌉ₑ

source

theorem ENat.ceil_le_floor_add_one (r : ENNReal) :

⌈r⌉ₑ ≤ ⌊r⌋ₑ + 1

source

theorem ENat.floor_lt_ceil {r s : ENNReal} (hrs : r < s) :

⌊r⌋ₑ < ⌈s⌉ₑ

source

theorem ENat.floor_congr {r s : ENNReal} (h : ∀ (n : ℕ∞), ↑n ≤ r ↔ ↑n ≤ s) :

⌊r⌋ₑ = ⌊s⌋ₑ

source

theorem ENat.ceil_congr {r s : ENNReal} (h : ∀ (n : ℕ∞), r ≤ ↑n ↔ s ≤ ↑n) :

⌈r⌉ₑ = ⌈s⌉ₑ

source

@[simp]

theorem ENat.floor_add_toENNReal (r : ENNReal) (n : ℕ∞) :

⌊r + ↑n⌋ₑ = ⌊r⌋ₑ + n

source

@[simp]

theorem ENat.ceil_add_toENNReal (r : ENNReal) (n : ℕ∞) :

⌈r + ↑n⌉ₑ = ⌈r⌉ₑ + n

source

@[simp]

theorem ENat.floor_toENNReal_add (r : ENNReal) (n : ℕ∞) :

⌊↑n + r⌋ₑ = n + ⌊r⌋ₑ

source

@[simp]

theorem ENat.ceil_toENNReal_add (r : ENNReal) (n : ℕ∞) :

⌈↑n + r⌉ₑ = n + ⌈r⌉ₑ

source

@[simp]

theorem ENat.floor_add_natCast (r : ENNReal) (n : ℕ) :

⌊r + ↑n⌋ₑ = ⌊r⌋ₑ + ↑n

source

@[simp]

theorem ENat.ceil_add_natCast (r : ENNReal) (n : ℕ) :

⌈r + ↑n⌉ₑ = ⌈r⌉ₑ + ↑n

source

@[simp]

theorem ENat.floor_natCast_add (r : ENNReal) (n : ℕ) :

⌊↑n + r⌋ₑ = ↑n + ⌊r⌋ₑ

source

@[simp]

theorem ENat.ceil_natCast_add (r : ENNReal) (n : ℕ) :

⌈↑n + r⌉ₑ = ↑n + ⌈r⌉ₑ

source

@[simp]

theorem ENat.floor_add_one (r : ENNReal) :

⌊r + 1⌋ₑ = ⌊r⌋ₑ + 1

source

@[simp]

theorem ENat.ceil_add_one (r : ENNReal) :

⌈r + 1⌉ₑ = ⌈r⌉ₑ + 1

source

@[simp]

theorem ENat.floor_add_ofNat (r : ENNReal) (n : ℕ) [n.AtLeastTwo] :

⌊r + OfNat.ofNat n⌋ₑ = ⌊r⌋ₑ + OfNat.ofNat n

source

@[simp]

theorem ENat.ceil_add_ofNat (r : ENNReal) (n : ℕ) [n.AtLeastTwo] :

⌈r + OfNat.ofNat n⌉ₑ = ⌈r⌉ₑ + OfNat.ofNat n

source

@[simp]

theorem ENat.floor_sub_toENNReal (r : ENNReal) (n : ℕ∞) :

⌊r - ↑n⌋ₑ = ⌊r⌋ₑ - n

source

@[simp]

theorem ENat.ceil_sub_toENNReal (r : ENNReal) (n : ℕ∞) :

⌈r - ↑n⌉ₑ = ⌈r⌉ₑ - n

source

@[simp]

theorem ENat.floor_sub_natCast (r : ENNReal) (n : ℕ) :

⌊r - ↑n⌋ₑ = ⌊r⌋ₑ - ↑n

source

@[simp]

theorem ENat.ceil_sub_natCast (r : ENNReal) (n : ℕ) :

⌈r - ↑n⌉ₑ = ⌈r⌉ₑ - ↑n

source

@[simp]

theorem ENat.floor_sub_one (r : ENNReal) :

⌊r - 1⌋ₑ = ⌊r⌋ₑ - 1

source

@[simp]

theorem ENat.ceil_sub_one (r : ENNReal) :

⌈r - 1⌉ₑ = ⌈r⌉ₑ - 1

source

@[simp]

theorem ENat.floor_sub_ofNat (r : ENNReal) (n : ℕ) [n.AtLeastTwo] :

⌊r - OfNat.ofNat n⌋ₑ = ⌊r⌋ₑ - OfNat.ofNat n

source

@[simp]

theorem ENat.ceil_sub_ofNat (r : ENNReal) (n : ℕ) [n.AtLeastTwo] :

⌈r - OfNat.ofNat n⌉ₑ = ⌈r⌉ₑ - OfNat.ofNat n

source

theorem ENat.ceil_lt_add_one {r : ENNReal} (hr : r ≠ ⊤) :

↑⌈r⌉ₑ < r + 1

source

theorem ENat.ceil_add_le (r s : ENNReal) :

⌈r + s⌉ₑ ≤ ⌈r⌉ₑ + ⌈s⌉ₑ

source

@[simp]

theorem ENat.toENNReal_iSup {ι : Sort u_1} (f : ι → ℕ∞) :

↑(⨆ (i : ι), f i) = ⨆ (i : ι), ↑(f i)

source

@[simp]

theorem ENat.toENNReal_iInf {ι : Sort u_1} (f : ι → ℕ∞) :

↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)

source

def Mathlib.Meta.Positivity.evalENatCeil :

PositivityExt

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

Equations

One or more equations did not get rendered due to their size.

Instances For

Documentation

Mathlib.Algebra.Order.Floor.Extended

Extended floor and ceil #

Main declarations #

Notation #

TODO #

Tags #