zpow_inj
theorem zpow_inj :
∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {a : α} {m n : ℤ}, 0 < a → a ≠ 1 → (a ^ m = a ^ n ↔ m = n) := by
sorry
This theorem states that for any linearly ordered semiring `α` and any two integers `m` and `n`, if `a` is a positive element of `α` which is not equal to 1, then `a` raised to the power of `m` is equal to `a` raised to the power of `n` if and only if `m` is equal to `n`. In mathematical terms, given $a \in \alpha$, $a > 0$, $a \neq 1$, and any two integers $m$ and $n$, it holds that $a^m = a^n$ if and only if $m = n$.
More concisely: For any linearly ordered semiring `α` and positive element `a ≠ 1` in `α`, the power `a^m` equals `a^n` if and only if integers `m` and `n` are equal.
|
zpow_le_of_le
theorem zpow_le_of_le :
∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {a : α} {m n : ℤ}, 1 ≤ a → m ≤ n → a ^ m ≤ a ^ n
This theorem states that for any type `α` that forms a linear ordered semifield, and for any element `a` of that type and any integers `m` and `n`, if `a` is greater than or equal to 1 and `m` is less than or equal to `n`, then `a` raised to the power of `m` is less than or equal to `a` raised to the power of `n`. Essentially, this theorem asserts the monotonicity of the exponentiation function in a linear ordered semifield when the base is greater than or equal to 1.
More concisely: For any linear ordered semifield type `α` and `a` in `α` greater than or equal to 1, if `m` is less than or equal to `n`, then `a^m ≤ a^n`.
|
zpow_strictMono
theorem zpow_strictMono :
∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {a : α}, 1 < a → StrictMono fun x => a ^ x
The theorem `zpow_strictMono` states that for any type `α` that has a structure of a linearly ordered semifield, and for any element `a` of `α` which is greater than 1, the function `f(x) = a^x` is strictly monotonic. That is, for any two elements `b` and `c` of `α` such that `b < c`, we will have `a^b < a^c`.
More concisely: For any linearly ordered semifield type `α` and element `a` greater than 1 in `α`, the function `x ↔ a^x` is strictly increasing.
|
zpow_bit0_nonneg
theorem zpow_bit0_nonneg : ∀ {α : Type u_1} [inst : LinearOrderedField α] (a : α) (n : ℤ), 0 ≤ a ^ bit0 n
The theorem `zpow_bit0_nonneg` states that for any linearly ordered field `α`, and for any elements `a` from `α` and `n` from integers `ℤ`, the result of raising `a` to the power of two times `n` (`a ^ (2n)`) is always non-negative (greater than or equal to zero). In simpler terms, it asserts that, in a linearly ordered field, the square of any integer power of any element is non-negative. Here `bit0 n` is a function that doubles the integer `n`, and `0 ≤ a ^ bit0 n` is the non-negativity claim.
More concisely: In a linearly ordered field, for all elements `a` and integers `n`, `a ^ (2n)` is non-negative.
|
Even.zpow_pos
theorem Even.zpow_pos :
∀ {α : Type u_1} [inst : LinearOrderedField α] {a : α} {n : ℤ}, Even n → n ≠ 0 → a ≠ 0 → 0 < a ^ n
This theorem states that for any type `α` that forms a linearly ordered field, given an element `a` of type `α` and an integer `n`, if `n` is an even number and both `n` and `a` are non-zero, then `a` raised to the power `n` is positive. In mathematical terms, given `α` as a linearly ordered field, `a ∈ α`, and `n ∈ ℤ` such that `n` is even and `n ≠ 0, a ≠ 0`, then `a^n > 0`.
More concisely: For any linearly ordered field `α`, if `a ∈ α` is non-zero and `n ∈ ℤ` is even and non-zero, then `a^n > 0`.
|
zpow_bit0_pos
theorem zpow_bit0_pos : ∀ {α : Type u_1} [inst : LinearOrderedField α] {a : α}, a ≠ 0 → ∀ (n : ℤ), 0 < a ^ bit0 n := by
sorry
This theorem, `zpow_bit0_pos`, states that for any type `α` that has a structure of a linearly ordered field, given any non-zero element `a` of `α` and any integer `n`, the value of `a` raised to the power of `bit0 n` (meaning `2n`, as `bit0` function doubles its input) is always positive. Essentially, it's stating that for non-zero values, raising them to an even power will always yield a positive result, which aligns with the mathematical fact that the square of any non-zero real number is always positive.
More concisely: For any non-zero element in a linearly ordered field, raising it to an even power results in a positive value.
|
Nat.cast_le_pow_div_sub
theorem Nat.cast_le_pow_div_sub :
∀ {α : Type u_1} [inst : LinearOrderedField α] {a : α}, 1 < a → ∀ (n : ℕ), ↑n ≤ a ^ n / (a - 1)
This theorem states that for any number `a` greater than 1 and any natural number `n`, the value of `n` is less than or equal to `a` raised to the power `n` divided by `(a - 1)`. This holds for all `a` in `α`, where `α` is an ordered field. There is also a stronger version of this inequality where `a^n - 1` is used in the numerator, as referenced in `Nat.cast_le_pow_sub_div_sub`.
More concisely: For any number `a` in an ordered field greater than 1 and any natural number `n`, `n` is less than or equal to `a^n / (a - 1)`.
|
zpow_bit1_neg_iff
theorem zpow_bit1_neg_iff : ∀ {α : Type u_1} [inst : LinearOrderedField α] {a : α} {n : ℤ}, a ^ bit1 n < 0 ↔ a < 0 := by
sorry
The theorem `zpow_bit1_neg_iff` states that for any linear ordered field `α` and elements `a` in `α` and integer `n`, `a` raised to the power `bit1 n` (where `bit1 n` is defined as `2n + 1`) is less than zero if and only if `a` is less than zero. Thus, this theorem gives a condition for a number raised to an odd power to be negative in a linear ordered field.
More concisely: For any linear ordered field `α` and element `a` in `α` and integer `n`, `a^(2n+1) < 0` if and only if `a < 0`.
|
Odd.zpow_nonpos
theorem Odd.zpow_nonpos : ∀ {α : Type u_1} [inst : LinearOrderedField α] {a : α} {n : ℤ}, Odd n → a ≤ 0 → a ^ n ≤ 0
The theorem `Odd.zpow_nonpos` states that for any type `α` that is a linear ordered field, given an `α` element `a` and an integer `n`, if `n` is odd and `a` is less than or equal to zero, then `a` to the power `n` is less than or equal to zero. In mathematical terms, if `n` is odd and `a ≤ 0`, then `a^n ≤ 0`.
More concisely: For any linear ordered field `α` and odd integer `n`, if `0 ≤ a` in `α`, then `0 ≤ a^n`.
|
Odd.zpow_neg
theorem Odd.zpow_neg : ∀ {α : Type u_1} [inst : LinearOrderedField α] {a : α} {n : ℤ}, Odd n → a < 0 → a ^ n < 0 := by
sorry
The theorem `Odd.zpow_neg` states that in any linearly ordered field, for any number `a` and any integer `n`, if `n` is odd and `a` is less than zero, then `a` raised to the power `n` will be less than zero. Here, a number is considered odd if it can be expressed as `2 * k + 1` for some integer `k`.
More concisely: In any linearly ordered field, if an element is less than zero and an integer `n` is odd, then `(a: num) ^ n < 0`.
|
Nat.cast_le_pow_sub_div_sub
theorem Nat.cast_le_pow_sub_div_sub :
∀ {α : Type u_1} [inst : LinearOrderedField α] {a : α}, 1 < a → ∀ (n : ℕ), ↑n ≤ (a ^ n - 1) / (a - 1)
This theorem, referred to as 'Nat.cast_le_pow_sub_div_sub', states that for any type `α` which forms a linear ordered field, and for any real number `a` greater than 1, for any natural number `n`, the value of `n` is less than or equal to `(a^n - 1) / (a - 1)`. In other words, for a given real number `a` and natural number `n`, the inequality `n ≤ (a^n - 1) / (a - 1)` holds. This is a reformulation of Bernoulli's inequality used to estimate the value of `n`.
More concisely: For any real number `a > 1` and natural number `n`, `n <= (a^n - 1) / (a - 1)`.
|
zpow_bit1_nonpos_iff
theorem zpow_bit1_nonpos_iff : ∀ {α : Type u_1} [inst : LinearOrderedField α] {a : α} {n : ℤ}, a ^ bit1 n ≤ 0 ↔ a ≤ 0
The theorem `zpow_bit1_nonpos_iff` states that for any type `α` which is an instance of `LinearOrderedField`, and for any elements `a` of type `α` and `n` of type `ℤ` (integer), `a` raised to the power `bit1 n` (which is `2*n + 1`) is less than or equal to zero if and only if `a` itself is less than or equal to zero.
More concisely: For any `α` an instance of `LinearOrderedField` and `a : α` and `n : ℤ`, `a^(2*n+1) ≤ 0` if and only if `a ≤ 0`.
|