awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ioi c
⊢ x ^ a.re = ‖(↑x : ℂ) ^ a‖
have rw : x ^ a.re = x ^ a.re
Tactic: rw [Complex.norm_cpow_eq_rpow_re_of_pos (hc.trans hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ a) (Ioi c) volume
have refine : AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ a)
  (Measure.restrict volume (Ioi c))
Tactic: refine (integrable_norm_iff ?_).mp <| integrableOn_Ioi_norm_cpow_of_lt ha hc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ a)
    (Measure.restrict volume (Ioi c))
have refine : ∀ (t : ℝ) (ht : t ∈ Ioi c), ContinuousWithinAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ a) (Ioi c) t
Tactic: refine ContinuousOn.aestronglyMeasurable (fun t ht ↦ ?_) measurableSet_Ioi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ s‖) (Ioi t) volume ↔ s.re < -1
have refine : ∀ (h : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ s‖) (Ioi t) volume),
  s.re < -1
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ integrableOn_Ioi_norm_cpow_of_lt h ht⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ s‖) (Ioi t) volume
⊢ s.re < -1
have refine : ∀ (a : ℝ) (ha : a ∈ Ioi t), ‖(↑a : ℂ) ^ s‖ = a ^ s.re
Tactic: refine (integrableOn_Ioi_rpow_iff ht).mp <| h.congr_fun (fun a ha ↦ ?_) measurableSet_Ioi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
h : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ s‖) (Ioi t) volume
a : ℝ
ha : a ∈ Ioi t
⊢ ‖(↑a : ℂ) ^ s‖ = a ^ s.re
have rw : a ^ s.re = a ^ s.re
Tactic: rw [Complex.norm_cpow_eq_rpow_re_of_pos (ht.trans ha)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s * (↑x : ℂ) ^ (s - 1)) (Ioi t) volume
have refine : (s - 1).re < -1
Tactic: refine (integrableOn_Ioi_cpow_of_lt ?_ ht).const_mul _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
⊢ (s - 1).re < -1
have rwa : s.re - Complex.re 1 < -1
Tactic: rwa [Complex.sub_re, Complex.one_re, sub_lt_iff_lt_add, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
rwa : s.re - Complex.re 1 < -1
⊢ (s - 1).re < -1
have rwa₁ : s.re - 1 < -1
Tactic: rwa [Complex.sub_re, Complex.one_re, sub_lt_iff_lt_add, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
rwa : s.re - Complex.re 1 < -1
rwa₁ : s.re - 1 < -1
⊢ (s - 1).re < -1
have rwa₂ : s.re < HAdd.hAdd (α := ℝ) (-1) 1
Tactic: rwa [Complex.sub_re, Complex.one_re, sub_lt_iff_lt_add, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (hypothesis)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi t) volume
have h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s * (↑x : ℂ) ^ (s - 1)) (Ioi t) volume
Tactic: have h : IntegrableOn (fun x : ℝ ↦ s * x ^ (s - 1)) (Set.Ioi t) := by
    refine (integrableOn_Ioi_cpow_of_lt ?_ ht).const_mul _
    rwa [Complex.sub_re, Complex.one_re, sub_lt_iff_lt_add, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s * (↑x : ℂ) ^ (s - 1)) (Ioi t) volume
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi t) volume
have refine : ∀ (x : ℝ) (hx : x ∈ Ioi t), s * (↑x : ℂ) ^ (s - 1) = deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) x
Tactic: refine h.congr_fun (fun x hx ↦ ?_) measurableSet_Ioi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re < 0
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s * (↑x : ℂ) ^ (s - 1)) (Ioi t) volume
x : ℝ
hx : x ∈ Ioi t
⊢ s * (↑x : ℂ) ^ (s - 1) = deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) x
have rw : s * (↑x : ℂ) ^ (s - 1) = s * (↑x : ℂ) ^ (s - 1)
Tactic: rw [Complex.deriv_ofReal_cpow_const (ht.trans hx).ne' (fun h ↦ (Complex.zero_re ▸ h ▸ hs).false)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re ≤ 0
x : ℝ
hx : x ∈ Ioi t
⊢ deriv (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ s‖) x = s.re * x ^ (s.re - 1)
have rw : s.re * x ^ (s.re - 1) = s.re * x ^ (s.re - 1)
Tactic: rw [deriv_norm_ofReal_cpow _ (ht.trans hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re ≤ 0
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (deriv fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ s‖) (Ioi t) volume
have rw : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume
Tactic: rw [integrableOn_congr_fun (fun x hx ↦ by
    rw [deriv_norm_ofReal_cpow _ (ht.trans hx)]) measurableSet_Ioi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re ≤ 0
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume
have inl : ∀ (hs : s.re = 0),
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume
Tactic: obtain hs | hs := eq_or_lt_of_le hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs : s.re ≤ 0
inl :
  ∀ (hs : s.re = 0),
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume
have inr : ∀ (hs : s.re < 0),
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume
Tactic: obtain hs | hs := eq_or_lt_of_le hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs_1 : s.re ≤ 0
hs : s.re = 0
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume
have inl : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ 0) (Ioi t) volume
Tactic: simp_rw [hs, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs_1 : s.re ≤ 0
hs : s.re < 0
⊢ s.re - 1 < -1
have rwa : s.re < HAdd.hAdd (α := ℝ) (-1) 1
Tactic: rwa [sub_lt_iff_lt_add, neg_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (hypothesis)
Goal:
s : ℂ
t : ℝ
ht : 0 < t
hs_1 : s.re ≤ 0
hs : s.re < 0
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ s.re * x ^ (s.re - 1)) (Ioi t) volume
have hs₁ : s.re - 1 < -1
Tactic: replace hs : s.re - 1 < -1 := by rwa [sub_lt_iff_lt_add, neg_add_cancel]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 0) volume
⊢ False
have inl : ∀ (hs : s.re ≤ -1), False
Tactic: rcases le_or_gt s.re (-1) with hs | hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℂ
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 0) volume
inl : ∀ (hs : s.re ≤ -1), False
⊢ False
have inr : ∀ (hs : -1 < s.re), False
Tactic: rcases le_or_gt s.re (-1) with hs | hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (hypothesis)
Goal:
s : ℂ
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 0) volume
hs : s.re ≤ -1
⊢ False
have this : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 1) volume
Tactic: have : IntegrableOn (fun x : ℝ ↦ (x : ℂ) ^ s) (Ioo (0 : ℝ) 1) :=
      h.mono Ioo_subset_Ioi_self le_rfl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (hypothesis)
