[Merged by Bors] - feat(analysis/special_functions): the japanese bracket

src/analysis/special_functions/japanese_bracket.lean

@@ -0,0 +1,214 @@
+/-
+Copyright (c) 2022 Moritz Doll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll
+-/
+
+import analysis.special_functions.integrals
+import analysis.special_functions.pow
+import measure_theory.integral.integral_eq_improper
+import measure_theory.integral.layercake
+import tactic.positivity
+
+/-!
+# 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
+
+-/
+
+
+noncomputable theory
+
+open_locale big_operators nnreal filter topological_space ennreal
+
+open asymptotics filter set real measure_theory finite_dimensional
+
+variables {E : Type*} [normed_add_comm_group E]
+
+lemma jap_le_one_add_norm (x : E) : real.sqrt (1 + ∥x∥^2) ≤ 1 + ∥x∥ :=
+begin
+  have h1 : 0 ≤ 1 + ∥x∥^2 := by positivity,
+  have h2 : 0 ≤ 1 + ∥x∥ := by positivity,
+  have h3 : 0 < 2 := by positivity,
+  refine le_of_pow_le_pow 2 h2 h3 _,
+  rw [sq_sqrt h1, add_pow_two],
+  simp,
+end
+
+lemma one_add_norm_le_jap (x : E) : 1 + ∥x∥ ≤ (real.sqrt 2) * sqrt (1 + ∥x∥^2) :=
+begin
+  have h1 : 0 ≤ 1 + ∥x∥^2 := by positivity,
+  have h2 : 0 ≤ (real.sqrt 2) * real.sqrt (1 + ∥x∥^2) := by positivity,
+  have : (sqrt 2 * sqrt (1 + ∥x∥ ^ 2)) ^ 2 - (1 + ∥x∥) ^ 2 = (1 - ∥x∥) ^2 :=
+  begin
+    rw [mul_pow, sq_sqrt h1, add_pow_two, sub_pow_two],
+    norm_num,
+    ring,
+  end,
+  refine le_of_pow_le_pow 2 h2 (by norm_num) _,
+  rw [←sub_nonneg, this],
+  positivity,
+end
+
+lemma rpow_neg_jap_le_one_add_norm {r : ℝ} (x : E) (hr : 0 < r) :
+  (1 + ∥x∥^2)^(-r/2) ≤ 2^(r/2) * (1 + ∥x∥)^(-r) :=
+begin
+  have h1 : 0 ≤ (2 : ℝ) := by positivity,
+  have h2 : 0 ≤ (1 + ∥x∥^2) := by positivity,
+  have h3 : 0 < sqrt 2 := by positivity,
+  have h4 : 0 < 1 + ∥x∥ := by positivity,
+  have h5 : 0 < sqrt (1 + ∥x∥ ^ 2) := by positivity,
+  have h6 : 0 < sqrt 2 * sqrt (1 + ∥x∥^2) := mul_pos h3 h5,
+  rw [rpow_div_two_eq_sqrt _ h1, rpow_div_two_eq_sqrt _ h2, ←inv_mul_le_iff (rpow_pos_of_pos h3 _),
+    rpow_neg h4.le, rpow_neg (sqrt_nonneg _), ←mul_inv, ←mul_rpow h3.le h5.le,
+    inv_le_inv (rpow_pos_of_pos h6 _) (rpow_pos_of_pos h4 _), rpow_le_rpow_iff h4.le h6.le hr],
+  exact one_add_norm_le_jap _,
+end
+
+variables (E)
+
+lemma set_le_one_add_norm_eq_closed_ball_aux {r t : ℝ} (hr : 0 < r) (ht : 0 < t) :
+  {a : E | t ≤ (1 + ∥a∥) ^ -r} = metric.closed_ball 0 (t^(-r⁻¹) - 1) :=
+begin
+  ext,
+  simp only [norm_eq_abs, mem_set_of_eq, mem_closed_ball_zero_iff],
+  rw [le_sub_iff_add_le', neg_inv],
+  exact (real.le_rpow_inv_iff_of_neg (by positivity) ht (neg_lt_zero.mpr hr)).symm,
+end
+
+lemma closed_ball_rpow_sub_one_eq_empty_aux {r t : ℝ} (hr : 0 < r) (ht : 1 < t) :
+  metric.closed_ball (0 : E) (t^(-r⁻¹) - 1) = ∅ :=
+begin
+  rw [metric.closed_ball_eq_empty, sub_neg],
+  exact real.rpow_lt_one_of_one_lt_of_neg ht (by simp only [hr, right.neg_neg_iff, inv_pos]),
+end
+
+variables [normed_space ℝ E] [finite_dimensional ℝ E]
+
+variables {E}
+
+lemma finite_integral_rpow_sub_one_pow_aux {r : ℝ} (n : ℕ) (hnr : (n : ℝ) < r) :
+  ∫⁻ (x : ℝ) in Ioc 0 1, ennreal.of_real ((x ^ -r⁻¹ - 1) ^ n) < ∞ :=
+begin
+  have hr : 0 < r := lt_of_le_of_lt n.cast_nonneg hnr,
+  have h_int : ∀ (x : ℝ) (hx : x ∈ Ioc (0 : ℝ) 1),
+    ennreal.of_real ((x ^ -r⁻¹ - 1) ^ n) ≤ ennreal.of_real (x ^ -(r⁻¹ * n)) :=
+  begin
+    intros x hx,
+    have hxr : 0 ≤ x^ -r⁻¹ := rpow_nonneg_of_nonneg hx.1.le _,
+    apply ennreal.of_real_le_of_real,
+    rw [←neg_mul, rpow_mul hx.1.le, rpow_nat_cast],
+    refine pow_le_pow_of_le_left _ (by simp only [sub_le_self_iff, zero_le_one]) n,
+    rw [le_sub_iff_add_le', add_zero],
+    refine real.one_le_rpow_of_pos_of_le_one_of_nonpos hx.1 hx.2 _,
+    simp only [hr.le, right.neg_nonpos_iff, inv_nonneg],
+  end,
+  refine lt_of_le_of_lt (set_lintegral_mono (by measurability) (by measurability) h_int) _,
+  refine integrable_on.set_lintegral_lt_top _,
+  rw ←interval_integrable_iff_integrable_Ioc_of_le zero_le_one,
+  apply interval_integral.interval_integrable_rpow',
+  simp [neg_lt_neg_iff, inv_mul_lt_iff' hr, hnr],
+end
+
+lemma finite_integral_one_add_norm [measure_space E] [borel_space E]
+  [(@volume E _).is_add_haar_measure] {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) :
+  ∫⁻ (x : E), ennreal.of_real ((1 + ∥x∥) ^ -r) < ∞ :=
+begin
+  have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr,
+
+  -- We start by applying the layer cake formula
+  have h_meas : measurable (λ (ω : E), (1 + ∥ω∥) ^ -r) := by measurability,
+  have h_pos : ∀ x : E, 0 ≤ (1 + ∥x∥) ^ -r :=
+  by { intros x, positivity },
+  rw lintegral_eq_lintegral_meas_le volume h_pos h_meas,
+
+  -- We use the first transformation of the integrant to show that we only have to integrate from
+  -- 0 to 1 and from 1 to ∞
+  have h_int : ∀ (t : ℝ) (ht : t ∈ Ioi (0 : ℝ)),
+    (volume {a : E | t ≤ (1 + ∥a∥) ^ -r} : ennreal) =
+    volume (metric.closed_ball (0 : E) (t^(-r⁻¹) - 1)) :=
+  begin
+    intros t ht,
+    congr' 1,
+    exact set_le_one_add_norm_eq_closed_ball_aux E hr (mem_Ioi.mp ht),
+  end,
+  rw set_lintegral_congr_fun measurable_set_Ioi (ae_of_all volume $ h_int),
+  have hIoi_eq : Ioi (0 : ℝ) = Ioc (0 : ℝ) 1 ∪ Ioi 1 :=
+    (set.Ioc_union_Ioi_eq_Ioi zero_le_one).symm,
+  have hdisjoint : disjoint (Ioc (0 : ℝ) 1) (Ioi 1) := by simp [disjoint_iff],
+  rw [hIoi_eq, lintegral_union measurable_set_Ioi hdisjoint, ennreal.add_lt_top],
+
+  have h_int' : ∀ (t : ℝ) (ht : t ∈ Ioc (0 : ℝ) 1),
+    (volume (metric.closed_ball (0 : E) (t^(-r⁻¹) - 1)) : ennreal) =
+    ennreal.of_real ((t^(-r⁻¹) - 1) ^ finite_dimensional.finrank ℝ E)
+      * volume (metric.ball (0:E) 1) :=
+  begin
+    intros t ht,
+    rw measure.add_haar_closed_ball,
+    rw [le_sub_iff_add_le', add_zero],
+    exact real.one_le_rpow_of_pos_of_le_one_of_nonpos ht.1 ht.2 (by simp [hr.le]),
+  end,
+  have h_meas' : measurable (λ (a : ℝ), ennreal.of_real ((a ^ -r⁻¹ - 1) ^ finrank ℝ E)) :=
+  by measurability,
+  split,
+  -- The integral from 0 to 1:
+  { rw [set_lintegral_congr_fun measurable_set_Ioc (ae_of_all volume $ h_int'),
+      lintegral_mul_const _ h_meas', ennreal.mul_lt_top_iff],
+    left,
+    -- We calculate the integral
+    use finite_integral_rpow_sub_one_pow_aux _ hnr,
+    -- The unit ball has finite measure
+    rw ←measure.add_haar_closed_unit_ball_eq_add_haar_unit_ball,
+    exact (is_compact_closed_ball _ _).measure_lt_top, },
+
+  -- The integral from 1 to ∞ is zero:
+  have h_int'' : ∀ (t : ℝ) (ht : t ∈ Ioi (1 : ℝ)),
+    (volume (metric.closed_ball (0 : E) (t^(-r⁻¹) - 1)) : ennreal) = 0 :=
+  begin
+    intros t ht,
+    rw closed_ball_rpow_sub_one_eq_empty_aux E hr ht,
+    simp,
+  end,
+  rw set_lintegral_congr_fun measurable_set_Ioi (ae_of_all volume $ h_int''),
+  simp,
+end
+
+lemma integrable_one_add_norm [measure_space E] [borel_space E] [(@volume E _).is_add_haar_measure]
+  {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) :
+  integrable (λ (x : E), (1 + ∥x∥) ^ -r) :=
+begin
+  refine ⟨by measurability, _⟩,
+  -- Lower Lebesgue integral
+  have : ∫⁻ (a : E), ∥(1 + ∥a∥) ^ -r∥₊ =
+    ∫⁻ (a : E), ennreal.of_real ((1 + ∥a∥) ^ -r) :=
+  begin
+    refine lintegral_nnnorm_eq_of_nonneg (λ x, _),
+    have h : 0 ≤ (1 + ∥x∥) ^ -r := rpow_nonneg_of_nonneg (by positivity) _,
+    simp [h],
+  end,
+  rw [has_finite_integral, this],
+  exact finite_integral_one_add_norm hnr,
+end
+
+lemma integrable_jap [measure_space E] [borel_space E] [(@volume E _).is_add_haar_measure]
+  {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) :
+  integrable (λ (x : E), (1 + ∥x∥^2) ^ (-r/2)) :=
+begin
+  have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr,
+  refine ((integrable_one_add_norm hnr).const_mul $ 2 ^ (r / 2)).mono (by measurability)
+    (eventually_of_forall $ λ x, _),
+  have h1 : 0 ≤ (1 + ∥x∥ ^ 2) ^ (-r/2) := by positivity,
+  have h2 : 0 ≤ (1 + ∥x∥) ^ -r := by positivity,
+  have h3 : 0 ≤ (2 : ℝ)^(r/2) := by positivity,
+  simp_rw [norm_mul, norm_eq_abs, abs_of_nonneg h1, abs_of_nonneg h2, abs_of_nonneg h3],
+  exact rpow_neg_jap_le_one_add_norm _ hr,
+end

src/measure_theory/measure/haar_lebesgue.lean

@@ -459,6 +459,15 @@ lemma add_haar_closed_ball (x : E) {r : ℝ} (hr : 0 ≤ r) :
   μ (closed_ball x r) = ennreal.of_real (r ^ (finrank ℝ E)) * μ (ball 0 1) :=
 by rw [add_haar_closed_ball' μ x hr, add_haar_closed_unit_ball_eq_add_haar_unit_ball]
 
+lemma add_haar_closed_ball_eq_add_haar_ball [nontrivial E] (x : E) (r : ℝ) :
+  μ (closed_ball x r) = μ (ball x r) :=
+begin
+  by_cases h : r < 0,
+  { rw [metric.closed_ball_eq_empty.mpr h, metric.ball_eq_empty.mpr h.le] },
+  push_neg at h,
+  rw [add_haar_closed_ball μ x h, add_haar_ball μ x h],
+end
+
 lemma add_haar_sphere_of_ne_zero (x : E) {r : ℝ} (hr : r ≠ 0) :
   μ (sphere x r) = 0 :=
 begin
@@ -470,6 +479,19 @@ begin
     apply_instance }
 end
 
+-- For the following lemma we don't need to assume that the space is Borel
+variables {F : Type*} [normed_add_comm_group F] [measurable_space F] [normed_space ℝ F]
+  [finite_dimensional ℝ F] (ν : measure F) [is_add_haar_measure ν]
+
+lemma add_haar_closed_ball_lt_top (x : F) (r : ℝ): ν (closed_ball x r) < ∞ :=
+(is_compact_closed_ball _ _).measure_lt_top
+
+lemma add_haar_ball_lt_top [nontrivial E] (x : E) (r : ℝ) : μ (ball x r) < ∞ :=
+begin
+  rw ←add_haar_closed_ball_eq_add_haar_ball,
+  exact add_haar_closed_ball_lt_top _ _ _,
+end
+
 lemma add_haar_sphere [nontrivial E] (x : E) (r : ℝ) :
   μ (sphere x r) = 0 :=
 begin