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

source

theorem sqrt_one_add_norm_sq_le {E : Type u_1} [normed_add_comm_group E] (x : E) :

√ (1 + ‖x‖ ^ 2) ≤ 1 + ‖x‖

source

theorem one_add_norm_le_sqrt_two_mul_sqrt {E : Type u_1} [normed_add_comm_group E] (x : E) :

1 + ‖x‖ ≤ √ 2 * √ (1 + ‖x‖ ^ 2)

source

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

source

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

source

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) :

metric.closed_ball 0 (t ^ -r⁻¹ - 1) = ∅

source

theorem finite_integral_rpow_sub_one_pow_aux {r : ℝ} (n : ℕ) (hnr : ↑n < r) :

∫⁻ (x : ℝ) in set.Ioc 0 1, ennreal.of_real ((x ^ -r⁻¹ - 1) ^ n) < ⊤

source

theorem finite_integral_one_add_norm {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measure_theory.measure_space E] [borel_space E] [measure_theory.measure_space.volume.is_add_haar_measure] {r : ℝ} (hnr : ↑(fdim E) < r) :

∫⁻ (x : E), ennreal.of_real ((1 + ‖x‖) ^ -r) < ⊤

source

theorem integrable_one_add_norm {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measure_theory.measure_space E] [borel_space E] [measure_theory.measure_space.volume.is_add_haar_measure] {r : ℝ} (hnr : ↑(fdim E) < r) :

measure_theory.integrable (λ (x : E), (1 + ‖x‖) ^ -r) measure_theory.measure_space.volume

source

theorem integrable_rpow_neg_one_add_norm_sq {E : Type u_1} [normed_add_comm_group E] [normed_space ℝ E] [finite_dimensional ℝ E] [measure_theory.measure_space E] [borel_space E] [measure_theory.measure_space.volume.is_add_haar_measure] {r : ℝ} (hnr : ↑(fdim E) < r) :

measure_theory.integrable (λ (x : E), (1 + ‖x‖ ^ 2) ^ (-r / 2)) measure_theory.measure_space.volume