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} [NormedAddCommGroup E] (x : E) : Real.sqrt (1 + ‖x‖ ^ 2) ≤ 1 + ‖x‖

theorem one_add_norm_le_sqrt_two_mul_sqrt {E : Type u_1} [NormedAddCommGroup E] (x : E) : 1 + ‖x‖ ≤ Real.sqrt 2 * Real.sqrt (1 + ‖x‖ ^ 2)

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) : Metric.closedBall 0 (t ^ (-r⁻¹) - 1) = ∅

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} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.Measure.IsAddHaarMeasure μ] {r : ℝ} (hnr : ↑(FiniteDimensional.finrank ℝ E) < r) : ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ < ⊤

theorem integrable_one_add_norm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.Measure.IsAddHaarMeasure μ] {r : ℝ} (hnr : ↑(FiniteDimensional.finrank ℝ E) < r) : MeasureTheory.Integrable (fun (x : E) => (1 + ‖x‖) ^ (-r)) μ

theorem integrable_rpow_neg_one_add_norm_sq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.Measure.IsAddHaarMeasure μ] {r : ℝ} (hnr : ↑(FiniteDimensional.finrank ℝ E) < r) : MeasureTheory.Integrable (fun (x : E) => (1 + ‖x‖ ^ 2) ^ (-r / 2)) μ