awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
h_int :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
    ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ (-(r⁻¹ * (↑n : ℝ)))) (Ioc 0 1) volume
have rw : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-(r⁻¹ * (↑n : ℝ)))) volume 0 1
Tactic: rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
h_int :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
    ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ (-(r⁻¹ * (↑n : ℝ)))) volume 0 1
have h : -1 < -(r⁻¹ * (↑n : ℝ))
Tactic: apply intervalIntegral.intervalIntegrable_rpow'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
h_int :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
    ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
⊢ -1 < -(r⁻¹ * (↑n : ℝ))
have h : r⁻¹ * (↑n : ℝ) < 1
Tactic: rwa [neg_lt_neg_iff, inv_mul_lt_iff₀' hr, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
r : ℝ
n : ℕ
hnr : (↑n : ℝ) < r
hr : 0 < r
h_int :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioc 0 1) x),
    ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * (↑n : ℝ))))
h : r⁻¹ * (↑n : ℝ) < 1
⊢ -1 < -(r⁻¹ * (↑n : ℝ))
have h₁ : (↑n : ℝ) < 1 * r
Tactic: rwa [neg_lt_neg_iff, inv_mul_lt_iff₀' hr, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
⊢ ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ < ∞
have hr : 0 < r
Tactic: have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
⊢ ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ < ∞
have h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
Tactic: have h_meas : Measurable fun ω : E => (1 + ‖ω‖) ^ (-r) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
⊢ ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ < ∞
have h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
Tactic: have h_pos : ∀ x : E, 0 ≤ (1 + ‖x‖) ^ (-r) := fun x ↦ by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
⊢ ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) ∂μ < ∞
have rw : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} < ∞
Tactic: rw [lintegral_eq_lintegral_meas_le μ (Eventually.of_forall h_pos) h_meas.aemeasurable]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
t : ℝ
ht : 0 < t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) : ℝ≥0∞)
have h : Eq.{u_1 + 1} (α := Set E) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
t : ℝ
ht : 0 < t
⊢ Eq.{u_1 + 1} (α := Set E) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
have h : ∀ (x : E),
  Membership.mem (γ := Set E) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} x ↔
    Membership.mem (γ := Set E) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
t : ℝ
ht : 0 < t
x : E
⊢ Membership.mem (γ := Set E) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} x ↔
    Membership.mem (γ := Set E) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) x
have h : t ≤ (1 + ‖x‖) ^ (-r) ↔ ‖x‖ ≤ t ^ (-r⁻¹) - 1
Tactic: simp only [mem_setOf_eq, mem_closedBall_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
⊢ ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} < ∞
have h_int : ∀ (t : ℝ),
  0 < t →
    Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) : ℝ≥0∞)
Tactic: have h_int : ∀ t, 0 < t → μ {a : E | t ≤ (1 + ‖a‖) ^ (-r)} =
      μ (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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int :
  ∀ (t : ℝ),
    0 < t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) : ℝ≥0∞)
⊢ ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} < ∞
have rw : ∫⁻ (x : ℝ) in Ioi 0, (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (x ^ (-r⁻¹) - 1)) ∂volume < ∞
Tactic: rw [setLIntegral_congr_fun measurableSet_Ioi h_int]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int :
  ∀ (t : ℝ),
    0 < t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) : ℝ≥0∞)
f : (t : ℝ) → ℝ≥0∞ := fun (t : ℝ) ↦ (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1)
⊢ lintegral (m := measurableSpace) (Measure.restrict volume (Ioi 0)) f < ∞
have calc_1 : ∫⁻ (t : ℝ) in Ioc 0 1, f t < ∞
Tactic: 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 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int :
  ∀ (t : ℝ),
    0 < t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) : ℝ≥0∞)
f : (t : ℝ) → ℝ≥0∞ := fun (t : ℝ) ↦ (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1)
calc_1 : ∫⁻ (t : ℝ) in Ioc 0 1, f t < ∞
⊢ lintegral (m := measurableSpace) (Measure.restrict volume (Ioi 0)) f < ∞
have calc_2 : ∫⁻ (t : ℝ) in Ioi 1, f t < ∞
Tactic: 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 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int :
  ∀ (t : ℝ),
    0 < t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) : ℝ≥0∞)
