Documentation

Mathlib.Algebra.Order.Field.Power

Lemmas about powers in ordered fields. #

Integer powers #

theorem zpow_le_of_le {α : Type u_1} [LinearOrderedSemifield α] {a : α} {m : } {n : } (ha : 1 a) (h : m n) :
a ^ m a ^ n
theorem zpow_le_one_of_nonpos {α : Type u_1} [LinearOrderedSemifield α] {a : α} {n : } (ha : 1 a) (hn : n 0) :
a ^ n 1
theorem one_le_zpow_of_nonneg {α : Type u_1} [LinearOrderedSemifield α] {a : α} {n : } (ha : 1 a) (hn : 0 n) :
1 a ^ n
theorem Nat.zpow_pos_of_pos {α : Type u_1} [LinearOrderedSemifield α] {a : } (h : 0 < a) (n : ) :
0 < a ^ n
theorem Nat.zpow_ne_zero_of_pos {α : Type u_1} [LinearOrderedSemifield α] {a : } (h : 0 < a) (n : ) :
a ^ n 0
theorem one_lt_zpow {α : Type u_1} [LinearOrderedSemifield α] {a : α} (ha : 1 < a) (n : ) :
0 < n1 < a ^ n
theorem zpow_strictMono {α : Type u_1} [LinearOrderedSemifield α] {a : α} (hx : 1 < a) :
StrictMono fun (x : ) => a ^ x
theorem zpow_strictAnti {α : Type u_1} [LinearOrderedSemifield α] {a : α} (h₀ : 0 < a) (h₁ : a < 1) :
StrictAnti fun (x : ) => a ^ x
@[simp]
theorem zpow_lt_iff_lt {α : Type u_1} [LinearOrderedSemifield α] {a : α} {m : } {n : } (hx : 1 < a) :
a ^ m < a ^ n m < n
theorem GCongr.zpow_lt_of_lt {α : Type u_1} [LinearOrderedSemifield α] {a : α} {m : } {n : } (hx : 1 < a) :
m < na ^ m < a ^ n

Alias of the reverse direction of zpow_lt_iff_lt.

@[deprecated GCongr.zpow_lt_of_lt]
theorem zpow_lt_of_lt {α : Type u_1} [LinearOrderedSemifield α] {a : α} {m : } {n : } (hx : 1 < a) :
m < na ^ m < a ^ n

Alias of the reverse direction of zpow_lt_iff_lt.


Alias of the reverse direction of zpow_lt_iff_lt.

@[simp]
theorem zpow_le_iff_le {α : Type u_1} [LinearOrderedSemifield α] {a : α} {m : } {n : } (hx : 1 < a) :
a ^ m a ^ n m n
@[simp]
theorem div_pow_le {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 a) (hb : 1 b) (k : ) :
a / b ^ k a
theorem zpow_injective {α : Type u_1} [LinearOrderedSemifield α] {a : α} (h₀ : 0 < a) (h₁ : a 1) :
Function.Injective fun (x : ) => a ^ x
@[simp]
theorem zpow_inj {α : Type u_1} [LinearOrderedSemifield α] {a : α} {m : } {n : } (h₀ : 0 < a) (h₁ : a 1) :
a ^ m = a ^ n m = n
theorem zpow_le_max_of_min_le {α : Type u_1} [LinearOrderedSemifield α] {x : α} (hx : 1 x) {a : } {b : } {c : } (h : min a b c) :
x ^ (-c) max (x ^ (-a)) (x ^ (-b))
theorem zpow_le_max_iff_min_le {α : Type u_1} [LinearOrderedSemifield α] {x : α} (hx : 1 < x) {a : } {b : } {c : } :
x ^ (-c) max (x ^ (-a)) (x ^ (-b)) min a b c
theorem Even.zpow_nonneg {α : Type u_1} [LinearOrderedField α] {n : } (hn : Even n) (a : α) :
0 a ^ n
theorem zpow_two_nonneg {α : Type u_1} [LinearOrderedField α] (a : α) :
0 a ^ 2
theorem zpow_neg_two_nonneg {α : Type u_1} [LinearOrderedField α] (a : α) :
0 a ^ (-2)
theorem Even.zpow_pos {α : Type u_1} [LinearOrderedField α] {a : α} {n : } (hn : Even n) (ha : a 0) :
0 < a ^ n
theorem zpow_two_pos_of_ne_zero {α : Type u_1} [LinearOrderedField α] {a : α} (ha : a 0) :
0 < a ^ 2
theorem Even.zpow_pos_iff {α : Type u_1} [LinearOrderedField α] {a : α} {n : } (hn : Even n) (h : n 0) :
0 < a ^ n a 0
theorem Odd.zpow_neg_iff {α : Type u_1} [LinearOrderedField α] {a : α} {n : } (hn : Odd n) :
a ^ n < 0 a < 0
theorem Odd.zpow_nonneg_iff {α : Type u_1} [LinearOrderedField α] {a : α} {n : } (hn : Odd n) :
0 a ^ n 0 a
theorem Odd.zpow_nonpos_iff {α : Type u_1} [LinearOrderedField α] {a : α} {n : } (hn : Odd n) :
a ^ n 0 a 0
theorem Odd.zpow_pos_iff {α : Type u_1} [LinearOrderedField α] {a : α} {n : } (hn : Odd n) :
0 < a ^ n 0 < a
theorem Odd.zpow_neg {α : Type u_1} [LinearOrderedField α] {a : α} {n : } (hn : Odd n) :
a < 0a ^ n < 0

Alias of the reverse direction of Odd.zpow_neg_iff.

theorem Odd.zpow_nonpos {α : Type u_1} [LinearOrderedField α] {a : α} {n : } (hn : Odd n) :
a 0a ^ n 0

Alias of the reverse direction of Odd.zpow_nonpos_iff.

theorem Even.zpow_abs {α : Type u_1} [LinearOrderedField α] {p : } (hp : Even p) (a : α) :
|a| ^ p = a ^ p

Bernoulli's inequality #

theorem Nat.cast_le_pow_sub_div_sub {α : Type u_1} [LinearOrderedField α] {a : α} (H : 1 < a) (n : ) :
n (a ^ n - 1) / (a - 1)

Bernoulli's inequality reformulated to estimate (n : α).

theorem Nat.cast_le_pow_div_sub {α : Type u_1} [LinearOrderedField α] {a : α} (H : 1 < a) (n : ) :
n a ^ n / (a - 1)

For any a > 1 and a natural n we have n ≤ a ^ n / (a - 1). See also Nat.cast_le_pow_sub_div_sub for a stronger inequality with a ^ n - 1 in the numerator.

The positivity extension which identifies expressions of the form a ^ (b : ℤ), such that positivity successfully recognises both a and b.

Equations
  • One or more equations did not get rendered due to their size.
Instances For