Goal:
s : ℂ
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 0) volume
hs : s.re ≤ -1
this : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioo 0 1) volume
⊢ False
have this₁ : -1 < s.re
Tactic: rw [integrableOn_Ioo_cpow_iff zero_lt_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (hypothesis)
Goal:
s : ℂ
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 0) volume
hs : -1 < s.re
⊢ False
have this : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 1) volume
Tactic: have : IntegrableOn (fun x : ℝ ↦ (x : ℂ) ^ s) (Ioi 1) :=
      h.mono (Ioi_subset_Ioi zero_le_one) le_rfl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (hypothesis)
Goal:
s : ℂ
h : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 0) volume
hs : -1 < s.re
this : IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑x : ℂ) ^ s) (Ioi 1) volume
⊢ False
have this₁ : s.re < -1
Tactic: rw [integrableOn_Ioi_cpow_iff zero_lt_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (t : ℝ) ↦ (↑t : ℂ) ^ a) =
    -(↑c : ℂ) ^ (a + 1) / (a + 1)
have c₁ : Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in c..id i, (↑x : ℂ) ^ a) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
Tactic: refine
    tendsto_nhds_unique
      (intervalIntegral_tendsto_integral_Ioi c (integrableOn_Ioi_cpow_of_lt ha hc) tendsto_id) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this :
  Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in c..id i, (↑x : ℂ) ^ a) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
have refine : ∀ (x : ℝ) (hx : 0 < x),
  ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1) = (fun (i : ℝ) ↦ (∫ (x : ℝ) in c..id i, (↑x : ℂ) ^ a : ℂ)) x
Tactic: refine this.congr' ((eventually_gt_atTop 0).mp (Eventually.of_forall fun x hx => ?_))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this :
  Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1) = ∫ (x : ℝ) in c..id x, (↑x : ℂ) ^ a
have rw : -1 < a.re ∨ a ≠ -1 ∧ 0 ∉ uIcc c (id x)
Tactic: rw [integral_cpow, id]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this :
  Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ -1 < a.re ∨ a ≠ -1 ∧ 0 ∉ uIcc c (id x)
have refine : a ≠ -1
Tactic: refine Or.inr ⟨?_, notMem_uIcc_of_lt hc hx⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
this :
  Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
