Lemmas about powers in ordered fields.

Integer powers

@[deprecated zpow_le_zpow_right₀ (since := "2024-10-08")]

theorem zpow_le_of_le {α : Type u_1} [LinearOrderedSemifield α] {a : α} {m n : ℤ} (ha : 1 ≤ a) (h : m ≤ n) : a ^ m ≤ a ^ n

@[deprecated zpow_le_one_of_nonpos₀ (since := "2024-10-08")]

theorem zpow_le_one_of_nonpos {α : Type u_1} [LinearOrderedSemifield α] {a : α} {n : ℤ} (ha : 1 ≤ a) (hn : n ≤ 0) : a ^ n ≤ 1

@[deprecated one_le_zpow₀ (since := "2024-10-08")]

theorem one_le_zpow_of_nonneg {α : Type u_1} [LinearOrderedSemifield α] {a : α} {n : ℤ} (ha : 1 ≤ a) (hn : 0 ≤ n) : 1 ≤ a ^ n

@[deprecated zpow_pos (since := "2024-10-08")]

theorem Nat.zpow_pos_of_pos {α : Type u_1} [LinearOrderedSemifield α] {a : ℕ} (h : 0 < a) (n : ℤ) : 0 < ↑a ^ n

@[deprecated zpow_ne_zero (since := "2024-10-08")]

theorem Nat.zpow_ne_zero_of_pos {α : Type u_1} [LinearOrderedSemifield α] {a : ℕ} (h : 0 < a) (n : ℤ) : ↑a ^ n ≠ 0

@[deprecated zpow_right_strictMono₀ (since := "2024-10-08")]

theorem zpow_strictMono {α : Type u_1} [LinearOrderedSemifield α] {a : α} (hx : 1 < a) : StrictMono fun (x : ℤ) => a ^ x

@[deprecated zpow_right_strictAnti₀ (since := "2024-10-08")]

theorem zpow_strictAnti {α : Type u_1} [LinearOrderedSemifield α] {a : α} (h₀ : 0 < a) (h₁ : a < 1) : StrictAnti fun (x : ℤ) => a ^ x

@[deprecated zpow_lt_zpow_iff_right₀ (since := "2024-10-08")]

theorem zpow_lt_iff_lt {α : Type u_1} [LinearOrderedSemifield α] {a : α} {m n : ℤ} (hx : 1 < a) : a ^ m < a ^ n ↔ m < n

@[deprecated zpow_le_zpow_iff_right₀ (since := "2024-10-08")]

theorem zpow_le_iff_le {α : Type u_1} [LinearOrderedSemifield α] {a : α} {m n : ℤ} (hx : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n

@[deprecated div_le_self (since := "2024-10-08")]

theorem div_pow_le {α : Type u_1} [LinearOrderedSemifield α] {a b : α} (ha : 0 ≤ a) (hb : 1 ≤ b) (k : ℕ) : a / b ^ k ≤ a

@[deprecated zpow_right_injective₀ (since := "2024-10-08")]

theorem zpow_injective {α : Type u_1} [LinearOrderedSemifield α] {a : α} (h₀ : 0 < a) (h₁ : a ≠ 1) : Function.Injective fun (x : ℤ) => a ^ x

@[deprecated zpow_right_inj₀ (since := "2024-10-08")]

theorem zpow_inj {α : Type u_1} [LinearOrderedSemifield α] {a : α} {m n : ℤ} (h₀ : 0 < a) (h₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n

@[deprecated "No deprecation message was provided." (since := "2024-10-08")]

theorem zpow_le_max_of_min_le {α : Type u_1} [LinearOrderedSemifield α] {x : α} (hx : 1 ≤ x) {a b c : ℤ} (h : a ⊓ b ≤ c) : x ^ (-c) ≤ x ^ (-a) ⊔ x ^ (-b)

@[deprecated "No deprecation message was provided." (since := "2024-10-08")]

theorem zpow_le_max_iff_min_le {α : Type u_1} [LinearOrderedSemifield α] {x : α} (hx : 1 < x) {a b c : ℤ} : x ^ (-c) ≤ x ^ (-a) ⊔ x ^ (-b) ↔ 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 < 0 → a ^ 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 ≤ 0 → a ^ 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

theorem zpow_eq_zpow_iff_of_ne_zero₀ {α : Type u_1} [LinearOrderedField α] {a b : α} {n : ℤ} (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b ∨ a = -b ∧ Even n

theorem zpow_eq_zpow_iff_cases₀ {α : Type u_1} [LinearOrderedField α] {a b : α} {n : ℤ} : a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

theorem zpow_eq_one_iff_of_ne_zero₀ {α : Type u_1} [LinearOrderedField α] {a : α} {n : ℤ} (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n

theorem zpow_eq_one_iff_cases₀ {α : Type u_1} [LinearOrderedField α] {a : α} {n : ℤ} : a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n

theorem zpow_eq_neg_zpow_iff₀ {α : Type u_1} [LinearOrderedField α] {a b : α} {n : ℤ} (hb : b ≠ 0) : a ^ n = -b ^ n ↔ a = -b ∧ Odd n

theorem zpow_eq_neg_one_iff₀ {α : Type u_1} [LinearOrderedField α] {a : α} {n : ℤ} : a ^ n = -1 ↔ a = -1 ∧ Odd n

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.

def Mathlib.Meta.Positivity.evalZPow : PositivityExt

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.