Mathlib.Algebra.Order.Ring.Pow

one_add_mul_le_pow' theorem

(Hsq : 0 ≤ a * a) (Hsq' : 0 ≤ (1 + a) * (1 + a)) (H : 0 ≤ 2 + a) : ∀ n : ℕ, 1 + n * a ≤ (1 + a) ^ n

Full source

/-- **Bernoulli's inequality**. This version works for semirings but requires
additional hypotheses `0 ≤ a * a` and `0 ≤ (1 + a) * (1 + a)`. -/
lemma one_add_mul_le_pow' (Hsq : 0 ≤ a * a) (Hsq' : 0 ≤ (1 + a) * (1 + a)) (H : 0 ≤ 2 + a) :
    ∀ n : ℕ, 1 + n * a ≤ (1 + a) ^ n
  | 0 => by simp
  | 1 => by simp
  | n + 2 =>
    have : 0 ≤ n * (a * a * (2 + a)) + a * a :=
      add_nonneg (mul_nonneg n.cast_nonneg (mul_nonneg Hsq H)) Hsq
    calc
      _ ≤ 1 + ↑(n + 2) * a + (n * (a * a * (2 + a)) + a * a) := le_add_of_nonneg_right this
      _ = (1 + a) * (1 + a) * (1 + n * a) := by
          simp only [Nat.cast_add, add_mul, mul_add, one_mul, mul_one, ← one_add_one_eq_two,
            Nat.cast_one, add_assoc, add_right_inj]
          simp only [← add_assoc, add_comm _ (↑n * a)]
          simp only [add_assoc, (n.cast_commute (_ : R)).left_comm]
          simp only [add_comm, add_left_comm]
      _ ≤ (1 + a) * (1 + a) * (1 + a) ^ n :=
        mul_le_mul_of_nonneg_left (one_add_mul_le_pow' Hsq Hsq' H _) Hsq'
      _ = (1 + a) ^ (n + 2) := by simp only [pow_succ', mul_assoc]

Bernoulli's Inequality for Semirings with Additional Nonnegativity Conditions

Informal description

Let $a$ be an element of a semiring such that $0 \leq a^2$, $0 \leq (1 + a)^2$, and $0 \leq 2 + a$. Then for every natural number $n$, we have the inequality: \[ 1 + n \cdot a \leq (1 + a)^n. \]

one_add_mul_le_pow theorem

(H : -2 ≤ a) (n : ℕ) : 1 + n * a ≤ (1 + a) ^ n

Full source

/-- **Bernoulli's inequality** for `n : ℕ`, `-2 ≤ a`. -/
lemma one_add_mul_le_pow (H : -2 ≤ a) (n : ℕ) : 1 + n * a ≤ (1 + a) ^ n :=
  one_add_mul_le_pow' (mul_self_nonneg _) (mul_self_nonneg _) (neg_le_iff_add_nonneg'.1 H) _

Bernoulli's Inequality: $1 + n a \leq (1 + a)^n$ for $-2 \leq a$ and $n \in \mathbb{N}$

Informal description

For any real number $a$ with $-2 \leq a$ and any natural number $n$, the following inequality holds: \[ 1 + n \cdot a \leq (1 + a)^n. \]

one_add_mul_sub_le_pow theorem

(H : -1 ≤ a) (n : ℕ) : 1 + n * (a - 1) ≤ a ^ n

Full source

/-- **Bernoulli's inequality** reformulated to estimate `a^n`. -/
lemma one_add_mul_sub_le_pow (H : -1 ≤ a) (n : ℕ) : 1 + n * (a - 1) ≤ a ^ n := by
  have : -2 ≤ a - 1 := by
    rwa [← one_add_one_eq_two, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right]
  simpa only [add_sub_cancel] using one_add_mul_le_pow this n

Bernoulli's Inequality Variant: $1 + n(a - 1) \leq a^n$ for $-1 \leq a$ and $n \in \mathbb{N}$

Informal description

For any real number $a$ with $-1 \leq a$ and any natural number $n$, the following inequality holds: \[ 1 + n \cdot (a - 1) \leq a^n. \]