mathlib3 documentation

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 #

theorem sqrt_one_add_norm_sq_le {E : Type u_1} [normed_add_comm_group E] (x : E) :
(1 + x ^ 2) 1 + x
theorem rpow_neg_one_add_norm_sq_le {E : Type u_1} [normed_add_comm_group 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} [normed_add_comm_group E] {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) [normed_add_comm_group E] {r t : } (hr : 0 < r) (ht : 1 < t) :
theorem finite_integral_rpow_sub_one_pow_aux {r : } (n : ) (hnr : n < r) :