[GOAL]
c : ℝ
⊢ IntegrableOn exp (Iic c)
[PROOFSTEP]
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 _ => _)
[GOAL]
c y : ℝ
x✝ : y ∈ Iic 0
⊢ ∫ (x : ℝ) in id y..c, ‖exp x‖ ≤ exp c
[PROOFSTEP]
simp_rw [norm_of_nonneg (exp_pos _).le, integral_exp, sub_le_self_iff]
[GOAL]
c y : ℝ
x✝ : y ∈ Iic 0
⊢ 0 ≤ exp (id y)
[PROOFSTEP]
exact (exp_pos _).le
[GOAL]
c : ℝ
⊢ ∫ (x : ℝ) in Iic c, exp x = exp c
[PROOFSTEP]
refine' tendsto_nhds_unique (intervalIntegral_tendsto_integral_Iic _ (integrableOn_exp_Iic _) tendsto_id) _
[GOAL]
c : ℝ
⊢ Tendsto (fun i => ∫ (x : ℝ) in id i..c, exp x) atBot (𝓝 (exp c))
[PROOFSTEP]
simp_rw [integral_exp, show 𝓝 (exp c) = 𝓝 (exp c - 0) by rw [sub_zero]]
[GOAL]
c : ℝ
⊢ 𝓝 (exp c) = 𝓝 (exp c - 0)
[PROOFSTEP]
rw [sub_zero]
[GOAL]
c : ℝ
⊢ Tendsto (fun i => exp c - exp (id i)) atBot (𝓝 (exp c - 0))
[PROOFSTEP]
exact tendsto_exp_atBot.const_sub _
[GOAL]
c : ℝ
⊢ ∫ (x : ℝ) in Ioi c, exp (-x) = exp (-c)
[PROOFSTEP]
simpa only [integral_comp_neg_Ioi] using integral_exp_Iic (-c)
[GOAL]
⊢ ∫ (x : ℝ) in Ioi 0, exp (-x) = 1
[PROOFSTEP]
simpa only [neg_zero, exp_zero] using integral_exp_neg_Ioi 0
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
⊢ IntegrableOn (fun t => t ^ a) (Ioi c)
[PROOFSTEP]
have hd : ∀ (x : ℝ) (_ : 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
  field_simp [show a + 1 ≠ 0 from ne_of_lt (by linarith), mul_comm]
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
⊢ ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
[PROOFSTEP]
intro x hx
[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
[PROOFSTEP]
convert (hasDerivAt_rpow_const (p := a + 1) (Or.inl (hc.trans_le hx).ne')).div_const _ using 1
[GOAL]
case h.e'_7
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
⊢ x ^ a = (a + 1) * x ^ (a + 1 - 1) / (a + 1)
[PROOFSTEP]
field_simp [show a + 1 ≠ 0 from ne_of_lt (by linarith), mul_comm]
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
⊢ a + 1 < 0
[PROOFSTEP]
linarith
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ IntegrableOn (fun t => t ^ a) (Ioi c)
[PROOFSTEP]
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))
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), 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)))
[PROOFSTEP]
apply Tendsto.div_const
[GOAL]
case hf
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ Tendsto (fun a_1 => a_1 ^ (a + 1)) atTop (𝓝 0)
[PROOFSTEP]
simpa only [neg_neg] using tendsto_rpow_neg_atTop (by linarith : 0 < -(a + 1))
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ 0 < -(a + 1)
[PROOFSTEP]
linarith
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), 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)))
⊢ IntegrableOn (fun t => t ^ a) (Ioi c)
[PROOFSTEP]
exact integrableOn_Ioi_deriv_of_nonneg' hd (fun t ht => rpow_nonneg_of_nonneg (hc.trans ht).le a) ht
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
⊢ ∫ (t : ℝ) in Ioi c, t ^ a = -c ^ (a + 1) / (a + 1)
[PROOFSTEP]
have hd : ∀ (x : ℝ) (_ : 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
  field_simp [show a + 1 ≠ 0 from ne_of_lt (by linarith), mul_comm]
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
⊢ ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
[PROOFSTEP]
intro x hx
[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
[PROOFSTEP]
convert (hasDerivAt_rpow_const (p := a + 1) (Or.inl (hc.trans_le hx).ne')).div_const _ using 1
[GOAL]
case h.e'_7
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
⊢ x ^ a = (a + 1) * x ^ (a + 1 - 1) / (a + 1)
[PROOFSTEP]
field_simp [show a + 1 ≠ 0 from ne_of_lt (by linarith), mul_comm]
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ici c
⊢ a + 1 < 0
[PROOFSTEP]
linarith
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ ∫ (t : ℝ) in Ioi c, t ^ a = -c ^ (a + 1) / (a + 1)
[PROOFSTEP]
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))
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), 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)))
[PROOFSTEP]
apply Tendsto.div_const
[GOAL]
case hf
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ Tendsto (fun a_1 => a_1 ^ (a + 1)) atTop (𝓝 0)
[PROOFSTEP]
simpa only [neg_neg] using tendsto_rpow_neg_atTop (by linarith : 0 < -(a + 1))
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), x ∈ Ici c → HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x
⊢ 0 < -(a + 1)
[PROOFSTEP]
linarith
[GOAL]
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), 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)))
⊢ ∫ (t : ℝ) in Ioi c, t ^ a = -c ^ (a + 1) / (a + 1)
[PROOFSTEP]
convert integral_Ioi_of_hasDerivAt_of_tendsto' hd (integrableOn_Ioi_rpow_of_lt ha hc) ht using 1
[GOAL]
case h.e'_3
a : ℝ
ha : a < -1
c : ℝ
hc : 0 < c
hd : ∀ (x : ℝ), 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)))
⊢ -c ^ (a + 1) / (a + 1) = 0 / (a + 1) - c ^ (a + 1) / (a + 1)
[PROOFSTEP]
simp only [neg_div, zero_div, zero_sub]
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ IntegrableOn (fun t => ↑t ^ a) (Ioi c)
[PROOFSTEP]
rw [IntegrableOn, ← integrable_norm_iff, ← IntegrableOn]
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ IntegrableOn (fun a_1 => ‖↑a_1 ^ a‖) (Ioi c)
a : ℂ ha : a.re < -1 c : ℝ hc : 0 < c ⊢ AEStronglyMeasurable (fun t => ↑t ^ a) (Measure.restrict volume (Ioi c))
[PROOFSTEP]
refine' (integrableOn_Ioi_rpow_of_lt ha hc).congr_fun (fun x hx => _) measurableSet_Ioi
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ioi c
⊢ x ^ a.re = ‖↑x ^ a‖
[PROOFSTEP]
dsimp only
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Ioi c
⊢ x ^ a.re = ‖↑x ^ a‖
[PROOFSTEP]
rw [Complex.norm_eq_abs, Complex.abs_cpow_eq_rpow_re_of_pos (hc.trans hx)]
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ AEStronglyMeasurable (fun t => ↑t ^ a) (Measure.restrict volume (Ioi c))
[PROOFSTEP]
refine' ContinuousOn.aestronglyMeasurable (fun t ht => _) measurableSet_Ioi
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
t : ℝ
ht : t ∈ Ioi c
⊢ ContinuousWithinAt (fun t => ↑t ^ a) (Ioi c) t
[PROOFSTEP]
exact (Complex.continuousAt_ofReal_cpow_const _ _ (Or.inr (hc.trans ht).ne')).continuousWithinAt
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ ∫ (t : ℝ) in Ioi c, ↑t ^ a = -↑c ^ (a + 1) / (a + 1)
[PROOFSTEP]
refine' tendsto_nhds_unique (intervalIntegral_tendsto_integral_Ioi c (integrableOn_Ioi_cpow_of_lt ha hc) tendsto_id) _
[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)))
[PROOFSTEP]
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.def]
  refine' Or.inr ⟨_, not_mem_uIcc_of_lt hc hx⟩
  apply_fun Complex.re
  rw [Complex.neg_re, Complex.one_re]
  exact ha.ne
