Theorems · Theorem · real analysis

rpow_one_add_lt_one_add_mul_self

∀ {s : ℝ}, -1 ≤ s → s ≠ 0 → ∀ {p : ℝ}, 0 < p → p < 1 → (1 + s) ^ p < 1 + p * s

Bernoulli's inequality for real exponents, strict version: for 0 < p < 1 and -1 ≤ s, with s ≠ 0, we have (1 + s) ^ p < 1 + p * s.

Defined in

Mathlib.Analysis.Convex.SpecificFunctions.Basic

Cited by

1 results in Mathlib

Foundations

Depth 195 from the axioms · uses propext, Classical.choice, Quot.sound