[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ sqrt (1 + ‖x‖ ^ 2) ≤ 1 + ‖x‖
[PROOFSTEP]
rw [sqrt_le_left (by positivity)]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 0 ≤ 1 + ‖x‖
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 1 + ‖x‖ ^ 2 ≤ (1 + ‖x‖) ^ 2
[PROOFSTEP]
simp [add_sq]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 1 + ‖x‖ ≤ sqrt 2 * sqrt (1 + ‖x‖ ^ 2)
[PROOFSTEP]
rw [← sqrt_mul zero_le_two]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 1 + ‖x‖ ≤ sqrt (2 * (1 + ‖x‖ ^ 2))
[PROOFSTEP]
have := sq_nonneg (‖x‖ - 1)
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
this : 0 ≤ (‖x‖ - 1) ^ 2
⊢ 1 + ‖x‖ ≤ sqrt (2 * (1 + ‖x‖ ^ 2))
[PROOFSTEP]
apply le_sqrt_of_sq_le
[GOAL]
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
this : 0 ≤ (‖x‖ - 1) ^ 2
⊢ (1 + ‖x‖) ^ 2 ≤ 2 * (1 + ‖x‖ ^ 2)
[PROOFSTEP]
linarith
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ (1 + ‖x‖ ^ 2) ^ (-r / 2) = 2 ^ (r / 2) * ((sqrt 2 * sqrt (1 + ‖x‖ ^ 2)) ^ r)⁻¹
[PROOFSTEP]
rw [rpow_div_two_eq_sqrt, rpow_div_two_eq_sqrt, mul_rpow, mul_inv, rpow_neg, mul_inv_cancel_left₀]
[GOAL]
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ sqrt 2 ^ r ≠ 0
[PROOFSTEP]
positivity
[GOAL]
case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ sqrt (1 + ‖x‖ ^ 2)
[PROOFSTEP]
positivity
[GOAL]
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ sqrt 2
[PROOFSTEP]
positivity
[GOAL]
case h₁
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ sqrt (1 + ‖x‖ ^ 2)
[PROOFSTEP]
positivity
[GOAL]
case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ 2
[PROOFSTEP]
positivity
[GOAL]
case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ 1 + ‖x‖ ^ 2
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 2 ^ (r / 2) * ((sqrt 2 * sqrt (1 + ‖x‖ ^ 2)) ^ r)⁻¹ ≤ 2 ^ (r / 2) * ((1 + ‖x‖) ^ r)⁻¹
[PROOFSTEP]
gcongr
[GOAL]
case h.h.h₁
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 1 + ‖x‖ ≤ sqrt 2 * sqrt (1 + ‖x‖ ^ 2)
[PROOFSTEP]
apply one_add_norm_le_sqrt_two_mul_sqrt
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 2 ^ (r / 2) * ((1 + ‖x‖) ^ r)⁻¹ = 2 ^ (r / 2) * (1 + ‖x‖) ^ (-r)
[PROOFSTEP]
rw [rpow_neg]
[GOAL]
case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ 1 + ‖x‖
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 0 < t
x : E
⊢ t ≤ (1 + ‖x‖) ^ (-r) ↔ ‖x‖ ≤ t ^ (-r⁻¹) - 1
[PROOFSTEP]
rw [le_sub_iff_add_le', neg_inv]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 0 < t
x : E
⊢ t ≤ (1 + ‖x‖) ^ (-r) ↔ 1 + ‖x‖ ≤ t ^ (-r)⁻¹
[PROOFSTEP]
exact (Real.le_rpow_inv_iff_of_neg (by positivity) ht (neg_lt_zero.mpr hr)).symm
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 0 < t
x : E
⊢ 0 < 1 + ‖x‖
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
⊢ Metric.closedBall 0 (t ^ (-r⁻¹) - 1) = ∅
[PROOFSTEP]
rw [Metric.closedBall_eq_empty, sub_neg]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
⊢ t ^ (-r⁻¹) < 1
[PROOFSTEP]
exact Real.rpow_lt_one_of_one_lt_of_neg ht (by simp only [hr, Right.neg_neg_iff, inv_pos])
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
⊢ -r⁻¹ < 0
[PROOFSTEP]
simp only [hr, Right.neg_neg_iff, inv_pos]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ⊤
[PROOFSTEP]
have hr : 0 < r := lt_of_le_of_lt n.cast_nonneg hnr
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ⊤
[PROOFSTEP]
have h_int : ∀ x : ℝ, x ∈ Ioc (0 : ℝ) 1 → ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * n))) :=
  fun x hx ↦ by
  apply ENNReal.ofReal_le_ofReal
  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 _
  rw [Right.neg_nonpos_iff, inv_nonneg]
  exact hr.le
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))
[PROOFSTEP]
apply ENNReal.ofReal_le_ofReal
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ (x ^ (-r⁻¹) - 1) ^ n ≤ x ^ (-(r⁻¹ * ↑n))
[PROOFSTEP]
rw [← neg_mul, rpow_mul hx.1.le, rpow_nat_cast]
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ (x ^ (-r⁻¹) - 1) ^ n ≤ (x ^ (-r⁻¹)) ^ n
[PROOFSTEP]
refine' pow_le_pow_of_le_left _ (by simp only [sub_le_self_iff, zero_le_one]) n
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ x ^ (-r⁻¹) - 1 ≤ x ^ (-r⁻¹)
[PROOFSTEP]
simp only [sub_le_self_iff, zero_le_one]
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ 0 ≤ x ^ (-r⁻¹) - 1
[PROOFSTEP]
rw [le_sub_iff_add_le', add_zero]
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ 1 ≤ x ^ (-r⁻¹)
[PROOFSTEP]
refine' Real.one_le_rpow_of_pos_of_le_one_of_nonpos hx.1 hx.2 _
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ -r⁻¹ ≤ 0
[PROOFSTEP]
rw [Right.neg_nonpos_iff, inv_nonneg]
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ 0 ≤ r
[PROOFSTEP]
exact hr.le
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
h_int : ∀ (x : ℝ), x ∈ Ioc 0 1 → ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ⊤
[PROOFSTEP]
refine' lt_of_le_of_lt (set_lintegral_mono' measurableSet_Ioc h_int) _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
h_int : ∀ (x : ℝ), x ∈ Ioc 0 1 → ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n))) < ⊤
[PROOFSTEP]
refine' IntegrableOn.set_lintegral_lt_top _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
h_int : ∀ (x : ℝ), x ∈ Ioc 0 1 → ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))
⊢ IntegrableOn (fun x => x ^ (-(r⁻¹ * ↑n))) (Ioc 0 1)
[PROOFSTEP]
rw [← intervalIntegrable_iff_integrable_Ioc_of_le zero_le_one]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
h_int : ∀ (x : ℝ), x ∈ Ioc 0 1 → ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))
⊢ IntervalIntegrable (fun x => x ^ (-(r⁻¹ * ↑n))) volume 0 1
[PROOFSTEP]
apply intervalIntegral.intervalIntegrable_rpow'
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
h_int : ∀ (x : ℝ), x ∈ Ioc 0 1 → ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))
⊢ -1 < -(r⁻¹ * ↑n)
[PROOFSTEP]
rwa [neg_lt_neg_iff, inv_mul_lt_iff' hr, one_mul]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) < ⊤
[PROOFSTEP]
have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
⊢ ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) < ⊤
[PROOFSTEP]
have h_meas : Measurable fun ω : E => (1 + ‖ω‖) ^ (-r) :=
  -- porting note: was `by measurability`(measurable_norm.const_add _).pow_const _
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
⊢ ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) < ⊤
[PROOFSTEP]
have h_pos : ∀ x : E, 0 ≤ (1 + ‖x‖) ^ (-r) := fun x ↦ by positivity
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
x : E
⊢ 0 ≤ (1 + ‖x‖) ^ (-r)
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
⊢ ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) < ⊤
[PROOFSTEP]
rw [lintegral_eq_lintegral_meas_le volume h_pos h_meas]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
⊢ ∫⁻ (t : ℝ) in Ioi 0, ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} < ⊤
[PROOFSTEP]
have h_int : ∀ t, 0 < t → volume {a : E | t ≤ (1 + ‖a‖) ^ (-r)} = volume (Metric.closedBall (0 : E) (t ^ (-r⁻¹) - 1)) :=
  fun t ht ↦ by
  congr 1
  ext x
  simp only [mem_setOf_eq, mem_closedBall_zero_iff]
  exact le_rpow_one_add_norm_iff_norm_le hr (mem_Ioi.mp ht) x
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
t : ℝ
ht : 0 < t
⊢ ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
t : ℝ
ht : 0 < t
⊢ {a | t ≤ (1 + ‖a‖) ^ (-r)} = Metric.closedBall 0 (t ^ (-r⁻¹) - 1)
[PROOFSTEP]
ext x
[GOAL]
case e_a.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
t : ℝ
ht : 0 < t
x : E
⊢ x ∈ {a | t ≤ (1 + ‖a‖) ^ (-r)} ↔ x ∈ Metric.closedBall 0 (t ^ (-r⁻¹) - 1)
[PROOFSTEP]
simp only [mem_setOf_eq, mem_closedBall_zero_iff]
[GOAL]
case e_a.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
t : ℝ
ht : 0 < t
x : E
⊢ t ≤ (1 + ‖x‖) ^ (-r) ↔ ‖x‖ ≤ t ^ (-r⁻¹) - 1
[PROOFSTEP]
exact le_rpow_one_add_norm_iff_norm_le hr (mem_Ioi.mp ht) x
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
⊢ ∫⁻ (t : ℝ) in Ioi 0, ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} < ⊤
[PROOFSTEP]
rw [set_lintegral_congr_fun measurableSet_Ioi (eventually_of_forall h_int)]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
⊢ ∫⁻ (x : ℝ) in Ioi 0, ↑↑volume (Metric.closedBall 0 (x ^ (-r⁻¹) - 1)) < ⊤
[PROOFSTEP]
set f := fun t : ℝ ↦ volume (Metric.closedBall (0 : E) (t ^ (-r⁻¹) - 1))
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
⊢ lintegral (Measure.restrict volume (Ioi 0)) f < ⊤
[PROOFSTEP]
set mB :=
  volume
    (Metric.ball (0 : E) 1)
      -- the next two inequalities are in fact equalities but we don't need that
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
⊢ lintegral (Measure.restrict volume (Ioi 0)) f < ⊤
[PROOFSTEP]
calc
  ∫⁻ t in Ioi 0, f t ≤ ∫⁻ t in Ioc 0 1 ∪ Ioi 1, f t := lintegral_mono_set Ioi_subset_Ioc_union_Ioi
  _ ≤ (∫⁻ t in Ioc 0 1, f t) + ∫⁻ t in Ioi 1, f t := (lintegral_union_le _ _ _)
  _ < ∞ := ENNReal.add_lt_top.2 ⟨?_, ?_⟩
