English
For any real x and positive t, p ≥ 0, one has |x|^p ≤ (p/t)^p · max(exp(t x), exp(-t x)).
Русский
Для любого действительного x и положительного t, p ≥ 0 выполняется неравенство |x|^p ≤ (p/t)^p · max(e^{t x}, e^{-t x}).
LaTeX
$$$|x|^p \\leq \\left( \\frac{p}{t} \\right)^p \\max\\bigl( e^{t x}, e^{-t x} \\bigr)$$$
Lean4
/-- `integrableExpSet X μ` is a convex subset of `ℝ` (it is an interval). -/
theorem convex_integrableExpSet : Convex ℝ (integrableExpSet X μ) :=
by
rintro t₁ ht₁ t₂ ht₂ a b ha hb hab
wlog h_le : t₁ ≤ t₂
· rw [add_comm] at hab ⊢
exact this ht₂ ht₁ hb ha hab (not_le.mp h_le).le
refine integrable_exp_mul_of_le_of_le ht₁ ht₂ ?_ ?_
· simp only [smul_eq_mul]
calc
t₁
_ = a * t₁ + b * t₁ := by rw [← add_mul, hab, one_mul]
_ ≤ a * t₁ + b * t₂ := by gcongr
· simp only [smul_eq_mul]
calc
a * t₁ + b * t₂
_ ≤ a * t₂ + b * t₂ := by gcongr
_ = t₂ := by rw [← add_mul, hab, one_mul]