x : ℝ
hx : 0 < x
⊢ a ≠ -1
have apply_fun : a.re ≠ Complex.re (-1)
Tactic: apply_fun Complex.re
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in c..id i, (↑x : ℂ) ^ a) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
have Tendsto : Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
Tactic: suffices
    Tendsto (fun x : ℝ => ((x : ℂ) ^ (a + 1) - (c : ℂ) ^ (a + 1)) / (a + 1)) atTop
      (𝓝 <| -c ^ (a + 1) / (a + 1)) by
    refine this.congr' ((eventually_gt_atTop 0).mp (Eventually.of_forall fun x hx => ?_))
    dsimp only
    rw [integral_cpow, id]
    refine Or.inr ⟨?_, notMem_uIcc_of_lt hc hx⟩
    apply_fun Complex.re
    rw [Complex.neg_re, Complex.one_re]
    exact ha.ne
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ Tendsto (fun (x : ℝ) ↦ ((↑x : ℂ) ^ (a + 1) - (↑c : ℂ) ^ (a + 1)) / (a + 1)) atTop (𝓝 (-(↑c : ℂ) ^ (a + 1) / (a + 1)))
have simp_rw : Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) ^ (a + 1) / (a + 1) - (↑c : ℂ) ^ (a + 1) / (a + 1)) atTop
  (𝓝 (0 / (a + 1) - (↑c : ℂ) ^ (a + 1) / (a + 1)))
