ι : Type ?u.1930290
𝕜 : Type ?u.1930293
E : Type ?u.1930296
F : Type ?u.1930299
A : Type ?u.1930302
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' g : ℝ → ℝ
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntegrableOn g (f '' [[a, b]])
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) [[a, b]]
hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
⊢ (∫ (x : ℝ) in a..b, (g ∘ f) x * f' x) = ∫ (u : ℝ) in f a..f b, g u
ι : Type ?u.1930290
𝕜 : Type ?u.1930293
E : Type ?u.1930296
F : Type ?u.1930299
A : Type ?u.1930302
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' g : ℝ → ℝ
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntegrableOn g (f '' [[a, b]])
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) [[a, b]]
⊢ (∫ (x : ℝ) in a..b, (g ∘ f) x * f' x) = ∫ (u : ℝ) in f a..f b, g u
have hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] := by simpa [mul_comm] using hg2
no goals
ι : Type ?u.1930290
𝕜 : Type ?u.1930293
E : Type ?u.1930296
F : Type ?u.1930299
A : Type ?u.1930302
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' g : ℝ → ℝ
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntegrableOn g (f '' [[a, b]])
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) [[a, b]]
hg2' : IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
⊢ (∫ (x : ℝ) in a..b, (g ∘ f) x * f' x) = ∫ (u : ℝ) in f a..f b, g u
simpa [mul_comm] using integral_comp_smul_deriv''' hf hff' hg_cont hg1 hg2'
no goals
ι : Type ?u.1930290
𝕜 : Type ?u.1930293
E : Type ?u.1930296
F : Type ?u.1930299
A : Type ?u.1930302
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝¹ : ℝ → E
g' g✝ φ : ℝ → ℝ
f✝ f'✝ : ℝ → E
a b : ℝ
f f' g : ℝ → ℝ
hf : ContinuousOn f [[a, b]]
hff' : ∀ (x : ℝ), x ∈ Ioo (min a b) (max a b) → HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))
hg1 : IntegrableOn g (f '' [[a, b]])
hg2 : IntegrableOn (fun x => (g ∘ f) x * f' x) [[a, b]]
⊢ IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]]
simpa [mul_comm] using hg2