[GOAL]
case calc_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
⊢ ∫⁻ (t : ℝ) in Ioc 0 1, f t < ⊤
[PROOFSTEP]
have h_int' : ∀ t ∈ Ioc (0 : ℝ) 1, f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB := fun t ht ↦
  by
  refine' volume.addHaar_closedBall (0 : E) _
  rw [sub_nonneg]
  exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos ht.1 ht.2 (by simp [hr.le])
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
t : ℝ
ht : t ∈ Ioc 0 1
⊢ f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB
[PROOFSTEP]
refine' volume.addHaar_closedBall (0 : E) _
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
t : ℝ
ht : t ∈ Ioc 0 1
⊢ 0 ≤ t ^ (-r⁻¹) - 1
[PROOFSTEP]
rw [sub_nonneg]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
t : ℝ
ht : t ∈ Ioc 0 1
⊢ 1 ≤ t ^ (-r⁻¹)
[PROOFSTEP]
exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos ht.1 ht.2 (by simp [hr.le])
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
t : ℝ
ht : t ∈ Ioc 0 1
⊢ -r⁻¹ ≤ 0
[PROOFSTEP]
simp [hr.le]
[GOAL]
case calc_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
h_int' : ∀ (t : ℝ), t ∈ Ioc 0 1 → f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB
⊢ ∫⁻ (t : ℝ) in Ioc 0 1, f t < ⊤
[PROOFSTEP]
rw [set_lintegral_congr_fun measurableSet_Ioc (ae_of_all _ h_int'), lintegral_mul_const' _ _ measure_ball_lt_top.ne]
[GOAL]
case calc_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
h_int' : ∀ (t : ℝ), t ∈ Ioc 0 1 → f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB
⊢ (∫⁻ (a : ℝ) in Ioc 0 1, ENNReal.ofReal ((a ^ (-r⁻¹) - 1) ^ finrank ℝ E)) * ↑↑volume (Metric.ball 0 1) < ⊤
[PROOFSTEP]
exact ENNReal.mul_lt_top (finite_integral_rpow_sub_one_pow_aux (finrank ℝ E) hnr).ne measure_ball_lt_top.ne
[GOAL]
case calc_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
⊢ ∫⁻ (t : ℝ) in Ioi 1, f t < ⊤
[PROOFSTEP]
have h_int'' : ∀ t ∈ Ioi (1 : ℝ), f t = 0 := fun t ht => by
  simp only [closedBall_rpow_sub_one_eq_empty_aux E hr ht, measure_empty]
    -- The integral over the constant zero function is finite:
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
t : ℝ
ht : t ∈ Ioi 1
⊢ f t = 0
[PROOFSTEP]
simp only [closedBall_rpow_sub_one_eq_empty_aux E hr ht, measure_empty]
  -- The integral over the constant zero function is finite:
[GOAL]
case calc_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
h_int'' : ∀ (t : ℝ), t ∈ Ioi 1 → f t = 0
⊢ ∫⁻ (t : ℝ) in Ioi 1, f t < ⊤
[PROOFSTEP]
rw [set_lintegral_congr_fun measurableSet_Ioi (ae_of_all volume <| h_int''), lintegral_const 0, zero_mul]
[GOAL]
case calc_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
h_int'' : ∀ (t : ℝ), t ∈ Ioi 1 → f t = 0
⊢ 0 < ⊤
[PROOFSTEP]
exact WithTop.zero_lt_top
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ Integrable fun x => (1 + ‖x‖) ^ (-r)
[PROOFSTEP]
constructor
[GOAL]
case left
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ AEStronglyMeasurable (fun x => (1 + ‖x‖) ^ (-r)) volume
[PROOFSTEP]
exact ((measurable_norm.const_add _).pow_const _).aestronglyMeasurable
[GOAL]
case right
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ HasFiniteIntegral fun x => (1 + ‖x‖) ^ (-r)
[PROOFSTEP]
have : (∫⁻ a : E, ‖(1 + ‖a‖) ^ (-r)‖₊) = ∫⁻ a : E, ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) :=
  lintegral_nnnorm_eq_of_nonneg fun _ => rpow_nonneg_of_nonneg (by positivity) _
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
x✝ : E
⊢ 0 ≤ 1 + ‖x✝‖
[PROOFSTEP]
positivity
[GOAL]
case right
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
this : ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ (-r)‖₊ = ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r))
⊢ HasFiniteIntegral fun x => (1 + ‖x‖) ^ (-r)
[PROOFSTEP]
rw [HasFiniteIntegral, this]
[GOAL]
case right
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
this : ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ (-r)‖₊ = ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r))
⊢ ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) < ⊤
[PROOFSTEP]
exact finite_integral_one_add_norm hnr
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ Integrable fun x => (1 + ‖x‖ ^ 2) ^ (-r / 2)
[PROOFSTEP]
have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
⊢ Integrable fun x => (1 + ‖x‖ ^ 2) ^ (-r / 2)
[PROOFSTEP]
refine ((integrable_one_add_norm hnr).const_mul <| (2 : ℝ) ^ (r / 2)).mono' ?_ (eventually_of_forall fun x => ?_)
[GOAL]
case refine_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
⊢ AEStronglyMeasurable (fun x => (1 + ‖x‖ ^ 2) ^ (-r / 2)) volume
[PROOFSTEP]
exact (((measurable_id.norm.pow_const _).const_add _).pow_const _).aestronglyMeasurable
[GOAL]
case refine_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
x : E
⊢ ‖(1 + ‖x‖ ^ 2) ^ (-r / 2)‖ ≤ 2 ^ (r / 2) * (1 + ‖x‖) ^ (-r)
[PROOFSTEP]
refine (abs_of_pos ?_).trans_le (rpow_neg_one_add_norm_sq_le x hr)
[GOAL]
case refine_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
x : E
⊢ 0 < (1 + ‖x‖ ^ 2) ^ (-r / 2)
[PROOFSTEP]
positivity
