English
Auxiliary lemma giving a positive bound for |x|^p using exponentials; a version of the earlier lemma with explicit form.
Русский
Вспомогательная лемма, дающая неравенство для |x|^p через экспоненты; версия ранее упомянутой леммы.
LaTeX
$$$|x|^p \\leq \\left( \\frac{p}{t} \\right)^p \\max\\bigl( e^{t x}, e^{-t x} \\bigr)$$$
Lean4
/-- Auxiliary lemma for `rpow_abs_le_mul_max_exp`. -/
theorem rpow_abs_le_mul_max_exp_of_pos (x : ℝ) {t p : ℝ} (hp : 0 ≤ p) (ht : 0 < t) :
|x| ^ p ≤ (p / t) ^ p * max (exp (t * x)) (exp (-t * x)) :=
by
by_cases hp_zero : p = 0
· simp only [hp_zero, rpow_zero, zero_div, neg_mul, one_mul, le_sup_iff, one_le_exp_iff, Left.nonneg_neg_iff]
exact le_total 0 (t * x)
have h_x_le c (hc : 0 < c) : x ≤ c⁻¹ * exp (c * x) := le_inv_mul_exp x hc
have h_neg_x_le c (hc : 0 < c) : -x ≤ c⁻¹ * exp (-c * x) := by simpa using le_inv_mul_exp (-x) hc
have h_abs_le c (hc : 0 < c) : |x| ≤ c⁻¹ * max (exp (c * x)) (exp (-c * x)) :=
by
refine abs_le.mpr ⟨?_, ?_⟩
· rw [neg_le]
refine (h_neg_x_le c hc).trans ?_
gcongr
exact le_max_right _ _
· refine (h_x_le c hc).trans ?_
gcongr
exact le_max_left _ _
calc
|x| ^ p
_ ≤ ((t / p)⁻¹ * max (exp (t / p * x)) (exp (-t / p * x))) ^ p :=
by
refine rpow_le_rpow (abs_nonneg _) ?_ hp
convert h_abs_le (t / p) (div_pos ht (hp.lt_of_ne' hp_zero)) using 5
rw [neg_div]
_ = (p / t) ^ p * max (exp (t * x)) (exp (-t * x)) :=
by
rw [mul_rpow (by positivity) (by positivity)]
congr
· simp
· rw [rpow_max (by positivity) (by positivity) hp, ← exp_mul, ← exp_mul]
ring_nf
congr <;> rw [mul_assoc, mul_inv_cancel₀ hp_zero, mul_one]