f : (t : ℝ) → ℝ≥0∞ := fun (t : ℝ) ↦ (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
⊢ f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB
have refine : 0 ≤ t ^ (-r⁻¹) - 1
Tactic: refine μ.addHaar_closedBall (0 : E) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int :
  ∀ (t : ℝ),
    0 < t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) : ℝ≥0∞)
f : (t : ℝ) → ℝ≥0∞ := fun (t : ℝ) ↦ (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
⊢ 0 ≤ t ^ (-r⁻¹) - 1
have rw : 1 ≤ t ^ (-r⁻¹)
Tactic: rw [sub_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int :
  ∀ (t : ℝ),
    0 < t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) : ℝ≥0∞)
f : (t : ℝ) → ℝ≥0∞ := fun (t : ℝ) ↦ (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1)
⊢ ∫⁻ (t : ℝ) in Ioc 0 1, f t < ∞
have h_int' : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioc 0 1) t → f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB
Tactic: have h_int' : ∀ t ∈ Ioc (0 : ℝ) 1,
        f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB := fun t ht ↦ by
      refine μ.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])
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int :
  ∀ (t : ℝ),
    0 < t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) : ℝ≥0∞)
f : (t : ℝ) → ℝ≥0∞ := fun (t : ℝ) ↦ (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1)
h_int' : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioc 0 1) t → f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB
⊢ ∫⁻ (t : ℝ) in Ioc 0 1, f t < ∞
have calc_1 : HMul.hMul (β := ℝ≥0∞) (∫⁻ (a : ℝ) in Ioc 0 1, ENNReal.ofReal ((a ^ (-r⁻¹) - 1) ^ finrank ℝ E) ∂volume)
    ((μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1) : ℝ≥0∞) <
  ∞
Tactic: rw [setLIntegral_congr_fun measurableSet_Ioc h_int',
      lintegral_mul_const' _ _ measure_ball_lt_top.ne]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int :
  ∀ (t : ℝ),
    0 < t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) : ℝ≥0∞)
f : (t : ℝ) → ℝ≥0∞ := fun (t : ℝ) ↦ (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1)
⊢ ∫⁻ (t : ℝ) in Ioi 1, f t < ∞
have h_int'' : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 1) t → f t = 0
Tactic: have h_int'' : ∀ t ∈ Ioi (1 : ℝ), f t = 0 := fun t ht => by
      simp only [f, closedBall_rpow_sub_one_eq_empty_aux E hr ht, measure_empty]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
h_meas : Measurable (β := ℝ) fun (ω : E) ↦ (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int :
  ∀ (t : ℝ),
    0 < t →
      Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {a : E | t ≤ (1 + ‖a‖) ^ (-r)} : ℝ≥0∞)
        ((μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1)) : ℝ≥0∞)
f : (t : ℝ) → ℝ≥0∞ := fun (t : ℝ) ↦ (μ : (a : Set E) → ℝ≥0∞) (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) (Metric.ball 0 1)
h_int'' : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 1) t → f t = 0
⊢ ∫⁻ (t : ℝ) in Ioi 1, f t < ∞
have calc_2 : LT.lt (α := ℝ≥0∞) 0 ∞
Tactic: rw [setLIntegral_congr_fun measurableSet_Ioi h_int'', lintegral_const 0,
      zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-r)) μ
have left : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-r)) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
left : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-r)) μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-r)) μ
have right : HasFiniteIntegral (ε := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-r)) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-r)) μ
have this : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-r)‖ₑ ∂μ = ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ
Tactic: have : (∫⁻ a : E, ‖(1 + ‖a‖) ^ (-r)‖ₑ ∂μ) = ∫⁻ a : E, ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ :=
    lintegral_enorm_of_nonneg fun _ => rpow_nonneg (by positivity) _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
