mathlib documentation

algebra.group_power.order

Lemmas about the interaction of power operations with order #

Note that some lemmas are in algebra/group_power/lemmas.lean as they import files which depend on this file.

theorem nsmul_nonneg {A : Type u_1} [ordered_add_comm_monoid A] {a : A} (H : 0 a) (n : ) :
0 n a
theorem nsmul_pos {A : Type u_1} [ordered_add_comm_monoid A] {a : A} (ha : 0 < a) {k : } (hk : 0 < k) :
0 < k a
theorem nsmul_le_nsmul {A : Type u_1} [ordered_add_comm_monoid A] {a : A} {n m : } (ha : 0 a) (h : n m) :
n a m a
theorem nsmul_le_nsmul_of_le_right {A : Type u_1} [ordered_add_comm_monoid A] {a b : A} (hab : a b) (i : ) :
i a i b
theorem gsmul_nonneg {A : Type u_1} [ordered_add_comm_group A] {a : A} (H : 0 a) {n : } (hn : 0 n) :
0 n a
theorem nsmul_lt_nsmul {A : Type u_1} [ordered_cancel_add_comm_monoid A] {a : A} {n m : } (ha : 0 < a) (h : n < m) :
n a < m a
theorem canonically_ordered_semiring.pow_pos {R : Type u_2} [canonically_ordered_comm_semiring R] {a : R} (H : 0 < a) (n : ) :
0 < a ^ n
theorem canonically_ordered_semiring.pow_le_pow_of_le_left {R : Type u_2} [canonically_ordered_comm_semiring R] {a b : R} (hab : a b) (i : ) :
a ^ i b ^ i
theorem canonically_ordered_semiring.one_le_pow_of_one_le {R : Type u_2} [canonically_ordered_comm_semiring R] {a : R} (H : 1 a) (n : ) :
1 a ^ n
theorem canonically_ordered_semiring.pow_le_one {R : Type u_2} [canonically_ordered_comm_semiring R] {a : R} (H : a 1) (n : ) :
a ^ n 1
@[simp]
theorem pow_pos {R : Type u_2} [ordered_semiring R] {a : R} (H : 0 < a) (n : ) :
0 < a ^ n
@[simp]
theorem pow_nonneg {R : Type u_2} [ordered_semiring R] {a : R} (H : 0 a) (n : ) :
0 a ^ n
theorem pow_add_pow_le {R : Type u_2} [ordered_semiring R] {x y : R} {n : } (hx : 0 x) (hy : 0 y) (hn : n 0) :
x ^ n + y ^ n (x + y) ^ n
theorem pow_lt_pow_of_lt_left {R : Type u_2} [ordered_semiring R] {x y : R} {n : } (Hxy : x < y) (Hxpos : 0 x) (Hnpos : 0 < n) :
x ^ n < y ^ n
theorem strict_mono_incr_on_pow {R : Type u_2} [ordered_semiring R] {n : } (hn : 0 < n) :
strict_mono_incr_on (λ (x : R), x ^ n) (set.Ici 0)
theorem one_le_pow_of_one_le {R : Type u_2} [ordered_semiring R] {a : R} (H : 1 a) (n : ) :
1 a ^ n
theorem pow_mono {R : Type u_2} [ordered_semiring R] {a : R} (h : 1 a) :
monotone (λ (n : ), a ^ n)
theorem pow_le_pow {R : Type u_2} [ordered_semiring R] {a : R} {n m : } (ha : 1 a) (h : n m) :
a ^ n a ^ m
theorem strict_mono_pow {R : Type u_2} [ordered_semiring R] {a : R} (h : 1 < a) :
strict_mono (λ (n : ), a ^ n)
theorem pow_lt_pow {R : Type u_2} [ordered_semiring R] {a : R} {n m : } (h : 1 < a) (h2 : n < m) :
a ^ n < a ^ m
theorem pow_lt_pow_iff {R : Type u_2} [ordered_semiring R] {a : R} {n m : } (h : 1 < a) :
a ^ n < a ^ m n < m
theorem pow_le_pow_of_le_left {R : Type u_2} [ordered_semiring R] {a b : R} (ha : 0 a) (hab : a b) (i : ) :
a ^ i b ^ i
theorem pow_left_inj {R : Type u_2} [linear_ordered_semiring R] {x y : R} {n : } (Hxpos : 0 x) (Hypos : 0 y) (Hnpos : 0 < n) (Hxyn : x ^ n = y ^ n) :
x = y
theorem lt_of_pow_lt_pow {R : Type u_2} [linear_ordered_semiring R] {a b : R} (n : ) (hb : 0 b) (h : a ^ n < b ^ n) :
a < b
theorem le_of_pow_le_pow {R : Type u_2} [linear_ordered_semiring R] {a b : R} (n : ) (hb : 0 b) (hn : 0 < n) (h : a ^ n b ^ n) :
a b
theorem pow_abs {R : Type u_2} [linear_ordered_ring R] (a : R) (n : ) :
abs a ^ n = abs (a ^ n)
theorem abs_neg_one_pow {R : Type u_2} [linear_ordered_ring R] (n : ) :
abs ((-1) ^ n) = 1
theorem pow_bit0_nonneg {R : Type u_2} [linear_ordered_ring R] (a : R) (n : ) :
0 a ^ bit0 n
theorem sq_nonneg {R : Type u_2} [linear_ordered_ring R] (a : R) :
0 a ^ 2
theorem pow_two_nonneg {R : Type u_2} [linear_ordered_ring R] (a : R) :
0 a ^ 2

