E : Type ?u.179480
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' g : ℝ → ℝ
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) (Ici a)
hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
⊢ (∫ (x : ℝ) in Ioi a, (g ∘ f) x * f' x) = ∫ (u : ℝ) in Ioi (f a), g u
E : Type ?u.179480
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' g : ℝ → ℝ
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) (Ici a)
⊢ (∫ (x : ℝ) in Ioi a, (g ∘ f) x * f' x) = ∫ (u : ℝ) in Ioi (f a), g u
have hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a) := by simpa [mul_comm] using hg2
no goals
E : Type ?u.179480
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' g : ℝ → ℝ
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) (Ici a)
hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
⊢ (∫ (x : ℝ) in Ioi a, (g ∘ f) x * f' x) = ∫ (u : ℝ) in Ioi (f a), g u
simpa [mul_comm] using integral_comp_smul_deriv_Ioi hf hft hff' hg_cont hg1 hg2'
no goals
E : Type ?u.179480
f✝ : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f f' g : ℝ → ℝ
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ (x : ℝ), x ∈ Ioi a → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn g (f '' Ici a)
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) (Ici a)
⊢ IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)
simpa [mul_comm] using hg2