mathlib documentation

algebra.order.to_interval_mod

Reducing to an interval modulo its length #

This file defines operations that reduce a number (in an archimedean linear_ordered_add_comm_group) to a number in a given interval, modulo the length of that interval.

Main definitions #

source
noncomputable def to_Ico_div {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
ℤ

The unique integer such that this multiple of b, added to x, is in Ico a (a + b).

Equations
source
theorem add_to_Ico_div_zsmul_mem_Ico {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
x + to_Ico_div a hb x • b ∈ set.Ico a (a + b)
source
theorem eq_to_Ico_div_of_add_zsmul_mem_Ico {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {a b x : α} (hb : 0 < b) {y : ℤ} (hy : x + y • b ∈ set.Ico a (a + b)) :
y = to_Ico_div a hb x
source
noncomputable def to_Ioc_div {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
ℤ

The unique integer such that this multiple of b, added to x, is in Ioc a (a + b).

Equations
source
theorem add_to_Ioc_div_zsmul_mem_Ioc {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
x + to_Ioc_div a hb x • b ∈ set.Ioc a (a + b)
source
theorem eq_to_Ioc_div_of_add_zsmul_mem_Ioc {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {a b x : α} (hb : 0 < b) {y : ℤ} (hy : x + y • b ∈ set.Ioc a (a + b)) :
y = to_Ioc_div a hb x
source
noncomputable def to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
α

Reduce x to the interval Ico a (a + b).

Equations
source
noncomputable def to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
α

Reduce x to the interval Ioc a (a + b).

Equations
source
theorem to_Ico_mod_mem_Ico {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb x ∈ set.Ico a (a + b)
source
theorem to_Ioc_mod_mem_Ioc {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb x ∈ set.Ioc a (a + b)
source
theorem left_le_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
a ≤ to_Ico_mod a hb x
source
theorem left_lt_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
a < to_Ioc_mod a hb x
source
theorem to_Ico_mod_lt_right {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb x < a + b
source
theorem to_Ioc_mod_le_right {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb x ≤ a + b
source
@[simp]
theorem self_add_to_Ico_div_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
x + to_Ico_div a hb x • b = to_Ico_mod a hb x
source
@[simp]
theorem self_add_to_Ioc_div_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
x + to_Ioc_div a hb x • b = to_Ioc_mod a hb x
source
@[simp]
theorem to_Ico_div_zsmul_add_self {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_div a hb x • b + x = to_Ico_mod a hb x
source
@[simp]
theorem to_Ioc_div_zsmul_add_self {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_div a hb x • b + x = to_Ioc_mod a hb x
source
@[simp]
theorem to_Ico_mod_sub_self {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb x - x = to_Ico_div a hb x • b
source
@[simp]
theorem to_Ioc_mod_sub_self {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb x - x = to_Ioc_div a hb x • b
source
@[simp]
theorem self_sub_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
x - to_Ico_mod a hb x = -to_Ico_div a hb x • b
source
@[simp]
theorem self_sub_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
x - to_Ioc_mod a hb x = -to_Ioc_div a hb x • b
source
@[simp]
theorem to_Ico_mod_sub_to_Ico_div_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb x - to_Ico_div a hb x • b = x
source
@[simp]
theorem to_Ioc_mod_sub_to_Ioc_div_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb x - to_Ioc_div a hb x • b = x
source
@[simp]
theorem to_Ico_div_zsmul_sub_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_div a hb x • b - to_Ico_mod a hb x = -x
source
@[simp]
theorem to_Ioc_div_zsmul_sub_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_div a hb x • b - to_Ioc_mod a hb x = -x
source
theorem to_Ico_mod_eq_iff {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {a b x y : α} (hb : 0 < b) :
to_Ico_mod a hb x = y ↔ a ≤ y ∧ y < a + b ∧ ∃ (z : ℤ), y - x = z • b
source
theorem to_Ioc_mod_eq_iff {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {a b x y : α} (hb : 0 < b) :
to_Ioc_mod a hb x = y ↔ a < y ∧ y ≤ a + b ∧ ∃ (z : ℤ), y - x = z • b
source
@[simp]
theorem to_Ico_div_apply_left {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ico_div a hb a = 0
source
@[simp]
theorem to_Ioc_div_apply_left {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ioc_div a hb a = 1
source
@[simp]
theorem to_Ico_mod_apply_left {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ico_mod a hb a = a
source
@[simp]
theorem to_Ioc_mod_apply_left {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ioc_mod a hb a = a + b
source
theorem to_Ico_div_apply_right {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ico_div a hb (a + b) = -1
source
theorem to_Ioc_div_apply_right {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ioc_div a hb (a + b) = 0
source
theorem to_Ico_mod_apply_right {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ico_mod a hb (a + b) = a
source
theorem to_Ioc_mod_apply_right {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) :
to_Ioc_mod a hb (a + b) = a + b
source
@[simp]
theorem to_Ico_div_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ℤ) :
to_Ico_div a hb (x + m • b) = to_Ico_div a hb x - m
source
@[simp]
theorem to_Ioc_div_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ℤ) :
to_Ioc_div a hb (x + m • b) = to_Ioc_div a hb x - m
source
@[simp]
theorem to_Ico_div_zsmul_add {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ℤ) :
to_Ico_div a hb (m • b + x) = to_Ico_div a hb x - m
source
@[simp]
theorem to_Ioc_div_zsmul_add {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ℤ) :
to_Ioc_div a hb (m • b + x) = to_Ioc_div a hb x - m
source
@[simp]
theorem to_Ico_div_sub_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ℤ) :
to_Ico_div a hb (x - m • b) = to_Ico_div a hb x + m
source
@[simp]
theorem to_Ioc_div_sub_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ℤ) :
to_Ioc_div a hb (x - m • b) = to_Ioc_div a hb x + m
source
@[simp]
theorem to_Ico_div_add_right {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_div a hb (x + b) = to_Ico_div a hb x - 1
source
@[simp]
theorem to_Ioc_div_add_right {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_div a hb (x + b) = to_Ioc_div a hb x - 1
source
@[simp]
theorem to_Ico_div_add_left {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_div a hb (b + x) = to_Ico_div a hb x - 1
source
@[simp]
theorem to_Ioc_div_add_left {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_div a hb (b + x) = to_Ioc_div a hb x - 1
source
@[simp]
theorem to_Ico_div_sub {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_div a hb (x - b) = to_Ico_div a hb x + 1
source
@[simp]
theorem to_Ioc_div_sub {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_div a hb (x - b) = to_Ioc_div a hb x + 1
source
@[simp]
theorem to_Ico_mod_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ℤ) :
to_Ico_mod a hb (x + m • b) = to_Ico_mod a hb x
source
@[simp]
theorem to_Ioc_mod_add_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ℤ) :
to_Ioc_mod a hb (x + m • b) = to_Ioc_mod a hb x
source
@[simp]
theorem to_Ico_mod_zsmul_add {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ℤ) :
to_Ico_mod a hb (m • b + x) = to_Ico_mod a hb x
source
@[simp]
theorem to_Ioc_mod_zsmul_add {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ℤ) :
to_Ioc_mod a hb (m • b + x) = to_Ioc_mod a hb x
source
@[simp]
theorem to_Ico_mod_sub_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ℤ) :
to_Ico_mod a hb (x - m • b) = to_Ico_mod a hb x
source
@[simp]
theorem to_Ioc_mod_sub_zsmul {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) (m : ℤ) :
to_Ioc_mod a hb (x - m • b) = to_Ioc_mod a hb x
source
@[simp]
theorem to_Ico_mod_add_right {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb (x + b) = to_Ico_mod a hb x
source
@[simp]
theorem to_Ioc_mod_add_right {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb (x + b) = to_Ioc_mod a hb x
source
@[simp]
theorem to_Ico_mod_add_left {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb (b + x) = to_Ico_mod a hb x
source
@[simp]
theorem to_Ioc_mod_add_left {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb (b + x) = to_Ioc_mod a hb x
source
@[simp]
theorem to_Ico_mod_sub {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb (x - b) = to_Ico_mod a hb x
source
@[simp]
theorem to_Ioc_mod_sub {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb (x - b) = to_Ioc_mod a hb x
source
theorem to_Ico_mod_eq_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b x y : α} (hb : 0 < b) :
to_Ico_mod a hb x = to_Ico_mod a hb y ↔ ∃ (z : ℤ), y - x = z • b
source
theorem to_Ioc_mod_eq_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b x y : α} (hb : 0 < b) :
to_Ioc_mod a hb x = to_Ioc_mod a hb y ↔ ∃ (z : ℤ), y - x = z • b
source
theorem to_Ico_mod_eq_self {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {a b x : α} (hb : 0 < b) :
to_Ico_mod a hb x = x ↔ a ≤ x ∧ x < a + b
source
theorem to_Ioc_mod_eq_self {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {a b x : α} (hb : 0 < b) :
to_Ioc_mod a hb x = x ↔ a < x ∧ x ≤ a + b
source
@[simp]
theorem to_Ico_mod_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a₁ a₂ : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a₁ hb (to_Ico_mod a₂ hb x) = to_Ico_mod a₁ hb x
source
@[simp]
theorem to_Ico_mod_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a₁ a₂ : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a₁ hb (to_Ioc_mod a₂ hb x) = to_Ico_mod a₁ hb x
source
@[simp]
theorem to_Ioc_mod_to_Ioc_mod {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a₁ a₂ : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a₁ hb (to_Ioc_mod a₂ hb x) = to_Ioc_mod a₁ hb x
source
@[simp]
theorem to_Ioc_mod_to_Ico_mod {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a₁ a₂ : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a₁ hb (to_Ico_mod a₂ hb x) = to_Ioc_mod a₁ hb x
source
theorem to_Ico_mod_periodic {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) :
function.periodic (to_Ico_mod a hb) b
source
theorem to_Ioc_mod_periodic {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) :
function.periodic (to_Ioc_mod a hb) b
source
theorem to_Ico_div_eq_neg_floor {α : Type u_1} [linear_ordered_field α] [floor_ring α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_div a hb x = -⌊(x - a) / b⌋
source
theorem to_Ioc_div_eq_floor {α : Type u_1} [linear_ordered_field α] [floor_ring α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_div a hb x = ⌊(a + b - x) / b⌋
source
theorem to_Ico_div_zero_one {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : α) :
to_Ico_div 0 zero_lt_one x = -⌊x⌋
source
theorem to_Ico_mod_eq_add_fract_mul {α : Type u_1} [linear_ordered_field α] [floor_ring α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ico_mod a hb x = a + int.fract ((x - a) / b) * b
source
theorem to_Ioc_mod_eq_sub_fract_mul {α : Type u_1} [linear_ordered_field α] [floor_ring α] (a : α) {b : α} (hb : 0 < b) (x : α) :
to_Ioc_mod a hb x = a + b - int.fract ((a + b - x) / b) * b
source
theorem to_Ico_mod_zero_one {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : α) :
to_Ico_mod 0 zero_lt_one x = int.fract x