awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation (goal)
Goal:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * a * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + 2 * (↑π : ℂ) * b * (↑x : ℂ))
hCf : Continuous f
hFf : 𝓕 f = fun (x : ℝ) ↦ 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2)
h1 : 0 < ((↑π : ℂ) * a).re
h2 : 0 < ((↑π : ℂ) / a).re
f_bd : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
Ff_bd : IsBigO (F := ℝ) (cocompact ℝ) (𝓕 f) fun (x : ℝ) ↦ HPow.hPow (β := ℝ) |x| (-2)
⊢ 1 / a ^ (1 / 2) * ∑' (n : ℤ), cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑n : ℂ) + I * b) 2) =
    ∑' (n : ℤ),
      HMul.hMul (β := ℂ) (𝓕 f (↑n : ℝ)) ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
have h : Eq (α := ℂ) (∑' (x : ℤ), 1 / a ^ (1 / 2) * cexp (-(↑π : ℂ) / a * HPow.hPow (β := ℕ) ((↑x : ℂ) + I * b) 2))
  (∑' (n : ℤ),
    HMul.hMul (β := ℂ) (𝓕 f (↑n : ℝ)) ((fourier n : (a : AddCircle 1) → ℂ) (↑0 : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
Tactic: rw [← tsum_mul_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
c : ℝ
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) rexp (Iic c) volume
have integrableOn_Iic_of_intervalIntegral_norm_bounded : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Iic 0) y → ∫ (x : ℝ) in id y..c, ‖rexp x‖ ≤ rexp c
Tactic: refine
    integrableOn_Iic_of_intervalIntegral_norm_bounded (exp c) c
      (fun y => intervalIntegrable_exp.1) tendsto_id
      (eventually_of_mem (Iic_mem_atBot 0) fun y _ => ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
c y : ℝ
h : Membership.mem (γ := Set ℝ) (Iic 0) y
⊢ ∫ (x : ℝ) in id y..c, ‖rexp x‖ ≤ rexp c
have simp_rw : 0 ≤ rexp (id y)
Tactic: simp_rw [norm_of_nonneg (exp_pos _).le, integral_exp, sub_le_self_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
c : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic c)) fun (x : ℝ) ↦ rexp x) = rexp c
have _ : Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in id i..c, rexp x) atBot (𝓝 (rexp c))
Tactic: refine
    tendsto_nhds_unique
      (intervalIntegral_tendsto_integral_Iic _ (integrableOn_exp_Iic _) tendsto_id) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
c : ℝ
⊢ 𝓝 (rexp c) = 𝓝 (rexp c - 0)
have rw : 𝓝 (rexp c) = 𝓝 (rexp c)
Tactic: rw [sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
c : ℝ
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in id i..c, rexp x) atBot (𝓝 (rexp c))
have simp_rw : Tendsto (fun (i : ℝ) ↦ rexp c - rexp (id i)) atBot (𝓝 (rexp c - 0))
Tactic: simp_rw [integral_exp, show 𝓝 (exp c) = 𝓝 (exp c - 0) by rw [sub_zero]]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ))) (Ioi c) volume
have refine_1 : AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ)))
  (Measure.restrict volume (Ioi c))
Tactic: refine (integrable_norm_iff ?_).mp ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
refine_1 :
  AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ)))
    (Measure.restrict volume (Ioi c))
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ))) (Ioi c) volume
have refine_2 : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (a_1 : ℝ) ↦ ‖Complex.exp (a * (↑a_1 : ℂ))‖)
  (Measure.restrict volume (Ioi c))
Tactic: refine (integrable_norm_iff ?_).mp ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ)))
    (Measure.restrict volume (Ioi c))
have refine_1 : Continuous (Y := ℂ) fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ))
Tactic: apply Continuous.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (hypothesis)
Goal:
a : ℝ
ha : a < 0
c : ℝ
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (a * x)) (Ioi c) volume
have this : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (a_1 : ℝ) ↦ ‖Complex.exp ((↑a : ℂ) * (↑a_1 : ℂ))‖)
  (Measure.restrict volume (Ioi c))
Tactic: have := Integrable.norm <| integrableOn_exp_mul_complex_Ioi (a := a) (by simpa using ha) c
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (hypothesis)
Goal:
a : ℝ
ha : 0 < a
c : ℝ
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (a * x)) (Iic c) volume
have this : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (a_1 : ℝ) ↦ ‖Complex.exp ((↑a : ℂ) * (↑a_1 : ℂ))‖)
  (Measure.restrict volume (Iic c))
