English
For any real x, any nonnegative p, and any nonzero t, the power |x|^p is bounded by (p/|t|)^p times the larger of exp(t x) and exp(-t x).
Русский
Для любых действительных x, неотрицательного p и не нулевого t выполняется неравенство |x|^p ≤ (p/|t|)^p · max(e^{t x}, e^{-t x}).
LaTeX
$$$\forall x \in \mathbb{R}, \forall p \in \mathbb{R}_{\ge 0}, \forall t \in \mathbb{R} \setminus \{0\}: |x|^p \le \left(\frac{p}{|t|}\right)^p \cdot \max(\exp(t x), \exp(-t x)).$$$
Lean4
theorem rpow_abs_le_mul_max_exp (x : ℝ) {t p : ℝ} (hp : 0 ≤ p) (ht : t ≠ 0) :
|x| ^ p ≤ (p / |t|) ^ p * max (exp (t * x)) (exp (-t * x)) :=
by
rcases lt_or_gt_of_ne ht with ht_neg | ht_pos
· rw [abs_of_nonpos ht_neg.le, sup_comm]
convert rpow_abs_le_mul_max_exp_of_pos x hp (t := -t) (by simp [ht_neg])
simp
· rw [abs_of_nonneg ht_pos.le]
exact rpow_abs_le_mul_max_exp_of_pos x hp ht_pos
