Documentation

Mathlib.Analysis.SpecialFunctions.JapaneseBracket

Japanese Bracket #

In this file, we show that Japanese bracket $(1 + |x|^2)^{1/2}$ can be estimated from above and below by $1 + |x|$. The functions $(1 + |x|^2)^{-r/2}$ and $(1 + |x|)^{-r}$ are integrable provided that r is larger than the dimension.

Main statements #

theorem rpow_neg_one_add_norm_sq_le {E : Type u_1} [NormedAddCommGroup E] {r : } (x : E) (hr : 0 < r) :
(1 + x ^ 2) ^ (-r / 2) 2 ^ (r / 2) * (1 + x) ^ (-r)
theorem le_rpow_one_add_norm_iff_norm_le {E : Type u_1} [NormedAddCommGroup E] {r : } {t : } (hr : 0 < r) (ht : 0 < t) (x : E) :
t (1 + x) ^ (-r) x t ^ (-r⁻¹) - 1
theorem closedBall_rpow_sub_one_eq_empty_aux (E : Type u_1) [NormedAddCommGroup E] {r : } {t : } (hr : 0 < r) (ht : 1 < t) :
theorem finite_integral_rpow_sub_one_pow_aux {r : } (n : ) (hnr : n < r) :
∫⁻ (x : ) in Set.Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) <