mathlib3 documentation

algebra.order.field.power

Lemmas about powers in ordered fields. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Integer powers #

source
theorem zpow_le_of_le {α : Type u_1} [linear_ordered_semifield α] {a : α} {m n : ℤ} (ha : 1 ≤ a) (h : m ≤ n) :
a ^ m ≤ a ^ n
source
theorem zpow_le_one_of_nonpos {α : Type u_1} [linear_ordered_semifield α] {a : α} {n : ℤ} (ha : 1 ≤ a) (hn : n ≤ 0) :
a ^ n ≤ 1
source
theorem one_le_zpow_of_nonneg {α : Type u_1} [linear_ordered_semifield α] {a : α} {n : ℤ} (ha : 1 ≤ a) (hn : 0 ≤ n) :
1 ≤ a ^ n
source
@[protected]
theorem nat.zpow_pos_of_pos {α : Type u_1} [linear_ordered_semifield α] {a : ℕ} (h : 0 < a) (n : ℤ) :
0 < ↑a ^ n
source
theorem nat.zpow_ne_zero_of_pos {α : Type u_1} [linear_ordered_semifield α] {a : ℕ} (h : 0 < a) (n : ℤ) :
↑a ^ n ≠ 0
source
theorem one_lt_zpow {α : Type u_1} [linear_ordered_semifield α] {a : α} (ha : 1 < a) (n : ℤ) :
0 < n → 1 < a ^ n
source
theorem zpow_strict_mono {α : Type u_1} [linear_ordered_semifield α] {a : α} (hx : 1 < a) :
strict_mono (has_pow.pow a)
source
theorem zpow_strict_anti {α : Type u_1} [linear_ordered_semifield α] {a : α} (h₀ : 0 < a) (h₁ : a < 1) :
strict_anti (has_pow.pow a)
source
@[simp]
theorem zpow_lt_iff_lt {α : Type u_1} [linear_ordered_semifield α] {a : α} {m n : ℤ} (hx : 1 < a) :
a ^ m < a ^ n ↔ m < n
source
@[simp]
theorem zpow_le_iff_le {α : Type u_1} [linear_ordered_semifield α] {a : α} {m n : ℤ} (hx : 1 < a) :
a ^ m ≤ a ^ n ↔ m ≤ n
source
@[simp]
theorem div_pow_le {α : Type u_1} [linear_ordered_semifield α] {a b : α} (ha : 0 ≤ a) (hb : 1 ≤ b) (k : ℕ) :
a / b ^ k ≤ a
source
theorem zpow_injective {α : Type u_1} [linear_ordered_semifield α] {a : α} (h₀ : 0 < a) (h₁ : a ≠ 1) :
function.injective (has_pow.pow a)
source
@[simp]
theorem zpow_inj {α : Type u_1} [linear_ordered_semifield α] {a : α} {m n : ℤ} (h₀ : 0 < a) (h₁ : a ≠ 1) :
a ^ m = a ^ n ↔ m = n
source
theorem zpow_le_max_of_min_le {α : Type u_1} [linear_ordered_semifield α] {x : α} (hx : 1 ≤ x) {a b c : ℤ} (h : linear_order.min a b ≤ c) :
x ^ -c ≤ linear_order.max (x ^ -a) (x ^ -b)
source
theorem zpow_le_max_iff_min_le {α : Type u_1} [linear_ordered_semifield α] {x : α} (hx : 1 < x) {a b c : ℤ} :
x ^ -c ≤ linear_order.max (x ^ -a) (x ^ -b) ↔ linear_order.min a b ≤ c

Lemmas about powers to numerals. #