Tactic: have := Integrable.norm <| integrableOn_exp_mul_complex_Iic (a := a) (by simpa using ha) c
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (x : ℝ) ↦
      Complex.exp (a * (↑x : ℂ))) =
    -Complex.exp (a * (↑c : ℂ)) / a
have refine : Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in c..id i, Complex.exp (a * (↑x : ℂ))) atTop (𝓝 (-Complex.exp (a * (↑c : ℂ)) / a))
Tactic: refine tendsto_nhds_unique (intervalIntegral_tendsto_integral_Ioi c
    (integrableOn_exp_mul_complex_Ioi ha c) tendsto_id) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in c..id i, Complex.exp (a * (↑x : ℂ))) atTop (𝓝 (-Complex.exp (a * (↑c : ℂ)) / a))
have simp_rw : Tendsto (fun (i : ℝ) ↦ (Complex.exp (a * (↑i : ℂ)) - Complex.exp (a * (↑c : ℂ))) / a) atTop
  (𝓝 (-Complex.exp (a * (↑c : ℂ)) / a))
Tactic: simp_rw [integral_exp_mul_complex (c := a) (by aesop), id_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℂ
ha : a.re < 0
c : ℝ
⊢ Tendsto (fun (i : ℝ) ↦ (Complex.exp (a * (↑i : ℂ)) - Complex.exp (a * (↑c : ℂ))) / a) atTop
    (𝓝 (-Complex.exp (a * (↑c : ℂ)) / a))
have suffices : Tendsto (β := ℂ) (fun (x : ℝ) ↦ Complex.exp (a * (↑x : ℂ))) atTop (𝓝 0)
Tactic: suffices Tendsto (fun x : ℝ ↦ Complex.exp (a * x)) atTop (𝓝 0) by
    simpa using this.sub_const _ |>.div_const _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℝ
ha : a < 0
c : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (x : ℝ) ↦ rexp (a * x)) =
    -rexp (a * c) / a
have simp_rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (x : ℝ) ↦
    (RCLike.re : (a : ℂ) → ℝ) (Complex.exp ((↑a : ℂ) * (↑x : ℂ)))) =
  HDiv.hDiv (α := ℝ) (-(RCLike.re : (a : ℂ) → ℝ) (Complex.exp ((↑a : ℂ) * (↑c : ℂ))) : ℝ) a
Tactic: simp_rw [Real.exp, ← RCLike.re_to_complex, Complex.ofReal_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℝ
ha : a < 0
c : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (x : ℝ) ↦
      (RCLike.re : (a : ℂ) → ℝ) (Complex.exp ((↑a : ℂ) * (↑x : ℂ)))) =
    HDiv.hDiv (α := ℝ) (-(RCLike.re : (a : ℂ) → ℝ) (Complex.exp ((↑a : ℂ) * (↑c : ℂ))) : ℝ) a
have rw : @Integrable ℂ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ Complex.exp ((↑a : ℂ) * (↑x : ℂ)))
  (Measure.restrict volume (Ioi c))