Alias of sq_nonneg.

theorem pow_bit0_pos {R : Type u_2} [linear_ordered_ring R] {a : R} (h : a 0) (n : ) :
0 < a ^ bit0 n
theorem sq_pos_of_ne_zero {R : Type u_2} [linear_ordered_ring R] (a : R) (h : a 0) :
0 < a ^ 2
theorem pow_two_pos_of_ne_zero {R : Type u_2} [linear_ordered_ring R] (a : R) (h : a 0) :
0 < a ^ 2

Alias of sq_pos_of_ne_zero.

theorem sq_abs {R : Type u_2} [linear_ordered_ring R] (x : R) :
abs x ^ 2 = x ^ 2
theorem abs_sq {R : Type u_2} [linear_ordered_ring R] (x : R) :
abs (x ^ 2) = x ^ 2
theorem sq_lt_sq {R : Type u_2} [linear_ordered_ring R] {x y : R} (h : abs x < y) :
x ^ 2 < y ^ 2
theorem sq_lt_sq' {R : Type u_2} [linear_ordered_ring R] {x y : R} (h1 : -y < x) (h2 : x < y) :
x ^ 2 < y ^ 2
theorem sq_le_sq {R : Type u_2} [linear_ordered_ring R] {x y : R} (h : abs x abs y) :
x ^ 2 y ^ 2
theorem sq_le_sq' {R : Type u_2} [linear_ordered_ring R] {x y : R} (h1 : -y x) (h2 : x y) :
x ^ 2 y ^ 2
theorem abs_lt_abs_of_sq_lt_sq {R : Type u_2} [linear_ordered_ring R] {x y : R} (h : x ^ 2 < y ^ 2) :
abs x < abs y
theorem abs_lt_of_sq_lt_sq {R : Type u_2} [linear_ordered_ring R] {x y : R} (h : x ^ 2 < y ^ 2) (hy : 0 y) :
abs x < y
theorem abs_lt_of_sq_lt_sq' {R : Type u_2} [linear_ordered_ring R] {x y : R} (h : x ^ 2 < y ^ 2) (hy : 0 y) :
-y < x x < y
theorem abs_le_abs_of_sq_le_sq {R : Type u_2} [linear_ordered_ring R] {x y : R} (h : x ^ 2 y ^ 2) :
abs x abs y
theorem abs_le_of_sq_le_sq {R : Type u_2} [linear_ordered_ring R] {x y : R} (h : x ^ 2 y ^ 2) (hy : 0 y) :
abs x y
theorem abs_le_of_sq_le_sq' {R : Type u_2} [linear_ordered_ring R] {x y : R} (h : x ^ 2 y ^ 2) (hy : 0 y) :
-y x x y
@[simp]
theorem eq_of_sq_eq_sq {R : Type u_2} [linear_ordered_comm_ring R] {a b : R} (ha : 0 a) (hb : 0 b) :
a ^ 2 = b ^ 2 a = b
theorem two_mul_le_add_sq {R : Type u_2} [linear_ordered_comm_ring R] (a b : R) :
(2 * a) * b a ^ 2 + b ^ 2

Arithmetic mean-geometric mean (AM-GM) inequality for linearly ordered commutative rings.

theorem two_mul_le_add_pow_two {R : Type u_2} [linear_ordered_comm_ring R] (a b : R) :
(2 * a) * b a ^ 2 + b ^ 2

Alias of two_mul_le_add_sq.