# 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 #

• 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 closedBall_rpow_sub_one_eq_empty_aux (E : Type u_1) {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) <
theorem finite_integral_one_add_norm {E : Type u_1} [] [] [] [] {μ : } {r : } (hnr : < r) :
∫⁻ (x : E), ENNReal.ofReal ((1 + x) ^ (-r))μ <
theorem integrable_one_add_norm {E : Type u_1} [] [] [] [] {μ : } {r : } (hnr : < r) :
MeasureTheory.Integrable (fun (x : E) => (1 + x) ^ (-r)) μ
theorem integrable_rpow_neg_one_add_norm_sq {E : Type u_1} [] [] [] [] {μ : } {r : } (hnr : < r) :
MeasureTheory.Integrable (fun (x : E) => (1 + x ^ 2) ^ (-r / 2)) μ