source
theorem zpow_bit0_nonneg {α : Type u_1} [linear_ordered_field α] (a : α) (n : ℤ) :
0 ≤ a ^ bit0 n
source
theorem zpow_two_nonneg {α : Type u_1} [linear_ordered_field α] (a : α) :
0 ≤ a ^ 2
source
theorem zpow_neg_two_nonneg {α : Type u_1} [linear_ordered_field α] (a : α) :
0 ≤ a ^ -2
source
theorem zpow_bit0_pos {α : Type u_1} [linear_ordered_field α] {a : α} (h : a ≠ 0) (n : ℤ) :
0 < a ^ bit0 n
source
theorem zpow_two_pos_of_ne_zero {α : Type u_1} [linear_ordered_field α] {a : α} (h : a ≠ 0) :
0 < a ^ 2
source
@[simp]
theorem zpow_bit0_pos_iff {α : Type u_1} [linear_ordered_field α] {a : α} {n : ℤ} (hn : n ≠ 0) :
0 < a ^ bit0 n ↔ a ≠ 0
source
@[simp]
theorem zpow_bit1_neg_iff {α : Type u_1} [linear_ordered_field α] {a : α} {n : ℤ} :
a ^ bit1 n < 0 ↔ a < 0
source
@[simp]
theorem zpow_bit1_nonneg_iff {α : Type u_1} [linear_ordered_field α] {a : α} {n : ℤ} :
0 ≤ a ^ bit1 n ↔ 0 ≤ a
source
@[simp]
theorem zpow_bit1_nonpos_iff {α : Type u_1} [linear_ordered_field α] {a : α} {n : ℤ} :
a ^ bit1 n ≤ 0 ↔ a ≤ 0
source
@[simp]
theorem zpow_bit1_pos_iff {α : Type u_1} [linear_ordered_field α] {a : α} {n : ℤ} :
0 < a ^ bit1 n ↔ 0 < a
source
@[protected]
theorem even.zpow_nonneg {α : Type u_1} [linear_ordered_field α] {n : ℤ} (hn : even n) (a : α) :
0 ≤ a ^ n
source
theorem even.zpow_pos_iff {α : Type u_1} [linear_ordered_field α] {a : α} {n : ℤ} (hn : even n) (h : n ≠ 0) :
0 < a ^ n ↔ a ≠ 0
source
theorem odd.zpow_neg_iff {α : Type u_1} [linear_ordered_field α] {a : α} {n : ℤ} (hn : odd n) :
a ^ n < 0 ↔ a < 0
source
@[protected]
theorem odd.zpow_nonneg_iff {α : Type u_1} [linear_ordered_field α] {a : α} {n : ℤ} (hn : odd n) :
0 ≤ a ^ n ↔ 0 ≤ a
source
theorem odd.zpow_nonpos_iff {α : Type u_1} [linear_ordered_field α] {a : α} {n : ℤ} (hn : odd n) :
a ^ n ≤ 0 ↔ a ≤ 0
source
theorem odd.zpow_pos_iff {α : Type u_1} [linear_ordered_field α] {a : α} {n : ℤ} (hn : odd n) :
0 < a ^ n ↔ 0 < a
source
theorem even.zpow_pos {α : Type u_1} [linear_ordered_field α] {a : α} {n : ℤ} (hn : even n) (h : n ≠ 0) :
a ≠ 0 → 0 < a ^ n

Alias of the reverse direction of even.zpow_pos_iff.

source
theorem odd.zpow_neg {α : Type u_1} [linear_ordered_field α] {a : α} {n : ℤ} (hn : odd n) :
a < 0 → a ^ n < 0

Alias of the reverse direction of odd.zpow_neg_iff.

source
theorem odd.zpow_nonpos {α : Type u_1} [linear_ordered_field α] {a : α} {n : ℤ} (hn : odd n) :
a ≤ 0 → a ^ n ≤ 0

Alias of the reverse direction of odd.zpow_nonpos_iff.

source
theorem even.zpow_abs {α : Type u_1} [linear_ordered_field α] {p : ℤ} (hp : even p) (a : α) :
|a| ^ p = a ^ p
source
@[simp]
theorem zpow_bit0_abs {α : Type u_1} [linear_ordered_field α] (a : α) (p : ℤ) :
|a| ^ bit0 p = a ^ bit0 p

Miscellaneous lemmmas #

source
theorem nat.cast_le_pow_sub_div_sub {α : Type u_1} [linear_ordered_field α] {a : α} (H : 1 < a) (n : ℕ) :
↑n ≤ (a ^ n - 1) / (a - 1)

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

source
theorem nat.cast_le_pow_div_sub {α : Type u_1} [linear_ordered_field α] {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.