E : Type ?u.162446
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'neg : ∀ (x : ℝ), x ∈ Ioi a → g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ Integrable (-g')
E : Type ?u.162446
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'neg : ∀ (x : ℝ), x ∈ Ioi a → g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn g' (Ioi a)
apply integrable_neg_iff.1
no goals
E : Type ?u.162446
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn g (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt g (g' x) x
g'neg : ∀ (x : ℝ), x ∈ Ioi a → g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ Integrable (-g')
exact integrableOn_Ioi_deriv_of_nonneg hcont.neg (fun x hx => (hderiv x hx).neg)
  (fun x hx => neg_nonneg_of_nonpos (g'neg x hx)) hg.neg