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 #

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
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)
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
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
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)
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
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
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
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)
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)
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
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
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
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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
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
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
@[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
@[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
@[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
@[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
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
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
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
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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
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
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
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
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
@[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
@[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
@[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
@[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
theorem to_Ico_mod_periodic {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) :
theorem to_Ioc_mod_periodic {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] (a : α) {b : α} (hb : 0 < b) :
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
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
theorem to_Ico_div_zero_one {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : α) :
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
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
theorem to_Ico_mod_zero_one {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : α) :