a b : ℝ
h : 0 < b
this : Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b))
⊢ IntegrableOn (fun x => exp (-b * x)) (Ioi a)
a b : ℝ
h : 0 < b
⊢ IntegrableOn (fun x => exp (-b * x)) (Ioi a)
have : Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b)) := by
  refine' Tendsto.div_const (Tendsto.neg _) _
  exact tendsto_exp_atBot.comp (tendsto_id.neg_const_mul_atTop (Right.neg_neg_iff.2 h))
a b : ℝ
h : 0 < b
this : Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b))
x : ℝ
x✝ : x ∈ Ici a
⊢ HasDerivAt (fun x => -exp (-b * x) / b) (exp (-b * x)) x
a b : ℝ
h : 0 < b
this : Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b))
⊢ IntegrableOn (fun x => exp (-b * x)) (Ioi a)
refine' integrableOn_Ioi_deriv_of_nonneg' (fun x _ => _) (fun x _ => (exp_pos _).le) this
no goals
a b : ℝ
h : 0 < b
this : Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b))
x : ℝ
x✝ : x ∈ Ici a
⊢ HasDerivAt (fun x => -exp (-b * x) / b) (exp (-b * x)) x
simpa [h.ne'] using ((hasDerivAt_id x).const_mul b).neg.exp.neg.div_const b
a b : ℝ
h : 0 < b
⊢ Tendsto (fun x => exp (-b * x)) atTop (𝓝 0)
a b : ℝ
h : 0 < b
⊢ Tendsto (fun x => -exp (-b * x) / b) atTop (𝓝 (-0 / b))
refine' Tendsto.div_const (Tendsto.neg _) _
no goals
a b : ℝ
h : 0 < b
⊢ Tendsto (fun x => exp (-b * x)) atTop (𝓝 0)
exact tendsto_exp_atBot.comp (tendsto_id.neg_const_mul_atTop (Right.neg_neg_iff.2 h))