Tactic: rw [integral_re, integral_exp_mul_complex_Ioi (by simpa using ha), RCLike.re_to_complex,
    RCLike.re_to_complex, Complex.div_ofReal_re, Complex.neg_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
⊢ HasDerivAt (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x
have h : (x + m) ^ a = 1 * (a + 1) * (id x + m) ^ (a + 1 - 1) / (a + 1)
Tactic: convert! (((hasDerivAt_id _).add_const _).rpow_const _).div_const _ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
h : (x + m) ^ a = 1 * (a + 1) * (id x + m) ^ (a + 1 - 1) / (a + 1)
⊢ HasDerivAt (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x
have convert_3 : id x + m ≠ 0 ∨ 1 ≤ a + 1
Tactic: convert! (((hasDerivAt_id _).add_const _).rpow_const _).div_const _ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
⊢ a + 1 ≠ 0
have linarith : a + 1 = 0 → a - -1 + -(a + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
⊢ id x + m ≠ 0 ∨ 1 ≤ a + 1
have convert_3 : id x + m ≠ 0
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
x : ℝ
hx : x ∈ Ici c
⊢ id x + m ≠ 0
have linarith : id x + m = 0 → -m - c + (id x + m - 0) + (c - x) + -(id x - x) = 0
Tactic: linarith [mem_Ici.mp hx, id_eq x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (hypothesis)
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (x + m) ^ a) (Ioi c) volume
have hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x
Tactic: have hd : ∀ x ∈ Ici c, HasDerivAt (fun t ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x := by
    intro x hx
    convert! (((hasDerivAt_id _).add_const _).rpow_const _).div_const _ using 1
    · simp [show a + 1 ≠ 0 by linarith]
    left; linarith [mem_Ici.mp hx, id_eq x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x
⊢ Tendsto (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
have rw : Tendsto (fun (t : ℝ) ↦ (t + m) ^ (- -(a + 1)) / - -(a + 1)) atTop (𝓝 (0 / - -(a + 1)))
Tactic: rw [← neg_neg (a + 1)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x
⊢ 0 < -(a + 1)
have linarith : -(a + 1) ≤ 0 → a - -1 + (-(a + 1) - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (hypothesis)
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (x + m) ^ a) (Ioi c) volume
have ht : Tendsto (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
Tactic: have ht : Tendsto (fun t ↦ ((t + m) ^ (a + 1)) / (a + 1)) atTop (nhds (0 / (a + 1))) := by
    rw [← neg_neg (a + 1)]
    exact (tendsto_rpow_neg_atTop (by linarith)).comp
      (tendsto_atTop_add_const_right _ m tendsto_id) |>.div_const _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a c m : ℝ
ha : a < -1
hc : -m < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x
ht_1 : Tendsto (fun (t : ℝ) ↦ (t + m) ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
t : ℝ
ht : t ∈ Ioi c
⊢ 0 ≤ t + m
have linarith : t + m < 0 → -m - c + (t + m - 0) + (c - t) = 0
Tactic: linarith [mem_Ioi.mp ht]
-- 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 < -1
have refine : ∀ (h : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume), s < -1
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ integrableOn_Ioi_rpow_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 < -1
have contrapose! : ∀ (h : -1 ≤ s), ¬IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (hypothesis)
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
⊢ False
have H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
Tactic: have H' : IntegrableOn (fun x ↦ x ^ s) (Ioi (max 1 t)) :=
    H.mono (Set.Ioi_subset_Ioi (le_max_right _ _)) le_rfl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ioi (max 1 t)) volume
have apply : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioi (max 1 t)), ‖a⁻¹‖ ≤ a ^ s
Tactic: apply H'.mono' measurable_inv.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioi (max 1 t)), ‖a⁻¹‖ ≤ a ^ s
have h₁ : ∀ (x : ℝ) (hx : x ∈ Ioi (max 1 t)), ‖x⁻¹‖ ≤ x ^ s
Tactic: filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (hypothesis)
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
x : ℝ
hx : x ∈ Ioi (max 1 t)
⊢ ‖x⁻¹‖ ≤ x ^ s
have x_one : 1 ≤ x
Tactic: have x_one : 1 ≤ x := ((le_max_left _ _).trans_lt (mem_Ioi.1 hx)).le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
x : ℝ
hx : x ∈ Ioi (max 1 t)
x_one : 1 ≤ x
⊢ ‖x⁻¹‖ ≤ x ^ s
have h₁ : x⁻¹ ≤ x ^ s
Tactic: simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (zero_le_one.trans x_one)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
x : ℝ
hx : x ∈ Ioi (max 1 t)
x_one : 1 ≤ x
⊢ x⁻¹ ≤ x ^ s
have h₁ : HPow.hPow (β := ℝ) x (-1) ≤ x ^ s
Tactic: rw [← Real.rpow_neg_one x]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (hypothesis)
Goal:
s t : ℝ
ht : 0 < t
h : -1 ≤ s
H : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi t) volume
H' : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max 1 t)) volume
⊢ False
have this : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x⁻¹) (Ioi (max 1 t)) volume
Tactic: have : IntegrableOn (fun x ↦ x⁻¹) (Ioi (max 1 t)) := by
    apply H'.mono' measurable_inv.aestronglyMeasurable
    filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx
    have x_one : 1 ≤ x := ((le_max_left _ _).trans_lt (mem_Ioi.1 hx)).le
    simp only [norm_inv, Real.norm_eq_abs, abs_of_nonneg (zero_le_one.trans x_one)]
    rw [← Real.rpow_neg_one x]
    exact Real.rpow_le_rpow_of_exponent_le x_one h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℝ
⊢ IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) atTop volume ↔ s < -1
have refine : IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) atTop volume →
  ∀ (t : Set ℝ) (ht : Membership.mem (γ := Filter ℝ) atTop t)
    (hint : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) t volume), s < -1
Tactic: refine ⟨fun ⟨t, ht, hint⟩ ↦ ?_, fun h ↦
    ⟨Set.Ioi 1, Ioi_mem_atTop 1, (integrableOn_Ioi_rpow_iff zero_lt_one).mpr h⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℝ
h : IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) atTop volume
t : Set ℝ
ht : Membership.mem (γ := Filter ℝ) atTop t
hint : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) t volume
⊢ s < -1
have obtain : ∀ (a : ℝ) (ha : ∀ b ≥ a, b ∈ t), s < -1
Tactic: obtain ⟨a, ha⟩ := mem_atTop_sets.mp ht
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
s : ℝ
h : IntegrableAtFilter (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) atTop volume
t : Set ℝ
ht : Membership.mem (γ := Filter ℝ) atTop t
hint : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) t volume
a : ℝ
ha : ∀ b ≥ a, b ∈ t
⊢ s < -1
have refine : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi (max a 1)) volume
Tactic: refine (integrableOn_Ioi_rpow_iff (zero_lt_one.trans_le (le_max_right a 1))).mp ?_
-- 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 ≤ -1), False
Tactic: rcases le_or_gt s (-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 ≤ -1), False
⊢ False
have inr : ∀ (hs : -1 < s), False
Tactic: rcases le_or_gt s (-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 ≤ -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 ≤ -1
this : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioo 0 1) volume
⊢ False
have this₁ : -1 < s
Tactic: rw [integrableOn_Ioo_rpow_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
⊢ 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
this : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ x ^ s) (Ioi 1) volume
⊢ False
have this₁ : s < -1
Tactic: rw [integrableOn_Ioi_rpow_iff zero_lt_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
⊢ HasDerivAt (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
have h : x ^ a = (a + 1) * x ^ (a + 1 - 1) / (a + 1)
Tactic: convert! (hasDerivAt_rpow_const (p := a + 1) (Or.inl (hc.trans_le hx).ne')).div_const _ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
⊢ a + 1 < 0
have linarith : 0 ≤ a + 1 → a - -1 + (0 - (a + 1)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (hypothesis)
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (t : ℝ) ↦ t ^ a) =
    -c ^ (a + 1) / (a + 1)
have hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
Tactic: have hd : ∀ x ∈ Ici c, HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x := by
    intro x hx
    convert! (hasDerivAt_rpow_const (p := a + 1) (Or.inl (hc.trans_le hx).ne')).div_const _ using 1
    simp [show a + 1 ≠ 0 from ne_of_lt (by linarith), mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ Tendsto (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
have hf : Tendsto (β := ℝ) (fun (a_1 : ℝ) ↦ a_1 ^ (a + 1)) atTop (𝓝 0)
Tactic: apply Tendsto.div_const
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ 0 < -(a + 1)
have linarith : -(a + 1) ≤ 0 → a - -1 + (-(a + 1) - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (hypothesis)
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (t : ℝ) ↦ t ^ a) =
    -c ^ (a + 1) / (a + 1)
have ht : Tendsto (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
Tactic: have ht : Tendsto (fun t => t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1))) := by
    apply Tendsto.div_const
    simpa only [neg_neg] using tendsto_rpow_neg_atTop (by linarith : 0 < -(a + 1))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.ImproperIntegrals (goal)
Goal:
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ x ∈ Ici c, HasDerivAt (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) (x ^ a) x
ht : Tendsto (fun (t : ℝ) ↦ t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1)))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi c)) fun (t : ℝ) ↦ t ^ a) =
    -c ^ (a + 1) / (a + 1)
have h : -c ^ (a + 1) / (a + 1) = 0 / (a + 1) - c ^ (a + 1) / (a + 1)
Tactic: convert! integral_Ioi_of_hasDerivAt_of_tendsto' hd (integrableOn_Ioi_rpow_of_lt ha hc) ht using 1
-- 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 : ∀ (x : ℝ) (hx : x ∈ Ioi c), x ^ a.re = ‖(↑x : ℂ) ^ a‖
Tactic: refine (integrableOn_Ioi_rpow_of_lt ha hc).congr_fun (fun x hx => ?_) measurableSet_Ioi