Bernoulli's inequality #
theorem
one_add_mul_le_pow'
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
{a : R}
(Hsq : 0 ≤ a * a)
(Hsq' : 0 ≤ (1 + a) * (1 + a))
(H : 0 ≤ 2 + a)
(n : ℕ)
:
Bernoulli's inequality. This version works for semirings but requires
additional hypotheses 0 ≤ a * a and 0 ≤ (1 + a) * (1 + a).
theorem
one_add_mul_le_pow
{R : Type u_1}
[Ring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{a : R}
(H : -2 ≤ a)
(n : ℕ)
:
Bernoulli's inequality for n : ℕ, -2 ≤ a.
theorem
one_add_mul_sub_le_pow
{R : Type u_1}
[Ring R]
[LinearOrder R]
[IsStrictOrderedRing R]
{a : R}
(H : -1 ≤ a)
(n : ℕ)
:
Bernoulli's inequality reformulated to estimate a^n.