# mathlib3documentation

analysis.special_functions.japanese_bracket

# Japanese Bracket #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• integrable_one_add_norm: the function $(1 + |x|)^{-r}$ is integrable
• integrable_jap the Japanese bracket is integrable
theorem sqrt_one_add_norm_sq_le {E : Type u_1} (x : E) :
(1 + x ^ 2) 1 + x
theorem one_add_norm_le_sqrt_two_mul_sqrt {E : Type u_1} (x : E) :
1 + x 2 * (1 + x ^ 2)
theorem rpow_neg_one_add_norm_sq_le {E : Type u_1} {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} {r t : } (hr : 0 < r) (ht : 0 < t) (x : E) :
t (1 + x) ^ -r x t ^ -r⁻¹ - 1
theorem closed_ball_rpow_sub_one_eq_empty_aux (E : Type u_1) {r t : } (hr : 0 < r) (ht : 1 < t) :
(t ^ -r⁻¹ - 1) =
theorem finite_integral_rpow_sub_one_pow_aux {r : } (n : ) (hnr : n < r) :
∫⁻ (x : ) in 1, ennreal.of_real ((x ^ -r⁻¹ - 1) ^ n) <
theorem finite_integral_one_add_norm {E : Type u_1} [ E] [borel_space E] {r : } (hnr : (fdim E) < r) :
theorem integrable_one_add_norm {E : Type u_1} [ E] [borel_space E] {r : } (hnr : (fdim E) < r) :
theorem integrable_rpow_neg_one_add_norm_sq {E : Type u_1} [ E] [borel_space E] {r : } (hnr : (fdim E) < r) :