this : ∫⁻ (a : E), ‖(1 + ‖a‖) ^ (-r)‖ₑ ∂μ = ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : E) ↦ (1 + ‖x‖) ^ (-r)) μ
have right : ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ∂μ < ∞
Tactic: rw [hasFiniteIntegral_iff_enorm, this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)) μ
have hr : 0 < r
Tactic: have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)) μ
have refine_1 : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)) μ
Tactic: refine ((integrable_one_add_norm hnr).const_mul <| (2 : ℝ) ^ (r / 2)).mono'
    ?_ (Eventually.of_forall fun x => ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)) μ
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)) μ
have refine_2 : ∀ (x : E), ‖(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)‖ ≤ HPow.hPow (α := ℝ) 2 (r / 2) * (1 + ‖x‖) ^ (-r)
Tactic: refine ((integrable_one_add_norm hnr).const_mul <| (2 : ℝ) ^ (r / 2)).mono'
    ?_ (Eventually.of_forall fun x => ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.JapaneseBracket (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
r : ℝ
hnr : (↑(finrank ℝ E) : ℝ) < r
hr : 0 < r
x : E
⊢ ‖(1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)‖ ≤ HPow.hPow (α := ℝ) 2 (r / 2) * (1 + ‖x‖) ^ (-r)
have refine_2 : 0 < (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-r / 2)
Tactic: refine (abs_of_pos ?_).trans_le (rpow_neg_one_add_norm_sq_le x hr)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
⊢ logb 0 = 0
have h : ∀ (x : ℝ), logb 0 x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
x : ℝ
⊢ logb 0 x = 0 x
have h : Eq (α := ℝ) 0 (0 x)
Tactic: rw [logb_zero_left, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
x : ℝ
h : Eq (α := ℝ) 0 (0 x)
⊢ logb 0 x = 0 x
have h₁ : Eq (α := ℝ) 0 0
Tactic: rw [logb_zero_left, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
⊢ logb 1 = 0
have h : ∀ (x : ℝ), logb 1 x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
x : ℝ
⊢ logb 1 x = 0 x
have h : Eq (α := ℝ) 0 (0 x)
Tactic: rw [logb_one_left, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
x : ℝ
h : Eq (α := ℝ) 0 (0 x)
⊢ logb 1 x = 0 x
have h₁ : Eq (α := ℝ) 0 0
Tactic: rw [logb_one_left, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
⊢ logb |b| x = logb b x
have rw : log x / log |b| = logb b x
Tactic: rw [logb, logb, log_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
rw : log x / log |b| = logb b x
⊢ logb |b| x = logb b x
have rw₁ : log x / log |b| = log x / log b
Tactic: rw [logb, logb, log_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
rw : log x / log |b| = logb b x
rw₁ : log x / log |b| = log x / log b
⊢ logb |b| x = logb b x
have rw₂ : log x / log b = log x / log b
Tactic: rw [logb, logb, log_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
⊢ logb b |x| = logb b x
have rw : log |x| / log b = logb b x
Tactic: rw [logb, logb, log_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
rw : log |x| / log b = logb b x
⊢ logb b |x| = logb b x
have rw₁ : log |x| / log b = log x / log b
Tactic: rw [logb, logb, log_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
rw : log |x| / log b = logb b x
rw₁ : log |x| / log b = log x / log b
⊢ logb b |x| = logb b x
have rw₂ : log x / log b = log x / log b
Tactic: rw [logb, logb, log_abs]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b : ℝ
⊢ logb (-b) = logb b
have h : ∀ (x : ℝ), logb (-b) x = logb b x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
⊢ logb (-b) x = logb b x
have h : logb (-b) x = logb |b| x
Tactic: rw [← logb_abs_base b x, ← logb_abs_base (-b) x, abs_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Log.Base (goal)
Goal:
b x : ℝ
h : logb (-b) x = logb |b| x
⊢ logb (-b) x = logb b x
have h₁ : logb |(-b)| x = logb |b| x
Tactic: rw [← logb_abs_base b x, ← logb_abs_base (-b) x, abs_neg]