convexOn_exp
theorem convexOn_exp : ConvexOn ℝ Set.univ Real.exp
The theorem `convexOn_exp` asserts that the real exponential function `Real.exp` is convex on the entire real number line. In mathematical terms, a function is said to be convex on a set if, for any two points in the set and any two non-negative real numbers summing to 1, the value of the function at the weighted sum of the two points is less than or equal to the weighted sum of the values of the function at the two points. Hence, for any two real numbers and any two non-negative real numbers that sum to 1, the value of `Real.exp` at the weighted sum of the two real numbers is less than or equal to the weighted sum of the values of `Real.exp` at the two real numbers.
More concisely: For all real numbers x and y and non-negative real numbers α and β with α + β = 1, Real.exp α * x^2 + Real.exp β * y^2 ≤ Real.exp (α * x + β * y) * (x^2 + y^2).
|
one_add_mul_self_lt_rpow_one_add
theorem one_add_mul_self_lt_rpow_one_add : ∀ {s : ℝ}, -1 ≤ s → s ≠ 0 → ∀ {p : ℝ}, 1 < p → 1 + p * s < (1 + s) ^ p := by
sorry
This is a strict version of **Bernoulli's inequality** for real exponents. It states that for any real numbers `s` and `p` where `s` is not equal to `0` and lies between `-1` and `1`, and `p` is greater than `1`, the inequality `1 + p * s < (1 + s) ^ p` holds true.
More concisely: For real numbers `s` with `-1 < s < 0` and `p > 1`, the inequality `1 + p*s < (1+s) ^ p` holds.
|
one_add_mul_self_le_rpow_one_add
theorem one_add_mul_self_le_rpow_one_add : ∀ {s : ℝ}, -1 ≤ s → ∀ {p : ℝ}, 1 ≤ p → 1 + p * s ≤ (1 + s) ^ p
The theorem `one_add_mul_self_le_rpow_one_add` states Bernoulli's inequality for real exponents in a non-strict version. Specifically, it states that for any real numbers `s` and `p` such that `-1 ≤ s` and `1 ≤ p`, the inequality `1 + p * s ≤ (1 + s) ^ p` holds. This can be understood as stating that the value of `1 + p * s` is less than or equal to the `p`-th power of `(1 + s)`, under the given conditions on `s` and `p`. This inequality has various applications in mathematics including calculus and number theory.
More concisely: For any real numbers `s` with `-1 ≤ s` and `p` with `1 ≤ p`, `1 + p * s ≤ (1 + s) ^ p`.
|
strictConvexOn_exp
theorem strictConvexOn_exp : StrictConvexOn ℝ Set.univ Real.exp
The theorem `strictConvexOn_exp` states that the real exponential function `Real.exp` exhibits strict convexity over the entire set of real numbers. In more detail, for any two distinct points `x` and `y` in the real number line and any positive real numbers `a` and `b` summing to one, the value of the exponential function at the weighted average of `x` and `y` (with weights `a` and `b`) is strictly less than the weighted average of the exponential function values at `x` and `y`. This property signifies the "curved" shape of the exponential function on the real number line.
More concisely: For any distinct real numbers x and y, and any positive real numbers a and b summing to one, we have a * Real.exp x + b * Real.exp y < Real.exp (a * x + b * y).
|