one_add_mul_le_pow
theorem one_add_mul_le_pow :
∀ {R : Type u_1} [inst : LinearOrderedRing R] {a : R}, -2 ≤ a → ∀ (n : ℕ), 1 + ↑n * a ≤ (1 + a) ^ n
This is a statement of Bernoulli's inequality for any natural number `n` and any real number `a` such that `-2 ≤ a`. The theorem states that for any linearly ordered ring `R`, the value of `1 + n*a` is always less than or equal to `(1 + a)^n`.
More concisely: For any natural number `n` and real number `a` with `-2 ≤ a`, in any linearly ordered ring `R`, `(1 + a)^n ≥ 1 + n*a`. (Note that the statement is typically stated with the inequality reversed due to Lean's convention of negating inequalities in its proof assistant.)
|
one_add_mul_le_pow'
theorem one_add_mul_le_pow' :
∀ {R : Type u_1} [inst : OrderedSemiring R] {a : R},
0 ≤ a * a → 0 ≤ (1 + a) * (1 + a) → 0 ≤ 2 + a → ∀ (n : ℕ), 1 + ↑n * a ≤ (1 + a) ^ n
The theorem states Bernoulli's Inequality in a version that is applicable to semirings. It asserts that for any ordered semiring `R` and any element `a` of `R` satisfying the conditions `0 ≤ a * a`, `0 ≤ (1 + a) * (1 + a)`, and `0 ≤ 2 + a`, for any natural number `n`, the inequality `1 + n * a ≤ (1 + a) ^ n` holds. In simpler terms, after adding 1 to the product of any natural number and any number in the semiring, the result will be less than or equal to the number you get when you raise `1 + a` to the power of that natural number.
More concisely: For any ordered semiring `R` and element `a` in `R` with `0 ≤ a ^ 2`, `0 ≤ 1 + a`, and `0 ≤ 1 + a`, the inequality `1 + n * a ≤ (1 + a) ^ n` holds for all natural numbers `n`.
|
one_add_mul_sub_le_pow
theorem one_add_mul_sub_le_pow :
∀ {R : Type u_1} [inst : LinearOrderedRing R] {a : R}, -1 ≤ a → ∀ (n : ℕ), 1 + ↑n * (a - 1) ≤ a ^ n
This theorem is a reformulated version of Bernoulli's inequality, which provides an estimation for `a^n` in the context of a linear ordered ring `R`. It states that for any real number `a` in `R` where `-1 ≤ a`, and for any natural number `n`, the inequality `1 + n * (a - 1) ≤ a^n` holds true. This essentially highlights that the left hand side expression is less than or equal to `a` raised to the power of `n`.
More concisely: For any real number `a` with `-1 ≤ a` in a linear ordered ring `R` and natural number `n`, the inequality `1 + n * (a - 1) ≤ a^n` holds true.
|