-- Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean
theorem integrable_one_add_norm {r : ℝ} (hnr : (finrank ℝ E : ℝ) < r) :
    Integrable (fun x ↦ (1 + ‖x‖) ^ (-r)) μ

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
x✝ : E
⊢ 0 ≤ 1 + ‖x✝‖

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ Measurable fun x => (1 + ‖x‖) ^ (-r)

Tactic:
fun_prop

Result:
no goals

Proof state:
case left
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ AEStronglyMeasurable (fun x => (1 + ‖x‖) ^ (-r)) μ

Tactic:
apply Measurable.aestronglyMeasurable (by fun_prop)

Result:
no goals

Proof state:
case right
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
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)) ∂μ < ⊤

Tactic:
exact finite_integral_one_add_norm hnr

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ Integrable (fun x => (1 + ‖x‖) ^ (-r)) μ

Tactic:
constructor

Result:
case left
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ AEStronglyMeasurable (fun x => (1 + ‖x‖) ^ (-r)) μ

case right
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ HasFiniteIntegral (fun x => (1 + ‖x‖) ^ (-r)) μ

Proof state:
case right
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
this : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-r)‖ₑ ∂μ = ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ
⊢ HasFiniteIntegral (fun x => (1 + ‖x‖) ^ (-r)) μ

Tactic:
rw [hasFiniteIntegral_iff_enorm, this]

Result:
case right
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
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)) ∂μ < ⊤

Proof state:
case right
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ HasFiniteIntegral (fun x => (1 + ‖x‖) ^ (-r)) μ

Tactic:
have : (∫⁻ a : E, ‖(1 + ‖a‖) ^ (-r)‖ₑ ∂μ) = ∫⁻ a : E, ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ :=
  lintegral_enorm_of_nonneg fun _ => rpow_nonneg (by positivity) _

Result:
case right
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
r : ℝ
hnr : ↑(finrank ℝ E) < r
this : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-r)‖ₑ ∂μ = ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ
⊢ HasFiniteIntegral (fun x => (1 + ‖x‖) ^ (-r)) μ