pow_lt_pow_of_lt_one
theorem pow_lt_pow_of_lt_one :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R} {n m : ℕ}, 0 < a → a < 1 → m < n → a ^ n < a ^ m := by
sorry
This theorem, `pow_lt_pow_of_lt_one`, states that for any strictly ordered semiring `R` and any element `a` of `R`, if `0 < a < 1` and `n` and `m` are natural numbers where `m < n`, then `a^n` is strictly less than `a^m`. In other words, within a strictly ordered semiring, the power function for a number between 0 and 1 is strictly decreasing as the exponent increases.
More concisely: If `0 < a < 1` in a strictly ordered semiring `R` and `n > m` are natural numbers, then `a^n < a^m`.
|
zsmul_strictMono_right
theorem zsmul_strictMono_right :
∀ (α : Type u_1) [inst : OrderedAddCommGroup α] {n : ℤ}, 0 < n → StrictMono fun x => n • x
The theorem `zsmul_strictMono_right` states that for any type `α` that is an ordered additive commutative group, and for any integer `n` greater than zero, the function that scales elements of `α` by `n` is strictly monotonic. In other words, if `a` and `b` are elements of `α` and `a < b`, then `n` times `a` is less than `n` times `b`.
More concisely: For any ordered additive commutative group type `α` and integer `n` > 0, the multiplication by `n` function on `α` is strictly monotonic. That is, if `a < b` in `α`, then `n*a < n*b`.
|
pow_two_pos_of_ne_zero
theorem pow_two_pos_of_ne_zero :
∀ {R : Type u_4} [inst : LinearOrderedSemiring R] [inst_1 : ExistsAddOfLE R] {a : R}, a ≠ 0 → 0 < a ^ 2
This theorem, `pow_two_pos_of_ne_zero`, states that for any non-zero element `a` from a linear ordered semiring `R`, where addition operation exists for elements less than or equal to each other, the square of `a` (denoted as `a ^ 2`) is always positive. This is essentially asserting that the square of any non-zero real number is always greater than zero.
More concisely: For any non-zero element in a linear ordered semiring with squaring operation, the square is positive.
|
self_le_pow
theorem self_le_pow : ∀ {R : Type u_3} [inst : OrderedSemiring R] {a : R} {m : ℕ}, 1 ≤ a → m ≠ 0 → a ≤ a ^ m
This theorem, `self_le_pow`, states that for any type `R` that is an ordered semiring and any element `a` of `R` that is at least 1, along with a natural number `m` which is not zero, `a` is less than or equal to `a` raised to the power of `m`. In mathematical terms, for all `a ≥ 1` and `m ≠ 0`, we have `a ≤ a^m`.
More concisely: For any ordered semiring `R` and `a` in `R` with `a > 0`, `a` is less than or equal to `a^(m: nat)` for all natural numbers `m` not equal to zero.
|
pow_lt_pow_iff_right
theorem pow_lt_pow_iff_right :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R} {n m : ℕ}, 1 < a → (a ^ n < a ^ m ↔ n < m)
This theorem states that for any type `R` which is a Strict Ordered Semiring, given natural numbers `n` and `m` and an element `a` of `R` such that `a` is greater than 1, `a` raised to the power `n` is less than `a` raised to the power `m` if and only if `n` is less than `m`. In other words, in a Strict Ordered Semiring, for a number `a` greater than 1, a lower exponent results in a smaller result when used as a power of `a`.
More concisely: For any strict ordered semiring R and natural numbers n, m, and element a > 1 in R, a^n < a^m if and only if n < m.
|
Nat.pow_le_iff_le_left
theorem Nat.pow_le_iff_le_left : ∀ {a b n : ℕ}, n ≠ 0 → (a ^ n ≤ b ^ n ↔ a ≤ b)
This theorem, `Nat.pow_le_iff_le_left`, is an alias of `Nat.pow_le_pow_iff_left`. It states that for any natural numbers `a`, `b`, and `n`, given that `n` is not zero, the inequality `a ^ n ≤ b ^ n` holds if and only if `a ≤ b`. In other words, for any non-zero natural number `n`, `a` to the power of `n` is less than or equal to `b` to the power of `n` precisely when `a` is less than or equal to `b`.
More concisely: For any natural numbers $a, b$, and $n$ with $n \neq 0$, $a^n \leq b^n$ if and only if $a \leq b$.
|
strictMonoOn_pow
theorem strictMonoOn_pow :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {n : ℕ}, n ≠ 0 → StrictMonoOn (fun x => x ^ n) {a | 0 ≤ a} := by
sorry
The theorem `strictMonoOn_pow` states that for any strictly ordered semiring `R` and any natural number `n` which is not equal to zero, the function `x ↦ x^n` is strictly monotone on the set of all `a` such that `a` is greater than or equal to zero. In other words, for any pair of numbers `a` and `b` in this set, if `a` is less than `b`, then `a^n` is less than `b^n`. This theorem is an alias of `pow_left_strictMonoOn`; see also `pow_left_strictMono` and `Nat.pow_left_strictMono` for related results.
More concisely: For any strictly ordered semiring R and natural number n > 0, the function x ^ n is strictly increasing on the non-negative part of R.
|
pow_right_strictAnti
theorem pow_right_strictAnti :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R}, 0 < a → a < 1 → StrictAnti fun x => a ^ x
The theorem `pow_right_strictAnti` states that for any strict ordered semiring `R` and for any element `a` of `R`, if `a` is positive and less than 1, then the function `f(x) = a^x` is strictly antitone. In other words, if `a` and `b` are elements of `R` such that `a < b`, then `f(b) < f(a)`.
More concisely: For any strict ordered semiring `R` and strict positive element `a` in `R` less than 1, the function `f(x) = a^x` is strictly antitone, i.e., `a^b < a^a` for all `b` in `R` with `b > a`.
|
zpow_eq_zpow_iff'
theorem zpow_eq_zpow_iff' :
∀ {α : Type u_1} [inst : LinearOrderedCommGroup α] {n : ℤ} {a b : α}, n ≠ 0 → (a ^ n = b ^ n ↔ a = b)
This theorem, `zpow_eq_zpow_iff'`, states that for any type `α` which forms a linearly ordered commutative group, given any two elements `a` and `b` of `α` and an integer `n` that is not zero, `a` raised to the power `n` is equal to `b` raised to the power `n` if and only if `a` is equal to `b`. This is essentially a formalization of the property from elementary algebra that if the n-th powers of two numbers are equal (with n not being zero), then the numbers themselves must be equal.
More concisely: For any commutative group with identity `α` and integers `n ≠ 0`, `a^n = b^n` if and only if `a = b`.
|
sq_eq_sq
theorem sq_eq_sq :
∀ {R : Type u_3} [inst : LinearOrderedSemiring R] {a b : R}, 0 ≤ a → 0 ≤ b → (a ^ 2 = b ^ 2 ↔ a = b)
This theorem, `sq_eq_sq`, states that for any type `R` that has the structure of a linear ordered semiring, given any two non-negative elements `a` and `b` from `R`, `a` squared is equal to `b` squared if and only if `a` is equal to `b`. It essentially states that in a linear ordered semiring, squaring is an injective operation for non-negative numbers.
More concisely: In a linear ordered semiring, for all non-negative elements `a` and `b`, `a^2 = b^2` if and only if `a = b`.
|
pow_lt_pow
theorem pow_lt_pow :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R} {n m : ℕ}, 1 < a → m < n → a ^ m < a ^ n
This theorem, `pow_lt_pow`, is an alias of `pow_lt_pow_right`. It states that for any strictly ordered semiring `R` and any element `a` in `R` and two natural numbers `m` and `n`, if `a` is greater than 1 and `m` is less than `n`, then `a` to the power of `m` is less than `a` to the power of `n`. In other words, in a strictly ordered semiring, increasing the exponent of a number greater than 1 results in a larger value.
More concisely: For any strictly ordered semiring `R` and elements `a` in `R` with `a > 1` and natural numbers `m < n`, `a^m < a^n`.
|
pow_le_pow_left
theorem pow_le_pow_left :
∀ {R : Type u_3} [inst : OrderedSemiring R] {a b : R}, 0 ≤ a → a ≤ b → ∀ (n : ℕ), a ^ n ≤ b ^ n
This theorem states that for any type `R` that is an ordered semiring, given any two elements `a` and `b` of `R` such that `a` is non-negative and less than or equal to `b`, the power of `a` raised to any natural number `n` will always be less than or equal to the power of `b` raised to the same `n`. In LaTeX notation, this can be expressed as: for all $a, b \in R$ and $n \in \mathbb{N}$, if $0 \leq a \leq b$, then $a^n \leq b^n$.
More concisely: For any ordered semiring `R` and natural number `n`, if `a` is a non-negative element of `R` less than or equal to `b`, then `a^n` is less than or equal to `b^n`.
|
le_self_pow
theorem le_self_pow : ∀ {R : Type u_3} [inst : OrderedSemiring R] {a : R} {m : ℕ}, 1 ≤ a → m ≠ 0 → a ≤ a ^ m
This theorem states that for any ordered semiring 'R' and any element 'a' of 'R' along with a nonzero natural number 'm', if 'a' is greater than or equal to 1, then 'a' is less than or equal to 'a' raised to the power 'm'. This essentially asserts that any number greater than or equal to 1 is always less than or equal to its power, provided the exponent is a nonzero natural number.
More concisely: For any ordered semiring 'R' and element 'a' of 'R' with 'a' >= 1 and 'm' a nonzero natural number, 'a' <= 'a'^'m'.
|
Nat.pow_left_strictMono
theorem Nat.pow_left_strictMono : ∀ {n : ℕ}, n ≠ 0 → StrictMono fun x => x ^ n
The theorem `Nat.pow_left_strictMono` states that for any natural number `n` that is not equal to zero, the function that maps `x` to `x` raised to the power of `n` is strictly monotone. In other words, if we have two natural numbers, `a` and `b`, and `a` is less than `b`, then `a` raised to the power of `n` is less than `b` raised to the power of `n`. This theorem is also related to `pow_left_strictMonoOn`.
More concisely: For any natural number `n` where `n > 0`, the power function `x => x ^ n` is strictly increasing on the natural numbers.
|
pow_lt_pow_left
theorem pow_lt_pow_left :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {x y : R}, x < y → 0 ≤ x → ∀ {n : ℕ}, n ≠ 0 → x ^ n < y ^ n := by
sorry
The theorem `pow_lt_pow_left` states that for any strict ordered semiring `R` and any two elements `x` and `y` from `R`, if `x` is less than `y` and `x` is non-negative, then for any non-zero natural number `n`, the `n`th power of `x` is less than the `n`th power of `y`. In other words, in a strict ordered semiring, raising a smaller non-negative number and a larger number to the same positive power preserves the inequality.
More concisely: If `0 < x <= y` in a strict ordered semiring `R` and `n` is a non-zero natural number, then `x^n < y^n`.
|
pow_eq_one_iff_of_nonneg
theorem pow_eq_one_iff_of_nonneg :
∀ {R : Type u_3} [inst : LinearOrderedSemiring R] {a : R} {n : ℕ}, 0 ≤ a → n ≠ 0 → (a ^ n = 1 ↔ a = 1)
This theorem, `pow_eq_one_iff_of_nonneg`, states that for any type `R` that is a Linear Ordered Semiring and any non-negative real number `a` and a non-zero natural number `n` in `R`, `a` raised to the power `n` equals 1 if and only if `a` itself equals 1. Essentially, for a non-negative number `a` and a non-zero exponent `n`, `a^n` is 1 only when `a` is 1.
More concisely: For any non-negative element `a` in a Linear Ordered Semiring `R` and non-zero natural number `n`, `a^n = 1` if and only if `a = 1`.
|
pow_lt_pow_iff_of_lt_one
theorem pow_lt_pow_iff_of_lt_one :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R} {n m : ℕ}, 0 < a → a < 1 → (a ^ m < a ^ n ↔ n < m) := by
sorry
This theorem, `pow_lt_pow_iff_of_lt_one`, states that for any strictly ordered semiring `R` and any element `a` in `R`, if `a` is greater than zero and less than one, then `a` to the power of `m` is less than `a` to the power of `n` if and only if `n` is less than `m`. Essentially, it is stating that for numbers between 0 and 1, raising them to a higher power makes them smaller.
More concisely: For any strictly ordered semiring R and elements a in R with 0 < a < 1, the inequality a^m < a^n holds if and only if m > n.
|
lt_of_pow_lt_pow_left
theorem lt_of_pow_lt_pow_left :
∀ {R : Type u_3} [inst : LinearOrderedSemiring R] {a b : R} (n : ℕ), 0 ≤ b → a ^ n < b ^ n → a < b
This theorem states that for any linearly ordered semiring `R` and any two elements `a` and `b` of `R`, if `b` is nonnegative and `a` raised to the power of `n` is less than `b` raised to the power of `n`, then `a` must be less than `b`. Essentially, in a number system that behaves like the real numbers, if the `n`th power of `a` is less than the `n`th power of `b` (with `b` being nonnegative), then `a` is less than `b`.
More concisely: If `R` is a linearly ordered semiring, `a`, `b` are in `R` with `b` nonnegative, and `a^n < b^n`, then `a < b`.
|
le_of_pow_le_pow_left
theorem le_of_pow_le_pow_left :
∀ {R : Type u_3} [inst : LinearOrderedSemiring R] {a b : R} {n : ℕ}, n ≠ 0 → 0 ≤ b → a ^ n ≤ b ^ n → a ≤ b := by
sorry
This theorem states that for any linearly ordered semiring `R`, given any two elements `a` and `b` from `R`, and a natural number `n` which is not zero, if `b` is non-negative and `a` to the power of `n` is less than or equal to `b` to the power of `n`, then `a` is less than or equal to `b`. In mathematical terms, this could be written as: for all $a, b \in R$ and $n \in \mathbb{N}$, if $n \neq 0$, $b \geq 0$ and $a^n \leq b^n$, then $a \leq b$.
More concisely: If in a linearly ordered semiring, an element raised to a non-zero natural power is less than or equal to another element raised to the same power, then the first element is less than or equal to the second.
|
pow_right_mono
theorem pow_right_mono : ∀ {R : Type u_3} [inst : OrderedSemiring R] {a : R}, 1 ≤ a → Monotone fun x => a ^ x := by
sorry
The theorem `pow_right_mono` states that for all types `R`, where `R` is associated with an ordered semiring structure, and for any element `a` of type `R`, if `a` is greater than or equal to `1`, then the function that raises `a` to the power of any given number `x` is monotone. In mathematical terms, this means that for such `a` and any two numbers `x` and `y`, if `x ≤ y`, then `a^x ≤ a^y`.
More concisely: For any ordered semiring `R` and `a` in `R` with `a ≥ 1`, the function `x => a^x` is monotone on `R`.
|
pow_le_pow_of_le_left
theorem pow_le_pow_of_le_left :
∀ {R : Type u_3} [inst : OrderedSemiring R] {a b : R}, 0 ≤ a → a ≤ b → ∀ (n : ℕ), a ^ n ≤ b ^ n
This theorem, `pow_le_pow_of_le_left`, states that for any type `R` that is an ordered semiring, given two elements `a` and `b` in `R` such that `a` is non-negative and less than or equal to `b`, then for any natural number `n`, `a` to the power `n` will always be less than or equal to `b` to the power `n`. In mathematical terms, for $a, b \in R$ with $0 \leq a \leq b$ and any natural number $n$, we have $a^n \leq b^n$. This theorem is an alias (alternative name) for the theorem `pow_le_pow_left`.
More concisely: For any ordered semiring `R`, non-negative element `a` less than or equal to `b` in `R`, and natural number `n`, we have `a^n <= b^n`.
|
strictAnti_pow
theorem strictAnti_pow :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R}, 0 < a → a < 1 → StrictAnti fun x => a ^ x
The theorem `strictAnti_pow` states that for any strictly ordered semiring `R` and any element `a` of `R`, if `a` is greater than zero and less than one, then the function `x` mapped to `a` to the power `x` is strictly antitone. In other words, for any two elements `b` and `c` from `R`, if `b` is less than `c`, then `a` to the power `c` is less than `a` to the power `b`.
More concisely: For any strictly ordered semiring `R` and element `a` in `R` with `0 < a < 1`, the function `x => a ^ x` is strictly antitone.
|
pow_bit0_nonneg
theorem pow_bit0_nonneg : ∀ {R : Type u_3} [inst : LinearOrderedRing R] (a : R) (n : ℕ), 0 ≤ a ^ bit0 n
This theorem, `pow_bit0_nonneg`, states that for any linearly ordered ring `R` and any element `a` of `R`, the power of `a` raised to the `bit0` of any natural number `n` is always non-negative (`0 ≤ a ^ bit0 n`). In simpler terms, it's saying that for any real number `a` and natural number `n`, `a` to the power of twice `n` (since `bit0 n = n + n`) is always greater than or equal to zero.
More concisely: For any linearly ordered ring R and its element a, 0 ≤ a ^ bit0 n. (Or, equivalently, a ^ (2 * n) ≥ 0 for any natural number n.)
|
Nat.pow_le_iff_le_right
theorem Nat.pow_le_iff_le_right :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R} {n m : ℕ}, 1 < a → (a ^ n ≤ a ^ m ↔ n ≤ m)
This theorem, `Nat.pow_le_iff_le_right`, establishes a relationship between powers and ordering in a strict ordered semiring. Specifically, for any strict ordered semiring `R`, any element `a` of `R`, and any natural numbers `n` and `m`, if `a` is greater than 1, then `a` to the power of `n` is less than or equal to `a` to the power of `m` if and only if `n` is less than or equal to `m`.
More concisely: For any strict ordered semiring R and elements a of R with a > 1, the relation a^n <= a^m holds if and only if natural number n is less than or equal to m.
|
one_lt_pow
theorem one_lt_pow : ∀ {R : Type u_3} [inst : OrderedSemiring R] {a : R}, 1 < a → ∀ {n : ℕ}, n ≠ 0 → 1 < a ^ n := by
sorry
This theorem states that for any type `R` that is an ordered semiring, and for any element `a` of type `R`, if `a` is greater than 1, then `a` raised to the power of any non-zero natural number `n` is also greater than 1. In mathematical terms, this theorem can be written as: For all `a` in 'R' and 'n' in natural numbers, if 'a' > 1 and 'n' ≠ 0, then 'a^n' > 1.
More concisely: For any ordered semiring R and its element a > 1, the power a^n with a non-zero natural number n also holds the property a^n > 1.
|
one_le_pow_of_one_le
theorem one_le_pow_of_one_le : ∀ {R : Type u_3} [inst : OrderedSemiring R] {a : R}, 1 ≤ a → ∀ (n : ℕ), 1 ≤ a ^ n := by
sorry
This theorem states that for any ordered semiring `R` and any element `a` of `R`, if `a` is greater than or equal to 1 (`1 ≤ a`), then any natural number power of `a` (`a ^ n` for any `n` in the set of natural numbers, `ℕ`) is also greater than or equal to 1 (`1 ≤ a ^ n`). In other words, if a number is greater than or equal to 1, raising it to any natural number power will not make it less than 1 in an ordered semiring.
More concisely: For any ordered semiring `R` and its element `a` greater than or equal to 1, the natural power `a ^ n` is also greater than or equal to 1 for all `n` in the natural numbers.
|
pow_le_pow_right
theorem pow_le_pow_right :
∀ {R : Type u_3} [inst : OrderedSemiring R] {a : R} {n m : ℕ}, 1 ≤ a → n ≤ m → a ^ n ≤ a ^ m
This theorem states that for any type `R` that has an ordered semiring structure, given a value of `a` from `R` and two natural numbers `n` and `m`, if `a` is greater than or equal to 1 and `n` is less than or equal to `m`, then `a` to the power `n` is less than or equal to `a` to the power `m`. In other words, for non-negative real numbers, increasing the exponent while keeping the base fixed (which is at least 1) will increase or keep the same the overall value.
More concisely: For any ordered semiring `R` and natural numbers `n ≤ m` with base `a` (where `a > 0`), `a^n ≤ a^m`.
|
Nat.pow_lt_iff_lt_right
theorem Nat.pow_lt_iff_lt_right :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R} {n m : ℕ}, 1 < a → (a ^ n < a ^ m ↔ n < m)
This theorem, named `Nat.pow_lt_iff_lt_right`, is an alias of `pow_lt_pow_iff_right`. It states that for any strictly ordered semiring `R`, a positive element `a` of `R`, and two natural numbers `n` and `m`, if `a` is greater than 1, then `a` to the power of `n` is less than `a` to the power of `m` if and only if `n` is less than `m`. In mathematical terms, given $a > 1$, $a^n < a^m$ is equivalent to $n < m$.
More concisely: For any strictly ordered semiring with a positive element `a`, and natural numbers `n` and `m` where `a` is greater than 1, `a^n` is less than `a^m` if and only if `n` is less than `m`.
|
pow_le_pow
theorem pow_le_pow : ∀ {R : Type u_3} [inst : OrderedSemiring R] {a : R} {n m : ℕ}, 1 ≤ a → n ≤ m → a ^ n ≤ a ^ m := by
sorry
This is an alias for the `pow_le_pow_right` theorem in Lean. It states that for any type `R` which is an ordered semiring, any element `a` of `R` and any two natural numbers `n` and `m`, if `a` is greater than or equal to 1 and `n` is less than or equal to `m`, then `a` to the power of `n` is less than or equal to `a` to the power of `m`. This is a property of exponents in ordered semirings.
More concisely: For any ordered semiring `R` and elements `a` in `R` with `a >= 1` and natural numbers `n` and `m` with `n <= m`, we have `a^n <= a^m`.
|
Nat.pow_lt_pow_of_lt_left
theorem Nat.pow_lt_pow_of_lt_left : ∀ {a b : ℕ}, a < b → ∀ {n : ℕ}, n ≠ 0 → a ^ n < b ^ n
This theorem, `Nat.pow_lt_pow_of_lt_left`, is an alias of `Nat.pow_lt_pow_left`. It states that for any two natural numbers 'a' and 'b', if 'a' is less than 'b', then for any other natural number 'n' that is not zero, 'a' to the power of 'n' is less than 'b' to the power of 'n'.
In mathematical terms, this can be expressed as: ∀ a, b ∈ ℕ, if a < b and ∀ n ∈ ℕ, n ≠ 0, then a^n < b^n.
More concisely: For all natural numbers a and b, if a is less than b, then a raised to any non-zero natural power is less than b raised to that same power.
|
pow_lt_pow_of_lt_left
theorem pow_lt_pow_of_lt_left :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {x y : R}, x < y → 0 ≤ x → ∀ {n : ℕ}, n ≠ 0 → x ^ n < y ^ n := by
sorry
This theorem, named `pow_lt_pow_of_lt_left`, states that for any strictly ordered semiring `R` and for any two elements `x` and `y` from `R`, if `x` is strictly less than `y` and `x` is non-negative, then for any natural number `n` that is not zero, `x` raised to the power `n` is strictly less than `y` raised to the power `n`. Basically, in a certain type of number system, if you have a positive number less than another and raise them to the same non-zero natural number exponent, the inequality remains.
More concisely: If `0 < x < y` in a strictly ordered semiring `R` and `n` is a non-zero natural number, then `x^n < y^n`.
|
pow_bit0_pos
theorem pow_bit0_pos : ∀ {R : Type u_3} [inst : LinearOrderedRing R] {a : R}, a ≠ 0 → ∀ (n : ℕ), 0 < a ^ bit0 n := by
sorry
This theorem, `pow_bit0_pos`, states that for any type `R` which is a linearly ordered ring, and for any nonzero element `a` of `R`, for any natural number `n`, the nth power of `a` using the `bit0` function (which essentially doubles the input) is always positive. In mathematical terms, given a ≠ 0, it asserts that 0 < a^(2n) for all natural numbers n.
More concisely: For any nonzero element `a` in a linearly ordered ring `R`, `a` raised to the power of any natural number `n` results in a positive element, i.e., `0 < a^(2n)`.
|
pow_mono
theorem pow_mono : ∀ {R : Type u_3} [inst : OrderedSemiring R] {a : R}, 1 ≤ a → Monotone fun x => a ^ x
The theorem `pow_mono` states that for any ordered semiring `R` and any element `a` in `R`, if `a` is greater than or equal to 1, then the function `fun x => a ^ x` is monotone. In other words, for any numbers `x` and `y` in `R` such that `x ≤ y`, it holds that `a ^ x ≤ a ^ y`. This theorem is an alias of the `pow_right_mono` theorem.
More concisely: For any ordered semiring `R` and `a` in `R` with `a >= 1`, the function `x => a ^ x` is monotone, i.e., `a ^ x <= a ^ y` for all `x <= y` in `R`.
|
pow_le_pow_iff_right
theorem pow_le_pow_iff_right :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R} {n m : ℕ}, 1 < a → (a ^ n ≤ a ^ m ↔ n ≤ m)
This theorem states that for any strictly ordered semiring `R`, given any element `a` from `R` and two natural numbers `n` and `m`, if `a` is greater than 1, then `a` raised to the power of `n` is less than or equal to `a` raised to the power of `m` if and only if `n` is less than or equal to `m`. In mathematical notation, if `a > 1` in `R`, then `a^n ≤ a^m` is equivalent to `n ≤ m`.
More concisely: For any strictly ordered semiring `R` and elements `a` in `R` with `a > 1`, `a^n ≤ a^m` holds if and only if `n ≤ m`.
|
zsmul_strictMono_left
theorem zsmul_strictMono_left :
∀ {α : Type u_1} [inst : OrderedAddCommGroup α] {a : α}, 0 < a → StrictMono fun n => n • a
This theorem states that for any type `α` that forms an ordered additively commutative group, and a positive element `a` of this type, the function that maps any integer `n` to the result of "scaling" `a` by `n` (denoted as `n • a`) is strictly monotone. In mathematical terms, this means that for any two integers `n` and `m` with `n < m`, we have `n • a < m • a` whenever `a` is a positive element of an ordered additively commutative group.
More concisely: For any positive element `a` in an ordered additively commutative group `α`, the function `n => n • a` is strictly increasing.
|
zsmul_eq_zsmul_iff'
theorem zsmul_eq_zsmul_iff' :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {n : ℤ} {a b : α}, n ≠ 0 → (n • a = n • b ↔ a = b)
This theorem, `zsmul_eq_zsmul_iff'`, states that for any type `α` which is a linearly ordered additive commutative group, and for any integers `n` and elements `a`, `b` of type `α`, if `n` is not zero, then the statement "`n` times `a` equals `n` times `b`" is equivalent to the statement "`a` equals `b`". In mathematical terms, if `n ≠ 0`, then `n*a = n*b` if and only if `a = b`, where `•` denotes the multiplication operation in the group, and `a` and `b` are elements of the group.
More concisely: For any linearly ordered additive commutative group type `α` and non-zero integer `n`, the elements `a` and `b` of `α` satisfy `n * a = n * b` if and only if `a = b`.
|
zsmul_right_injective
theorem zsmul_right_injective :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {n : ℤ}, n ≠ 0 → Function.Injective fun x => n • x
This theorem, `zsmul_right_injective`, states that for any type `α` which is a Linear Ordered Additive Commutative Group, and for any integer `n` that is not zero, the function that scales every element `x` of `α` by `n` (written as `n • x`) is injective. In other words, if `n • x = n • y` then `x = y` for all `x, y` in `α`. This property is sometimes referred to as "right-injectivity of scalar multiplication". Note that the theorem would not hold if `n` was equal to zero, as all elements would be scaled to zero, violating the injectivity condition.
More concisely: For any non-zero integer `n` and Linear Ordered Additive Commutative Group `α`, the function `x ↔ n • x` is an injection.
|
self_lt_pow
theorem self_lt_pow : ∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R} {m : ℕ}, 1 < a → 1 < m → a < a ^ m := by
sorry
This theorem, `self_lt_pow`, states that for any strictly ordered semiring `R` and any element `a` of that semiring, if `a` is greater than 1 and `m` is a natural number greater than 1, then `a` is less than `a` raised to the power `m`. In other words, in a strictly ordered semiring, any number larger than 1 is always less than its power when the exponent is a natural number greater than 1.
More concisely: For any strictly ordered semiring `R` and `a` in `R` with `a > 1` and `m` a natural number `> 1`, `a` is strictly less than `a^m`.
|
sq_pos_of_ne_zero
theorem sq_pos_of_ne_zero :
∀ {R : Type u_4} [inst : LinearOrderedSemiring R] [inst_1 : ExistsAddOfLE R] {a : R}, a ≠ 0 → 0 < a ^ 2
This theorem, `sq_pos_of_ne_zero`, states that for any type `R` that is a linearly ordered ring (as specified by the type class `LinearOrderedRing R`), if an element `a` of `R` is not zero, then the square of `a` (denoted as `a ^ 2`) is always greater than zero. In other words, squaring any non-zero element in a linearly ordered ring gives a positive result.
More concisely: For any linearly ordered ring `R` and non-zero element `a` in `R`, `a^2` is positive.
|
lt_of_pow_lt_pow
theorem lt_of_pow_lt_pow :
∀ {R : Type u_3} [inst : LinearOrderedSemiring R] {a b : R} (n : ℕ), 0 ≤ b → a ^ n < b ^ n → a < b
This theorem, `lt_of_pow_lt_pow`, is essentially an alias of `lt_of_pow_lt_pow_left`. It states that for any type `R` that is a linear ordered semiring, given any two elements `a` and `b` of `R` and a natural number `n`, if `b` is not negative and `a` raised to the power of `n` is less than `b` raised to the power of `n`, then `a` must be less than `b`.
More concisely: For any linear ordered semiring `R` and natural number `n`, if `a` is an element of `R`, `0 ≤ n`, `b` is an element of `R` with `a^n < b^n`, then `a < b`.
|
zpow_right_strictMono
theorem zpow_right_strictMono :
∀ {α : Type u_1} [inst : OrderedCommGroup α] {a : α}, 1 < a → StrictMono fun n => a ^ n
The theorem `zpow_right_strictMono` states that for any ordered commutative group `α` and any element `a` of `α`, if `a` is greater than 1, then the function mapping any integer `n` to `a` raised to the power of `n` is strictly monotonic. In other words, if `a` is greater than 1 and `n < m` for any integers `n` and `m`, then `a^n` is less than `a^m`.
More concisely: For any ordered commutative group `α` and `a` in `α` with `a > 1`, the function `n => a ^ n` is strictly increasing on integers `n`.
|
pow_bit1_nonpos_iff
theorem pow_bit1_nonpos_iff : ∀ {R : Type u_3} [inst : LinearOrderedRing R] {a : R} {n : ℕ}, a ^ bit1 n ≤ 0 ↔ a ≤ 0
This theorem, `pow_bit1_nonpos_iff`, states for any linearly ordered ring `R` and any elements `a` from `R` and `n` from the natural numbers, that `a` raised to the power of `bit1 n` (which is `2n+1`) is less than or equal to zero if and only if `a` is less than or equal to zero. This theorem provides an equivalence relation between the non-positivity of an odd-powered element in a ring and the non-positivity of the element itself.
More concisely: For any element `a` in a linearly ordered ring `R` and natural number `n`, `a` raised to the power of `2n+1` is non-positive if and only if `a` is non-positive.
|
pow_lt_pow_iff
theorem pow_lt_pow_iff :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R} {n m : ℕ}, 1 < a → (a ^ n < a ^ m ↔ n < m)
This theorem, called `pow_lt_pow_iff`, states that for any strict ordered semiring `R` and any element `a` of `R`, along with two natural numbers `n` and `m`, if `a` is greater than 1, then `a` to the power of `n` is less than `a` to the power of `m` if and only if `n` is less than `m`. In other words, in a strict ordered semiring, for a number greater than 1, the order of exponents corresponds to the order of their results when used as exponents of that number.
More concisely: For any strict ordered semiring `R` and `a` in `R` with `a > 1`, `a^n < a^m` if and only if `n < m`.
|
pow_le_pow_iff
theorem pow_le_pow_iff :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R} {n m : ℕ}, 1 < a → (a ^ n ≤ a ^ m ↔ n ≤ m)
This theorem, `pow_le_pow_iff`, is an alias for `pow_le_pow_iff_right`. It states that for any type `R` that is a strict ordered semiring and any `a` in `R`, with natural numbers `n` and `m`, if `a` is greater than 1, then `a` to the power `n` is less than or equal to `a` to the power `m` if and only if `n` is less than or equal to `m`. This theorem provides a way to compare the powers of a number in a strict ordered semiring.
More concisely: For any strict ordered semiring R and elements a in R with a > 1, the inequality a^n <= a^m holds if and only if the natural number n is less than or equal to m.
|
pow_right_strictMono
theorem pow_right_strictMono :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R}, 1 < a → StrictMono fun x => a ^ x
The theorem `pow_right_strictMono` states that for any type `R` that is a strict ordered semiring, and for any element `a` of `R` such that `1 < a`, the function `x ↦ a ^ x` is strictly monotone. In other words, if `1 < a` in a strictly ordered semiring, then raising `a` to any power preserves the order: if `x < y` then `a ^ x < a ^ y`.
More concisely: For any strict ordered semiring `R` and `1 < a` in `R`, the function `x ↦ a ^ x` is strictly increasing.
|
zpow_strictMono_left
theorem zpow_strictMono_left :
∀ (α : Type u_1) [inst : OrderedCommGroup α] {n : ℤ}, 0 < n → StrictMono fun x => x ^ n
The theorem `zpow_strictMono_left` states that for any type `α` that forms an ordered commutative group, for any integer `n` that is greater than zero, the function that maps `x` to `x ^ n` (i.e., `x` raised to the power `n`) is strictly monotone. This means that if `a` and `b` are any two elements of `α` such that `a < b`, then `a^n < b^n`.
More concisely: For any ordered commutative group type `α` and positive integer `n`, the power function `x ↔ x ^ n` is strict monotone, i.e., `x < y` implies `x ^ n < y ^ n`.
|
pow_lt_pow_right
theorem pow_lt_pow_right :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R} {n m : ℕ}, 1 < a → m < n → a ^ m < a ^ n
This theorem states that for any strictly ordered semi-ring `R` of a certain type `u_3`, and for any element `a` from `R`, along with two natural numbers `n` and `m`, if `a` is greater than 1 and `m` is less than `n`, then `a` raised to the power of `m` is less than `a` raised to the power of `n`. In other words, if we have a number greater than 1 and two different natural number exponents, with one smaller than the other, the smaller exponent will result in a smaller result when both are raised to the base number.
More concisely: For any strictly ordered semiring `R` and `a` in `R` with `a > 1`, `m < n` implies `a^m < a^n`.
|
pow_left_inj
theorem pow_left_inj :
∀ {R : Type u_3} [inst : LinearOrderedSemiring R] {a b : R} {n : ℕ},
0 ≤ a → 0 ≤ b → n ≠ 0 → (a ^ n = b ^ n ↔ a = b)
This theorem, `pow_left_inj`, asserts that for any type `R` that is a `LinearOrderedSemiring`, and for any two elements `a` and `b` of `R` along with a natural number `n`, if `a` and `b` are both non-negative and `n` is not zero, then `a` to the power of `n` being equal to `b` to the power of `n` is equivalent to `a` being equal to `b`. Essentially, it formalizes the notion that, under these conditions, the n-th power function is injective.
More concisely: For any non-zero natural number `n` and elements `a` and `b` in a LinearOrderedSemiring `R` with `a`, `b` non-negative, `a^n = b^n` if and only if `a = b`.
|
Nat.pow_right_strictMono
theorem Nat.pow_right_strictMono :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R}, 1 < a → StrictMono fun x => a ^ x
The theorem `Nat.pow_right_strictMono` states that for any strictly ordered semiring `R` and any element `a` of `R` that is greater than 1, the function `x => a ^ x` is strictly monotone. In other words, if `a` is a number greater than 1 in a strictly ordered semiring, then raising `a` to higher powers results in strictly increasing values.
The theorem also serves as an alias for `pow_right_strictMono` and is related to `pow_right_strictMono'`.
More concisely: For any strictly ordered semiring `R` and `a` in `R` with `a > 1`, the function `x => a ^ x` is strictly increasing.
|
pow_le_pow_iff_left
theorem pow_le_pow_iff_left :
∀ {R : Type u_3} [inst : LinearOrderedSemiring R] {a b : R} {n : ℕ},
0 ≤ a → 0 ≤ b → n ≠ 0 → (a ^ n ≤ b ^ n ↔ a ≤ b)
This theorem states that for any type `R` which is a linear ordered semiring, and for any two elements `a` and `b` of this type, and a natural number `n`, if `a` and `b` are both non-negative and `n` is non-zero, then `a` raised to the power `n` is less than or equal to `b` raised to the power of `n` if and only if `a` is less than or equal to `b`. This theorem effectively provides a way to compare powers of non-negative numbers in a linear ordered semiring.
More concisely: For any linear ordered semiring (R, ≤, +, ⋅) and non-zero natural number n, a ≤ b if and only if a^n ≤ b^n.
|
pow_le_one
theorem pow_le_one : ∀ {R : Type u_3} [inst : OrderedSemiring R] {a : R} (n : ℕ), 0 ≤ a → a ≤ 1 → a ^ n ≤ 1
This theorem, `pow_le_one`, states that for any type `R` that has an ordered semiring structure, and for any element `a` of `R` and any natural number `n`, if `a` is non-negative and less than or equal to 1, then `a` to the power of `n` is also less than or equal to 1. In mathematical terms, it states that for all $a \in R$ and $n \in \mathbb{N}$, if $0 \leq a \leq 1$, then $a^n \leq 1$.
More concisely: For any ordered semiring type $R$ and all $a \in R$ with $0 \leq a \leq 1$ and natural number $n$, $a^n \leq 1$.
|
pow_left_strictMonoOn
theorem pow_left_strictMonoOn :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {n : ℕ}, n ≠ 0 → StrictMonoOn (fun x => x ^ n) {a | 0 ≤ a} := by
sorry
The theorem `pow_left_strictMonoOn` states that for any strict ordered semiring `R`, and any natural number `n` that is not zero, the function `f(x) = x^n` is strictly monotonic on the set of `a` such that `a` is greater than or equal to 0. In other words, for any two elements `a` and `b` from this set, if `a` is less than `b`, then `a^n` is less than `b^n`.
More concisely: For any strict ordered semiring R and natural number n > 0, the function x ↔ x^n is strict monotonic on the non-negative elements of R, i.e., if 0 ≤ a < b, then a^n < b^n.
|
Nat.pow_lt_pow_of_lt_right
theorem Nat.pow_lt_pow_of_lt_right :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R} {n m : ℕ}, 1 < a → m < n → a ^ m < a ^ n
This theorem, named `Nat.pow_lt_pow_of_lt_right`, states that for any strictly ordered semiring `R`, given a real number `a` from `R` and two natural numbers `n` and `m`, if `a` is greater than 1 and `m` is less than `n`, then `a` to the power of `m` is less than `a` to the power of `n`. In other words, it proves that in a strictly ordered semiring, for any number greater than 1, raising it to a higher natural number exponent results in a larger output.
More concisely: For any strictly ordered semiring R and natural numbers n, m with m < n, and a > 1 in R, a^m < a^n.
|
le_of_pow_le_pow
theorem le_of_pow_le_pow :
∀ {R : Type u_3} [inst : LinearOrderedSemiring R] {a b : R} {n : ℕ}, n ≠ 0 → 0 ≤ b → a ^ n ≤ b ^ n → a ≤ b := by
sorry
This theorem, `le_of_pow_le_pow`, is an alias of `le_of_pow_le_pow_left`. It states that for any type `R` that has a structure of a linear ordered semiring, for any two elements `a` and `b` of `R`, and for any natural number `n` that is not zero, if `b` is non-negative and `a` to the power of `n` is less than or equal to `b` to the power of `n`, then `a` is less than or equal to `b`.
More concisely: For any linear ordered semiring `R`, if `0 < n`, `b` is non-negative in `R`, and `a^n <= b^n`, then `a <= b` in `R`.
|
pow_strictMono_right
theorem pow_strictMono_right :
∀ {R : Type u_3} [inst : StrictOrderedSemiring R] {a : R}, 1 < a → StrictMono fun x => a ^ x
This theorem, referred to as `pow_strictMono_right`, states that for any strictly ordered semiring `R` and any element `a` from `R`, if `a` is greater than 1, then the function `f(x) = a ^ x` is strictly monotone. In other words, if `a` is larger than 1, then for any two elements of `R`, say `b` and `c`, if `b < c` then `a ^ b < a ^ c`.
More concisely: For any strictly ordered semiring `R` and `a` in `R` with `a > 1`, the function `f(x) = a ^ x` is strictly increasing.
|