[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)))
[PROOFSTEP]
refine' this.congr' ((eventually_gt_atTop 0).mp (eventually_of_forall fun x hx => _))
[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) = (fun i => ∫ (x : ℝ) in c..id i, ↑x ^ a) x
[PROOFSTEP]
dsimp only
[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
[PROOFSTEP]
rw [integral_cpow, id.def]
[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)
[PROOFSTEP]
refine' Or.inr ⟨_, not_mem_uIcc_of_lt hc hx⟩
[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
[PROOFSTEP]
apply_fun Complex.re
[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.re ≠ (-1).re
[PROOFSTEP]
rw [Complex.neg_re, Complex.one_re]
[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.re ≠ -1
[PROOFSTEP]
exact ha.ne
[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)))
[PROOFSTEP]
simp_rw [← zero_sub, sub_div]
[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)))
[PROOFSTEP]
refine' (Tendsto.div_const _ _).sub_const _
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ Tendsto (fun x => ↑x ^ (a + 1)) atTop (𝓝 0)
[PROOFSTEP]
rw [tendsto_zero_iff_norm_tendsto_zero]
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ Tendsto (fun e => ‖↑e ^ (a + 1)‖) atTop (𝓝 0)
[PROOFSTEP]
refine'
  (tendsto_rpow_neg_atTop (by linarith : 0 < -(a.re + 1))).congr'
    ((eventually_gt_atTop 0).mp (eventually_of_forall fun x hx => _))
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
⊢ 0 < -(a.re + 1)
[PROOFSTEP]
linarith
[GOAL]
a : ℂ
ha : a.re < -1
c : ℝ
hc : 0 < c
x : ℝ
hx : 0 < x
⊢ x ^ (- -(a.re + 1)) = (fun e => ‖↑e ^ (a + 1)‖) x
[PROOFSTEP]
simp_rw [neg_neg, Complex.norm_eq_abs, Complex.abs_cpow_eq_rpow_re_of_pos hx, Complex.add_re, Complex.one_re]
