English
If |t| ≠ 0 and p ≥ 0, then |x|^p ≤ (p/|t|)^p · exp(|t| · |x|) for all real x, with t fixed and nonzero.
Русский
Если |t| ≠ 0 и p ≥ 0, то для всех x ∈ ℝ выполняется |x|^p ≤ (p/|t|)^p · exp(|t| · |x|).
LaTeX
$$$\forall x \in \mathbb{R}, \forall p \in \mathbb{R}_{\ge 0}, \forall t \in \mathbb{R}, t \neq 0: |x|^p \le \left(\frac{p}{|t|}\right)^p \cdot \exp(|t| \cdot |x|).$$$
Lean4
theorem rpow_abs_le_mul_exp_abs (x : ℝ) {t p : ℝ} (hp : 0 ≤ p) (ht : t ≠ 0) :
|x| ^ p ≤ (p / |t|) ^ p * exp (|t| * |x|) :=
by
refine (rpow_abs_le_mul_max_exp_of_pos x hp (t := |t|) ?_).trans_eq ?_
· simp [ht]
· congr
rcases le_total 0 x with hx | hx
· rw [abs_of_nonneg hx]
simp only [neg_mul, sup_eq_left, exp_le_exp, neg_le_self_iff]
positivity
· rw [abs_of_nonpos hx]
simp only [neg_mul, mul_neg, sup_eq_right, exp_le_exp, le_neg_self_iff]
exact mul_nonpos_of_nonneg_of_nonpos (abs_nonneg _) hx