Tactic: simp_rw [← zero_sub, sub_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ Tendsto (fun (x : ℝ) ↦ (↑x : ℂ) ^ (a + 1) / (a + 1) - (↑c : ℂ) ^ (a + 1) / (a + 1)) atTop
    (𝓝 (0 / (a + 1) - (↑c : ℂ) ^ (a + 1) / (a + 1)))
have refine : Tendsto (β := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (a + 1)) atTop (𝓝 0)
Tactic: refine (Tendsto.div_const ?_ _).sub_const _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ Tendsto (β := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (a + 1)) atTop (𝓝 0)
have rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (a + 1)‖) atTop (𝓝 0)
Tactic: rw [tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ 0 < -(a.re + 1)
have linarith : -(a.re + 1) ≤ 0 → a.re - -1 + (-(a.re + 1) - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (a + 1)‖) atTop (𝓝 0)
have linarith : ∀ (x : ℝ) (hx : 0 < x), x ^ (- -(a.re + 1)) = (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (a + 1)‖) x
Tactic: refine
    (tendsto_rpow_neg_atTop (by linarith : 0 < -(a.re + 1))).congr'
      ((eventually_gt_atTop 0).mp (Eventually.of_forall fun x hx => ?_))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : 0 < x
simp_rw simp_rw₁ : x ^ (- -(a.re + 1)) = ‖(↑x : ℂ) ^ (a + 1)‖
⊢ x ^ (- -(a.re + 1)) = (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (a + 1)‖) x
have simp_rw₂ : x ^ (a.re + 1) = ‖(↑x : ℂ) ^ (a + 1)‖
Tactic: simp_rw [neg_neg, Complex.norm_cpow_eq_rpow_re_of_pos hx, Complex.add_re, Complex.one_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : 0 < x
simp_rw simp_rw₁ : x ^ (- -(a.re + 1)) = ‖(↑x : ℂ) ^ (a + 1)‖
simp_rw₂ : x ^ (a.re + 1) = ‖(↑x : ℂ) ^ (a + 1)‖
⊢ x ^ (- -(a.re + 1)) = (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (a + 1)‖) x
have simp_rw₃ : x ^ (a.re + 1) = x ^ (a + 1).re
Tactic: simp_rw [neg_neg, Complex.norm_cpow_eq_rpow_re_of_pos hx, Complex.add_re, Complex.one_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : 0 < x
simp_rw simp_rw₁ : x ^ (- -(a.re + 1)) = ‖(↑x : ℂ) ^ (a + 1)‖
simp_rw₂ : x ^ (a.re + 1) = ‖(↑x : ℂ) ^ (a + 1)‖
simp_rw₃ : x ^ (a.re + 1) = x ^ (a + 1).re
⊢ x ^ (- -(a.re + 1)) = (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (a + 1)‖) x
have simp_rw₄ : x ^ (a.re + 1) = x ^ (a.re + Complex.re 1)
Tactic: simp_rw [neg_neg, Complex.norm_cpow_eq_rpow_re_of_pos hx, Complex.add_re, Complex.one_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (1 + HPow.hPow (β := ℕ) x 2)⁻¹) volume
have suffices : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (1 + HPow.hPow (β := ℕ) ‖x‖ 2) ^ (-2 / 2)) volume
Tactic: suffices Integrable fun (x : ℝ) ↦ (1 + ‖x‖ ^ 2) ^ ((-2 : ℝ) / 2) by simpa [rpow_neg_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume a b
have suffices : ∀ (c : ℝ), IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
Tactic: suffices ∀ c : ℝ, IntervalIntegrable (fun x => x ^ r) volume 0 c by
    exact IntervalIntegrable.trans (this a).symm (this b)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
have rw : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ x ^ r) (Ioc 0 c) volume
Tactic: rw [intervalIntegrable_iff, uIoc_of_le hc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioo 0 c
⊢ HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
have h₁ : x ^ r = (r + 1) * x ^ (r + 1 - 1) / (r + 1)
Tactic: convert! (Real.hasDerivAt_rpow_const (p := r + 1) (Or.inl hx.1.ne')).div_const (r + 1) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
x : ℝ
hx : x ∈ Ioo 0 c
⊢ r + 1 ≠ 0
have linarith : r + 1 = 0 → -1 - r + (r + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ x ^ r) (Ioc 0 c) volume
have hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
Tactic: have hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun x : ℝ => x ^ (r + 1) / (r + 1)) (x ^ r) x := by
      intro x hx
      convert! (Real.hasDerivAt_rpow_const (p := r + 1) (Or.inl hx.1.ne')).div_const (r + 1) using 1
      simp [(by linarith : r + 1 ≠ 0)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ x ^ r) (Ioc 0 c) volume
have apply : ∀ x ∈ Ioo 0 c, 0 ≤ x ^ r
Tactic: apply integrableOn_deriv_of_nonneg _ hderiv
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
apply : ∀ x ∈ Ioo 0 c, 0 ≤ x ^ r
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ x ^ r) (Ioc 0 c) volume
have apply₁ : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (Icc 0 c)
Tactic: apply integrableOn_deriv_of_nonneg _ hderiv
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (Icc 0 c)
have refine : ∀ x ∈ Icc 0 c, id x ≠ 0 ∨ 0 ≤ r + 1
Tactic: refine (continuousOn_id.rpow_const ?_).div_const _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
h_1 : x ∈ Icc 0 c
⊢ id x ≠ 0 ∨ 0 ≤ r + 1
have h₁ : 0 ≤ r + 1
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
c : ℝ
hc : 0 ≤ c
hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun (x : ℝ) ↦ x ^ (r + 1) / (r + 1)) (x ^ r) x
x : ℝ
h_1 : x ∈ Icc 0 c
⊢ 0 ≤ r + 1
have linarith : r + 1 < 0 → -1 - r + (r + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
a b r : ℝ
h : -1 < r
⊢ ∀ (c : ℝ), IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
have this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
Tactic: have : ∀ c : ℝ, 0 ≤ c → IntervalIntegrable (fun x => x ^ r) volume 0 c := by
    intro c hc
    rw [intervalIntegrable_iff, uIoc_of_le hc]
    have hderiv : ∀ x ∈ Ioo 0 c, HasDerivAt (fun x : ℝ => x ^ (r + 1) / (r + 1)) (x ^ r) x := by
      intro x hx
      convert! (Real.hasDerivAt_rpow_const (p := r + 1) (Or.inl hx.1.ne')).div_const (r + 1) using 1
      simp [(by linarith : r + 1 ≠ 0)]
    apply integrableOn_deriv_of_nonneg _ hderiv
    · intro x hx; apply rpow_nonneg hx.1.le
    · refine (continuousOn_id.rpow_const ?_).div_const _; intro x _; right; linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
c : ℝ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
have inl : ∀ (hc : 0 ≤ c), IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
Tactic: rcases le_total 0 c with (hc | hc)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
c : ℝ
inl : ∀ (hc : 0 ≤ c), IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
have inr : ∀ (hc : c ≤ 0), IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
Tactic: rcases le_total 0 c with (hc | hc)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
have inr : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (-x) ^ r) volume 0 (-c)
Tactic: rw [IntervalIntegrable.iff_comp_neg, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (goal)
Goal:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ 0 ≤ -c
have linarith : -c < 0 → c - 0 + (-c - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.Basic (hypothesis)
Goal:
a b r : ℝ
h : -1 < r
this : ∀ (c : ℝ), 0 ≤ c → IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ x ^ r) volume 0 c
c : ℝ
hc : c ≤ 0
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (-x) ^ r) volume 0 (-c)
have m : IntervalIntegrable (HSMul.hSMul (β := ℝ → ℝ) (cos (r * π)) fun (x : ℝ) ↦ x ^ r) volume 0 (-c)
Tactic: have m := (this (-c) (by linarith)).smul (cos (r * π))